Metamath Proof Explorer

Theorem pell14qrval

Description: Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell14qrval ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D = y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ a = D → a = D
2 1 oveq1d ⊢ a = D → a ⁢ w = D ⁢ w
3 2 oveq2d ⊢ a = D → z + a ⁢ w = z + D ⁢ w
4 3 eqeq2d ⊢ a = D → y = z + a ⁢ w ↔ y = z + D ⁢ w
5 oveq1 ⊢ a = D → a ⁢ w 2 = D ⁢ w 2
6 5 oveq2d ⊢ a = D → z 2 − a ⁢ w 2 = z 2 − D ⁢ w 2
7 6 eqeq1d ⊢ a = D → z 2 − a ⁢ w 2 = 1 ↔ z 2 − D ⁢ w 2 = 1
8 4 7 anbi12d ⊢ a = D → y = z + a ⁢ w ∧ z 2 − a ⁢ w 2 = 1 ↔ y = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
9 8 2rexbidv ⊢ a = D → ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + a ⁢ w ∧ z 2 − a ⁢ w 2 = 1 ↔ ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
10 9 rabbidv ⊢ a = D → y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + a ⁢ w ∧ z 2 − a ⁢ w 2 = 1 = y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
11 df-pell14qr ⊢ Pell14QR = a ∈ ℕ ∖ ◻ ℕ ⟼ y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + a ⁢ w ∧ z 2 − a ⁢ w 2 = 1
12 reex ⊢ ℝ ∈ V
13 12 rabex ⊢ y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1 ∈ V
14 10 11 13 fvmpt ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D = y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1