Theorem pell1qrval

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

	Ref	Expression
Assertion	pell1qrval	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) = { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑎 = 𝐷 → ( √ ‘ 𝑎 ) = ( √ ‘ 𝐷 ) )
2	1	oveq1d	⊢ ( 𝑎 = 𝐷 → ( ( √ ‘ 𝑎 ) · 𝑤 ) = ( ( √ ‘ 𝐷 ) · 𝑤 ) )
3	2	oveq2d	⊢ ( 𝑎 = 𝐷 → ( 𝑧 + ( ( √ ‘ 𝑎 ) · 𝑤 ) ) = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) )
4	3	eqeq2d	⊢ ( 𝑎 = 𝐷 → ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑎 ) · 𝑤 ) ) ↔ 𝑦 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ) )
5		oveq1	⊢ ( 𝑎 = 𝐷 → ( 𝑎 · ( 𝑤 ↑ 2 ) ) = ( 𝐷 · ( 𝑤 ↑ 2 ) ) )
6	5	oveq2d	⊢ ( 𝑎 = 𝐷 → ( ( 𝑧 ↑ 2 ) − ( 𝑎 · ( 𝑤 ↑ 2 ) ) ) = ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) )
7	6	eqeq1d	⊢ ( 𝑎 = 𝐷 → ( ( ( 𝑧 ↑ 2 ) − ( 𝑎 · ( 𝑤 ↑ 2 ) ) ) = 1 ↔ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) )
8	4 7	anbi12d	⊢ ( 𝑎 = 𝐷 → ( ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑎 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑎 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ↔ ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) )
9	8	2rexbidv	⊢ ( 𝑎 = 𝐷 → ( ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑎 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑎 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ↔ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) )
10	9	rabbidv	⊢ ( 𝑎 = 𝐷 → { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑎 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑎 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } = { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )
11		df-pell1qr	⊢ Pell1QR = ( 𝑎 ∈ ( ℕ ∖ ◻NN ) ↦ { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑎 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑎 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )
12		reex	⊢ ℝ ∈ V
13	12	rabex	⊢ { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } ∈ V
14	10 11 13	fvmpt	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) = { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )