Metamath Proof Explorer

Theorem pellexlem1

Description: Lemma for pellex . Arithmetical core of pellexlem3, norm lower bound. This begins Dirichlet's proof of the Pell equation solution existence; the proof here follows theorem 62 of vandenDries p. 43. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion pellexlem1 
|- ( ( ( D e. NN /\ A e. NN /\ B e. NN ) /\ -. ( sqrt ` D ) e. QQ ) -> ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) =/= 0 )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( A e. NN -> A e. CC )
2 1 3ad2ant2 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> A e. CC )
3 2 sqcld 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( A ^ 2 ) e. CC )
4 nncn 
 |-  ( D e. NN -> D e. CC )
5 4 3ad2ant1 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> D e. CC )
6 nncn 
 |-  ( B e. NN -> B e. CC )
7 6 3ad2ant3 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> B e. CC )
8 7 sqcld 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( B ^ 2 ) e. CC )
9 5 8 mulcld 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( D x. ( B ^ 2 ) ) e. CC )
10 3 9 subeq0ad 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 0 <-> ( A ^ 2 ) = ( D x. ( B ^ 2 ) ) ) )
11 nnne0 
 |-  ( B e. NN -> B =/= 0 )
12 11 3ad2ant3 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> B =/= 0 )
13 sqne0 
 |-  ( B e. CC -> ( ( B ^ 2 ) =/= 0 <-> B =/= 0 ) )
14 7 13 syl 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( ( B ^ 2 ) =/= 0 <-> B =/= 0 ) )
15 12 14 mpbird 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( B ^ 2 ) =/= 0 )
16 3 5 8 15 divmul3d 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( ( ( A ^ 2 ) / ( B ^ 2 ) ) = D <-> ( A ^ 2 ) = ( D x. ( B ^ 2 ) ) ) )
17 sqdiv 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )
18 17 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( sqrt ` ( ( A / B ) ^ 2 ) ) = ( sqrt ` ( ( A ^ 2 ) / ( B ^ 2 ) ) ) )
19 2 7 12 18 syl3anc 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( sqrt ` ( ( A / B ) ^ 2 ) ) = ( sqrt ` ( ( A ^ 2 ) / ( B ^ 2 ) ) ) )
20 nnre 
 |-  ( A e. NN -> A e. RR )
21 20 3ad2ant2 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> A e. RR )
22 nnre 
 |-  ( B e. NN -> B e. RR )
23 22 3ad2ant3 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> B e. RR )
24 21 23 12 redivcld 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( A / B ) e. RR )
25 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
26 25 nn0ge0d 
 |-  ( A e. NN -> 0 <_ A )
27 26 3ad2ant2 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> 0 <_ A )
28 nngt0 
 |-  ( B e. NN -> 0 < B )
29 28 3ad2ant3 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> 0 < B )
30 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( A / B ) )
31 21 27 23 29 30 syl22anc 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> 0 <_ ( A / B ) )
32 24 31 sqrtsqd 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( sqrt ` ( ( A / B ) ^ 2 ) ) = ( A / B ) )
33 19 32 eqtr3d 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( sqrt ` ( ( A ^ 2 ) / ( B ^ 2 ) ) ) = ( A / B ) )
34 nnq 
 |-  ( A e. NN -> A e. QQ )
35 34 3ad2ant2 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> A e. QQ )
36 nnq 
 |-  ( B e. NN -> B e. QQ )
37 36 3ad2ant3 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> B e. QQ )
38 qdivcl 
 |-  ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A / B ) e. QQ )
39 35 37 12 38 syl3anc 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( A / B ) e. QQ )
40 33 39 eqeltrd 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( sqrt ` ( ( A ^ 2 ) / ( B ^ 2 ) ) ) e. QQ )
41 fveq2 
 |-  ( ( ( A ^ 2 ) / ( B ^ 2 ) ) = D -> ( sqrt ` ( ( A ^ 2 ) / ( B ^ 2 ) ) ) = ( sqrt ` D ) )
42 41 eleq1d 
 |-  ( ( ( A ^ 2 ) / ( B ^ 2 ) ) = D -> ( ( sqrt ` ( ( A ^ 2 ) / ( B ^ 2 ) ) ) e. QQ <-> ( sqrt ` D ) e. QQ ) )
43 40 42 syl5ibcom 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( ( ( A ^ 2 ) / ( B ^ 2 ) ) = D -> ( sqrt ` D ) e. QQ ) )
44 16 43 sylbird 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( ( A ^ 2 ) = ( D x. ( B ^ 2 ) ) -> ( sqrt ` D ) e. QQ ) )
45 10 44 sylbid 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 0 -> ( sqrt ` D ) e. QQ ) )
46 45 necon3bd 
 |-  ( ( D e. NN /\ A e. NN /\ B e. NN ) -> ( -. ( sqrt ` D ) e. QQ -> ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) =/= 0 ) )
47 46 imp 
 |-  ( ( ( D e. NN /\ A e. NN /\ B e. NN ) /\ -. ( sqrt ` D ) e. QQ ) -> ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) =/= 0 )