\\Header (and we assume the rules in the MathSE post)

PA1 ∀k∈N ∃m∈N ( k = m·2 ∨ k = m·2+1 )
PA1* ∀k,m ∈ N (k = 2m -> ¬∃n ∈ N (k = 2n+1)) \\modified PA1
P1 Z ∈ set
P2 φ is a property with two parameters and ∀x∀y: φ(x,y) <-> ∃z∈N [(x=2z ^ y=z) v (x=2z+1 ^ y=-z)]
P3 y ∈ {x : ψ(x)} <-> ψ(y)
P4 N ⊆ Z

\\Prove F := {⟨x,y⟩:x∈N ^ y ∈ Z ^ φ(x,y)} is a set in P(N x Z)
1 N x Z ∈ set \\from P1, **naturals**, **product-type**
2 F = {p: p ∈ N x Z ^ ∃n ∈ N ∃z ∈ Z (p = ⟨n,z⟩ ^ φ(n,z))} ∈ set \\from **comprehension**

∀ a,b,c,x ∈ ℝ ( a·x^2+b·x+c = 0 ∧ a ≠ 0 ⇒ x = –(b/(2·a))+√((b^2-4·a·c)/4·a^2) ∨ x = –(b/(2·a))–√((b^2-4·a·c)/4·a^2) ) [lemma]
  Given a,b,c,x ∈ ℝ:
    If a·x^2+b·x+c = 0 ∧ a ≠ 0:
      a·x^2+b·x+c = a·(x^2+b·x/a+c/a)
      a·(x^2+b·x+c) = a·(x+(b/(2·a)))^2+c/a–(b^2/4·a^2))
      x^2+b·x+c = (x+(b/(2·a)))^2+c/a–(b^2/4·a^2) [cancellation since a ≠ 0]
      (x+(b/(2·a)))^2+c/a–(b^2/4·a^2) = 0
      (x+(b/(2·a)))^2 = –c/a+(b^2/4·a^2)
      (x+(b/(2·a)))^2 = (b^2-4·a·c)/4·a^2
      √((x+(b/(2·a)))^2) = √((b^2-4·a·c)/4·a^2)