Metamath Proof Explorer

Theorem elpell14qr

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

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

Proof

Step Hyp Ref Expression
1 pell14qrval ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D = a ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ a = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
2 1 eleq2d ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell14QR ⁡ D ↔ A ∈ a ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ 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 ∈ ℤ a = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1 ↔ ∃ z ∈ ℕ 0 ∃ w ∈ ℤ A = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
6 5 elrab ⊢ A ∈ a ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ a = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1 ↔ A ∈ ℝ ∧ ∃ z ∈ ℕ 0 ∃ w ∈ ℤ A = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1
7 2 6 syl6bb ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell14QR ⁡ D ↔ A ∈ ℝ ∧ ∃ z ∈ ℕ 0 ∃ w ∈ ℤ A = z + D ⁢ w ∧ z 2 − D ⁢ w 2 = 1