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	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ )
2	1	a1i	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ ) )
3	2	anim1d	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝑏 ∈ ℕ0 ∧ ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝑏 ∈ ℤ ∧ ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
4	3	reximdv2	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ∃ 𝑏 ∈ ℕ0 ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ∃ 𝑏 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) )
5	4	reximdv	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) )
6	5	anim2d	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝑎 ∈ ℝ ∧ ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 ∈ ℝ ∧ ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
7		elpell1qr	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝑎 ∈ ℝ ∧ ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
8		elpell14qr	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝑎 ∈ ℝ ∧ ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
9	6 7 8	3imtr4d	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) → 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ) )
10	9	ssrdv	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) )