Metamath Proof Explorer

Theorem pell1234qrne0

Description: No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell1234qrne0 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A =/= 0 )

Proof

Step Hyp Ref Expression
1 elpell1234qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1234QR ` D ) <-> ( A e. RR /\ E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
2 simprl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
3 ax-1ne0 
 |-  1 =/= 0
4 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
5 4 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR ) -> D e. NN )
6 5 nncnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR ) -> D e. CC )
7 6 ad3antrrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> D e. CC )
8 7 sqrtcld 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( sqrt ` D ) e. CC )
9 zcn 
 |-  ( b e. ZZ -> b e. CC )
10 9 ad2antll 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
11 10 ad2antrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> b e. CC )
12 8 11 sqmuld 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( ( sqrt ` D ) x. b ) ^ 2 ) = ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) )
13 7 sqsqrtd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( sqrt ` D ) ^ 2 ) = D )
14 13 oveq1d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) = ( D x. ( b ^ 2 ) ) )
15 12 14 eqtr2d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( D x. ( b ^ 2 ) ) = ( ( ( sqrt ` D ) x. b ) ^ 2 ) )
16 15 oveq2d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) )
17 zcn 
 |-  ( a e. ZZ -> a e. CC )
18 17 ad2antrl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
19 18 ad2antrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> a e. CC )
20 8 11 mulcld 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( sqrt ` D ) x. b ) e. CC )
21 subsq 
 |-  ( ( a e. CC /\ ( ( sqrt ` D ) x. b ) e. CC ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
22 19 20 21 syl2anc 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
23 16 22 eqtrd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
24 simplr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
25 simpr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( a + ( ( sqrt ` D ) x. b ) ) = 0 )
26 25 oveq1d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) = ( 0 x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
27 19 20 subcld 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( a - ( ( sqrt ` D ) x. b ) ) e. CC )
28 27 mul02d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( 0 x. ( a - ( ( sqrt ` D ) x. b ) ) ) = 0 )
29 26 28 eqtrd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) = 0 )
30 23 24 29 3eqtr3d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) /\ ( a + ( ( sqrt ` D ) x. b ) ) = 0 ) -> 1 = 0 )
31 30 ex 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( a + ( ( sqrt ` D ) x. b ) ) = 0 -> 1 = 0 ) )
32 31 necon3d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( 1 =/= 0 -> ( a + ( ( sqrt ` D ) x. b ) ) =/= 0 ) )
33 3 32 mpi 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( a + ( ( sqrt ` D ) x. b ) ) =/= 0 )
34 33 adantrl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a + ( ( sqrt ` D ) x. b ) ) =/= 0 )
35 2 34 eqnetrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A =/= 0 )
36 35 ex 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> A =/= 0 ) )
37 36 rexlimdvva 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR ) -> ( E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> A =/= 0 ) )
38 37 expimpd 
 |-  ( D e. ( NN \ []NN ) -> ( ( A e. RR /\ E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A =/= 0 ) )
39 1 38 sylbid 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1234QR ` D ) -> A =/= 0 ) )
40 39 imp 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A =/= 0 )