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