Metamath Proof Explorer

Theorem pell14qrne0

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

Ref Expression
Assertion pell14qrne0 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ≠ 0

Proof

Step Hyp Ref Expression
1 pell14qrss1234 ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D ⊆ Pell1234QR ⁡ D
2 1 sselda ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ∈ Pell1234QR ⁡ D
3 pell1234qrne0 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1234QR ⁡ D → A ≠ 0
4 2 3 syldan ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ≠ 0