Metamath Proof Explorer

Theorem pell1234qrval

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

Ref Expression
Assertion pell1234qrval ⊢D∈ℕ∖◻ℕ→Pell1234QR⁡D=y∈ℝ|∃z∈ℤ∃w∈ℤy=z+D⁢w∧z2−D⁢w2=1

Proof

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