Metamath Proof Explorer

Theorem pell1qrval

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

Ref Expression
Assertion pell1qrval ⊢D∈ℕ∖◻ℕ→Pell1QR⁡D=y∈ℝ|∃z∈ℕ0∃w∈ℕ0y=z+D⁢w∧z2−D⁢w2=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⁢w2=D⁢w2
6 5 oveq2d ⊢a=D→z2−a⁢w2=z2−D⁢w2
7 6 eqeq1d ⊢a=D→z2−a⁢w2=1↔z2−D⁢w2=1
8 4 7 anbi12d ⊢a=D→y=z+a⁢w∧z2−a⁢w2=1↔y=z+D⁢w∧z2−D⁢w2=1
9 8 2rexbidv ⊢a=D→∃z∈ℕ0∃w∈ℕ0y=z+a⁢w∧z2−a⁢w2=1↔∃z∈ℕ0∃w∈ℕ0y=z+D⁢w∧z2−D⁢w2=1
10 9 rabbidv ⊢a=D→y∈ℝ|∃z∈ℕ0∃w∈ℕ0y=z+a⁢w∧z2−a⁢w2=1=y∈ℝ|∃z∈ℕ0∃w∈ℕ0y=z+D⁢w∧z2−D⁢w2=1
11 df-pell1qr ⊢Pell1QR=a∈ℕ∖◻ℕ⟼y∈ℝ|∃z∈ℕ0∃w∈ℕ0y=z+a⁢w∧z2−a⁢w2=1
12 reex ⊢ℝ∈V
13 12 rabex ⊢y∈ℝ|∃z∈ℕ0∃w∈ℕ0y=z+D⁢w∧z2−D⁢w2=1∈V
14 10 11 13 fvmpt ⊢D∈ℕ∖◻ℕ→Pell1QR⁡D=y∈ℝ|∃z∈ℕ0∃w∈ℕ0y=z+D⁢w∧z2−D⁢w2=1