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∧b2−D⁢c2=1→b∈ℤ∧∃c∈ℤa=b+D⁢c∧b2−D⁢c2=1
4 3 reximdv2 ⊢D∈ℕ∖◻ℕ→∃b∈ℕ0∃c∈ℤa=b+D⁢c∧b2−D⁢c2=1→∃b∈ℤ∃c∈ℤa=b+D⁢c∧b2−D⁢c2=1
5 4 anim2d ⊢D∈ℕ∖◻ℕ→a∈ℝ∧∃b∈ℕ0∃c∈ℤa=b+D⁢c∧b2−D⁢c2=1→a∈ℝ∧∃b∈ℤ∃c∈ℤa=b+D⁢c∧b2−D⁢c2=1
6 elpell14qr ⊢D∈ℕ∖◻ℕ→a∈Pell14QR⁡D↔a∈ℝ∧∃b∈ℕ0∃c∈ℤa=b+D⁢c∧b2−D⁢c2=1
7 elpell1234qr ⊢D∈ℕ∖◻ℕ→a∈Pell1234QR⁡D↔a∈ℝ∧∃b∈ℤ∃c∈ℤa=b+D⁢c∧b2−D⁢c2=1
8 5 6 7 3imtr4d ⊢D∈ℕ∖◻ℕ→a∈Pell14QR⁡D→a∈Pell1234QR⁡D
9 8 ssrdv ⊢D∈ℕ∖◻ℕ→Pell14QR⁡D⊆Pell1234QR⁡D