Metamath Proof Explorer

Theorem pell14qrss1234

Description: A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrss1234 ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D ⊆ Pell1234QR ⁡ D

Proof

Step Hyp Ref Expression
1 nn0z ⊢ b ∈ ℕ 0 → b ∈ ℤ
2 1 a1i ⊢ D ∈ ℕ ∖ ◻ ℕ → b ∈ ℕ 0 → b ∈ ℤ
3 2 anim1d ⊢ D ∈ ℕ ∖ ◻ ℕ → b ∈ ℕ 0 ∧ ∃ c ∈ ℤ a = b + D ⁢ c ∧ b 2 − D ⁢ c 2 = 1 → b ∈ ℤ ∧ ∃ c ∈ ℤ a = b + D ⁢ c ∧ b 2 − D ⁢ c 2 = 1
4 3 reximdv2 ⊢ D ∈ ℕ ∖ ◻ ℕ → ∃ b ∈ ℕ 0 ∃ c ∈ ℤ a = b + D ⁢ c ∧ b 2 − D ⁢ c 2 = 1 → ∃ b ∈ ℤ ∃ c ∈ ℤ a = b + D ⁢ c ∧ b 2 − D ⁢ c 2 = 1
5 4 anim2d ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ ℝ ∧ ∃ b ∈ ℕ 0 ∃ c ∈ ℤ a = b + D ⁢ c ∧ b 2 − D ⁢ c 2 = 1 → a ∈ ℝ ∧ ∃ b ∈ ℤ ∃ c ∈ ℤ a = b + D ⁢ c ∧ b 2 − D ⁢ c 2 = 1
6 elpell14qr ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ Pell14QR ⁡ D ↔ a ∈ ℝ ∧ ∃ b ∈ ℕ 0 ∃ c ∈ ℤ a = b + D ⁢ c ∧ b 2 − D ⁢ c 2 = 1
7 elpell1234qr ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ Pell1234QR ⁡ D ↔ a ∈ ℝ ∧ ∃ b ∈ ℤ ∃ c ∈ ℤ a = b + D ⁢ c ∧ b 2 − D ⁢ c 2 = 1
8 5 6 7 3imtr4d ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ Pell14QR ⁡ D → a ∈ Pell1234QR ⁡ D
9 8 ssrdv ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D ⊆ Pell1234QR ⁡ D