Theorem pell14qrne0

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

	Ref	Expression
Assertion	pell14qrne0	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		pell14qrss1234	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell14QR ‘ 𝐷 ) ⊆ ( Pell1234QR ‘ 𝐷 ) )
2	1	sselda	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) )
3		pell1234qrne0	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ) → 𝐴 ≠ 0 )
4	2 3	syldan	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ≠ 0 )