Theorem pell14qrss1234

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

	Ref	Expression
Assertion	pell14qrss1234	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell14QR ‘ 𝐷 ) ⊆ ( Pell1234QR ‘ 𝐷 ) )

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	anim2d	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝑎 ∈ ℝ ∧ ∃ 𝑏 ∈ ℕ0 ∃ 𝑐 ∈ ℤ ( 𝑎 = ( 𝑏 + ( ( √ ‘ 𝐷 ) · 𝑐 ) ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 ∈ ℝ ∧ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ( 𝑎 = ( 𝑏 + ( ( √ ‘ 𝐷 ) · 𝑐 ) ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 1 ) ) ) )
6		elpell14qr	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝑎 ∈ ℝ ∧ ∃ 𝑏 ∈ ℕ0 ∃ 𝑐 ∈ ℤ ( 𝑎 = ( 𝑏 + ( ( √ ‘ 𝐷 ) · 𝑐 ) ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 1 ) ) ) )
7		elpell1234qr	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑎 ∈ ( Pell1234QR ‘ 𝐷 ) ↔ ( 𝑎 ∈ ℝ ∧ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ( 𝑎 = ( 𝑏 + ( ( √ ‘ 𝐷 ) · 𝑐 ) ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 1 ) ) ) )
8	5 6 7	3imtr4d	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) → 𝑎 ∈ ( Pell1234QR ‘ 𝐷 ) ) )
9	8	ssrdv	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell14QR ‘ 𝐷 ) ⊆ ( Pell1234QR ‘ 𝐷 ) )