Metamath Proof Explorer

Theorem pell1qrge1

Description: A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell1qrge1 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1QR ` D ) ) -> 1 <_ A )

Proof

Step Hyp Ref Expression
1 elpell1qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
2 1red 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 1 e. RR )
3 simplrl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> a e. NN0 )
4 3 nn0red 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> a e. RR )
5 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
6 5 ad3antrrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> D e. NN )
7 6 nnnn0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> D e. NN0 )
8 7 nn0red 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> D e. RR )
9 7 nn0ge0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ D )
10 8 9 resqrtcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( sqrt ` D ) e. RR )
11 simplrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> b e. NN0 )
12 11 nn0red 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> b e. RR )
13 10 12 remulcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( sqrt ` D ) x. b ) e. RR )
14 4 13 readdcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( a + ( ( sqrt ` D ) x. b ) ) e. RR )
15 2nn0 
 |-  2 e. NN0
16 15 a1i 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 2 e. NN0 )
17 11 16 nn0expcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( b ^ 2 ) e. NN0 )
18 7 17 nn0mulcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( D x. ( b ^ 2 ) ) e. NN0 )
19 18 nn0ge0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ ( D x. ( b ^ 2 ) ) )
20 18 nn0red 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( D x. ( b ^ 2 ) ) e. RR )
21 2 20 addge02d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( 0 <_ ( D x. ( b ^ 2 ) ) <-> 1 <_ ( ( D x. ( b ^ 2 ) ) + 1 ) ) )
22 19 21 mpbid 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 1 <_ ( ( D x. ( b ^ 2 ) ) + 1 ) )
23 sq1 
 |-  ( 1 ^ 2 ) = 1
24 23 a1i 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( 1 ^ 2 ) = 1 )
25 nn0cn 
 |-  ( a e. NN0 -> a e. CC )
26 25 ad2antrl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> a e. CC )
27 26 sqcld 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> ( a ^ 2 ) e. CC )
28 5 ad2antrr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> D e. NN )
29 28 nncnd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> D e. CC )
30 nn0cn 
 |-  ( b e. NN0 -> b e. CC )
31 30 ad2antll 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> b e. CC )
32 31 sqcld 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> ( b ^ 2 ) e. CC )
33 29 32 mulcld 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> ( D x. ( b ^ 2 ) ) e. CC )
34 1cnd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> 1 e. CC )
35 27 33 34 subaddd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> ( ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( D x. ( b ^ 2 ) ) + 1 ) = ( a ^ 2 ) ) )
36 35 biimpa 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( D x. ( b ^ 2 ) ) + 1 ) = ( a ^ 2 ) )
37 36 eqcomd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( a ^ 2 ) = ( ( D x. ( b ^ 2 ) ) + 1 ) )
38 22 24 37 3brtr4d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( 1 ^ 2 ) <_ ( a ^ 2 ) )
39 0le1 
 |-  0 <_ 1
40 39 a1i 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ 1 )
41 3 nn0ge0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ a )
42 2 4 40 41 le2sqd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( 1 <_ a <-> ( 1 ^ 2 ) <_ ( a ^ 2 ) ) )
43 38 42 mpbird 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 1 <_ a )
44 8 9 sqrtge0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ ( sqrt ` D ) )
45 11 nn0ge0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ b )
46 10 12 44 45 mulge0d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 0 <_ ( ( sqrt ` D ) x. b ) )
47 4 13 addge01d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( 0 <_ ( ( sqrt ` D ) x. b ) <-> a <_ ( a + ( ( sqrt ` D ) x. b ) ) ) )
48 46 47 mpbid 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> a <_ ( a + ( ( sqrt ` D ) x. b ) ) )
49 2 4 14 43 48 letrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 1 <_ ( a + ( ( sqrt ` D ) x. b ) ) )
50 49 adantrl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 1 <_ ( a + ( ( sqrt ` D ) x. b ) ) )
51 simprl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
52 50 51 breqtrrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 1 <_ A )
53 52 ex 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 1 <_ A ) )
54 53 rexlimdvva 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR ) -> ( E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> 1 <_ A ) )
55 54 expimpd 
 |-  ( D e. ( NN \ []NN ) -> ( ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 1 <_ A ) )
56 1 55 sylbid 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) -> 1 <_ A ) )
57 56 imp 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1QR ` D ) ) -> 1 <_ A )