Theorem elpell1qr

Description: Membership in a first-quadrant Pell solution set. (Contributed by Stefan O'Rear, 17-Sep-2014)

	Ref	Expression
Assertion	elpell1qr	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pell1qrval	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) = { 𝑎 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )
2	1	eleq2d	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ 𝐴 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } ) )
3		eqeq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ↔ 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ) )
4	3	anbi1d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ↔ ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) )
5	4	2rexbidv	⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ↔ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) )
6	5	elrab	⊢ ( 𝐴 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) )
7	2 6	bitrdi	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) ) )