Metamath Proof Explorer

Theorem pell1qrss14

Description: First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1qrss14 ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell1QR ⁡ D ⊆ Pell14QR ⁡ D

Proof

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