Metamath Proof Explorer

Theorem elpell1234qr

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

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

Proof

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