Metamath Proof Explorer

Theorem pellqrex

Description: There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellqrex 
|- ( D e. ( NN \ []NN ) -> E. x e. ( Pell1QR ` D ) 1 < x )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
2 eldifn 
 |-  ( D e. ( NN \ []NN ) -> -. D e. []NN )
3 1 anim1i 
 |-  ( ( D e. ( NN \ []NN ) /\ ( sqrt ` D ) e. QQ ) -> ( D e. NN /\ ( sqrt ` D ) e. QQ ) )
4 fveq2 
 |-  ( a = D -> ( sqrt ` a ) = ( sqrt ` D ) )
5 4 eleq1d 
 |-  ( a = D -> ( ( sqrt ` a ) e. QQ <-> ( sqrt ` D ) e. QQ ) )
6 df-squarenn 
 |-  []NN = { a e. NN | ( sqrt ` a ) e. QQ }
7 5 6 elrab2 
 |-  ( D e. []NN <-> ( D e. NN /\ ( sqrt ` D ) e. QQ ) )
8 3 7 sylibr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( sqrt ` D ) e. QQ ) -> D e. []NN )
9 2 8 mtand 
 |-  ( D e. ( NN \ []NN ) -> -. ( sqrt ` D ) e. QQ )
10 pellex 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> E. c e. NN E. d e. NN ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 )
11 1 9 10 syl2anc 
 |-  ( D e. ( NN \ []NN ) -> E. c e. NN E. d e. NN ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 )
12 simpll 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) -> D e. ( NN \ []NN ) )
13 nnnn0 
 |-  ( c e. NN -> c e. NN0 )
14 13 adantr 
 |-  ( ( c e. NN /\ d e. NN ) -> c e. NN0 )
15 14 ad2antlr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) -> c e. NN0 )
16 nnnn0 
 |-  ( d e. NN -> d e. NN0 )
17 16 adantl 
 |-  ( ( c e. NN /\ d e. NN ) -> d e. NN0 )
18 17 ad2antlr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) -> d e. NN0 )
19 simpr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) -> ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 )
20 pellqrexplicit 
 |-  ( ( ( D e. ( NN \ []NN ) /\ c e. NN0 /\ d e. NN0 ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) -> ( c + ( ( sqrt ` D ) x. d ) ) e. ( Pell1QR ` D ) )
21 12 15 18 19 20 syl31anc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) -> ( c + ( ( sqrt ` D ) x. d ) ) e. ( Pell1QR ` D ) )
22 1re 
 |-  1 e. RR
23 22 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> 1 e. RR )
24 22 22 readdcli 
 |-  ( 1 + 1 ) e. RR
25 24 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( 1 + 1 ) e. RR )
26 nnre 
 |-  ( c e. NN -> c e. RR )
27 26 ad2antrl 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> c e. RR )
28 1 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> D e. NN )
29 28 nnrpd 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> D e. RR+ )
30 29 rpsqrtcld 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( sqrt ` D ) e. RR+ )
31 30 rpred 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( sqrt ` D ) e. RR )
32 nnre 
 |-  ( d e. NN -> d e. RR )
33 32 ad2antll 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> d e. RR )
34 31 33 remulcld 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( ( sqrt ` D ) x. d ) e. RR )
35 27 34 readdcld 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( c + ( ( sqrt ` D ) x. d ) ) e. RR )
36 22 ltp1i 
 |-  1 < ( 1 + 1 )
37 36 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> 1 < ( 1 + 1 ) )
38 nnge1 
 |-  ( c e. NN -> 1 <_ c )
39 38 ad2antrl 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> 1 <_ c )
40 1t1e1 
 |-  ( 1 x. 1 ) = 1
41 nnge1 
 |-  ( D e. NN -> 1 <_ D )
42 sq1 
 |-  ( 1 ^ 2 ) = 1
43 42 a1i 
 |-  ( D e. NN -> ( 1 ^ 2 ) = 1 )
44 nncn 
 |-  ( D e. NN -> D e. CC )
45 44 sqsqrtd 
 |-  ( D e. NN -> ( ( sqrt ` D ) ^ 2 ) = D )
