Metamath Proof Explorer

Theorem elpell1qr

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

Ref Expression
Assertion elpell1qr ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell1QR ⁡ D ↔ A ∈ ℝ ∧ ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 A = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1

Proof

Step Hyp Ref Expression
1 pell1qrval ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell1QR ⁡ D = a ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 a = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
2 1 eleq2d ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell1QR ⁡ D ↔ A ∈ a ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 a = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
3 eqeq1 ⊢ a = A → a = z + D ⁢ w ↔ A = z + D ⁢ w
4 3 anbi1d ⊢ a = A → a = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1 ↔ A = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
5 4 2rexbidv ⊢ a = A → ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 a = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1 ↔ ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 A = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
6 5 elrab ⊢ A ∈ a ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 a = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1 ↔ A ∈ ℝ ∧ ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 A = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
7 2 6 bitrdi ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell1QR ⁡ D ↔ A ∈ ℝ ∧ ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 A = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1