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 e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A =/= 0 )

Proof

Step Hyp Ref Expression
1 pell14qrss1234 
 |-  ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ ( Pell1234QR ` D ) )
2 1 sselda 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. ( Pell1234QR ` D ) )
3 pell1234qrne0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A =/= 0 )
4 2 3 syldan 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A =/= 0 )