46 41 43 45 3brtr4d 
 |-  ( D e. NN -> ( 1 ^ 2 ) <_ ( ( sqrt ` D ) ^ 2 ) )
47 22 a1i 
 |-  ( D e. NN -> 1 e. RR )
48 nnrp 
 |-  ( D e. NN -> D e. RR+ )
49 48 rpsqrtcld 
 |-  ( D e. NN -> ( sqrt ` D ) e. RR+ )
50 49 rpred 
 |-  ( D e. NN -> ( sqrt ` D ) e. RR )
51 0le1 
 |-  0 <_ 1
52 51 a1i 
 |-  ( D e. NN -> 0 <_ 1 )
53 49 rpge0d 
 |-  ( D e. NN -> 0 <_ ( sqrt ` D ) )
54 47 50 52 53 le2sqd 
 |-  ( D e. NN -> ( 1 <_ ( sqrt ` D ) <-> ( 1 ^ 2 ) <_ ( ( sqrt ` D ) ^ 2 ) ) )
55 46 54 mpbird 
 |-  ( D e. NN -> 1 <_ ( sqrt ` D ) )
56 28 55 syl 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> 1 <_ ( sqrt ` D ) )
57 nnge1 
 |-  ( d e. NN -> 1 <_ d )
58 57 ad2antll 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> 1 <_ d )
59 23 51 jctir 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( 1 e. RR /\ 0 <_ 1 ) )
60 lemul12a 
 |-  ( ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( sqrt ` D ) e. RR ) /\ ( ( 1 e. RR /\ 0 <_ 1 ) /\ d e. RR ) ) -> ( ( 1 <_ ( sqrt ` D ) /\ 1 <_ d ) -> ( 1 x. 1 ) <_ ( ( sqrt ` D ) x. d ) ) )
61 59 31 59 33 60 syl22anc 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( ( 1 <_ ( sqrt ` D ) /\ 1 <_ d ) -> ( 1 x. 1 ) <_ ( ( sqrt ` D ) x. d ) ) )
62 56 58 61 mp2and 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( 1 x. 1 ) <_ ( ( sqrt ` D ) x. d ) )
63 40 62 eqbrtrrid 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> 1 <_ ( ( sqrt ` D ) x. d ) )
64 23 23 27 34 39 63 le2addd 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( 1 + 1 ) <_ ( c + ( ( sqrt ` D ) x. d ) ) )
65 23 25 35 37 64 ltletrd 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> 1 < ( c + ( ( sqrt ` D ) x. d ) ) )
66 65 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) -> 1 < ( c + ( ( sqrt ` D ) x. d ) ) )
67 breq2 
 |-  ( x = ( c + ( ( sqrt ` D ) x. d ) ) -> ( 1 < x <-> 1 < ( c + ( ( sqrt ` D ) x. d ) ) ) )
68 67 rspcev 
 |-  ( ( ( c + ( ( sqrt ` D ) x. d ) ) e. ( Pell1QR ` D ) /\ 1 < ( c + ( ( sqrt ` D ) x. d ) ) ) -> E. x e. ( Pell1QR ` D ) 1 < x )
69 21 66 68 syl2anc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) -> E. x e. ( Pell1QR ` D ) 1 < x )
70 69 ex 
 |-  ( ( D e. ( NN \ []NN ) /\ ( c e. NN /\ d e. NN ) ) -> ( ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 -> E. x e. ( Pell1QR ` D ) 1 < x ) )
71 70 rexlimdvva 
 |-  ( D e. ( NN \ []NN ) -> ( E. c e. NN E. d e. NN ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 -> E. x e. ( Pell1QR ` D ) 1 < x ) )
72 11 71 mpd 
 |-  ( D e. ( NN \ []NN ) -> E. x e. ( Pell1QR ` D ) 1 < x )