Metamath Proof Explorer

Theorem pellfundgt1

Description: Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion pellfundgt1 
|- ( D e. ( NN \ []NN ) -> 1 < ( PellFund ` D ) )

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( D e. ( NN \ []NN ) -> 1 e. RR )
2 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
3 2 peano2nnd 
 |-  ( D e. ( NN \ []NN ) -> ( D + 1 ) e. NN )
4 3 nnrpd 
 |-  ( D e. ( NN \ []NN ) -> ( D + 1 ) e. RR+ )
5 4 rpsqrtcld 
 |-  ( D e. ( NN \ []NN ) -> ( sqrt ` ( D + 1 ) ) e. RR+ )
6 5 rpred 
 |-  ( D e. ( NN \ []NN ) -> ( sqrt ` ( D + 1 ) ) e. RR )
7 2 nnrpd 
 |-  ( D e. ( NN \ []NN ) -> D e. RR+ )
8 7 rpsqrtcld 
 |-  ( D e. ( NN \ []NN ) -> ( sqrt ` D ) e. RR+ )
9 8 rpred 
 |-  ( D e. ( NN \ []NN ) -> ( sqrt ` D ) e. RR )
10 6 9 readdcld 
 |-  ( D e. ( NN \ []NN ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) e. RR )
11 pellfundre 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR )
12 sqrt1 
 |-  ( sqrt ` 1 ) = 1
13 12 1 eqeltrid 
 |-  ( D e. ( NN \ []NN ) -> ( sqrt ` 1 ) e. RR )
14 13 13 readdcld 
 |-  ( D e. ( NN \ []NN ) -> ( ( sqrt ` 1 ) + ( sqrt ` 1 ) ) e. RR )
15 1lt2 
 |-  1 < 2
16 12 12 oveq12i 
 |-  ( ( sqrt ` 1 ) + ( sqrt ` 1 ) ) = ( 1 + 1 )
17 1p1e2 
 |-  ( 1 + 1 ) = 2
18 16 17 eqtri 
 |-  ( ( sqrt ` 1 ) + ( sqrt ` 1 ) ) = 2
19 15 18 breqtrri 
 |-  1 < ( ( sqrt ` 1 ) + ( sqrt ` 1 ) )
20 19 a1i 
 |-  ( D e. ( NN \ []NN ) -> 1 < ( ( sqrt ` 1 ) + ( sqrt ` 1 ) ) )
21 3 nnge1d 
 |-  ( D e. ( NN \ []NN ) -> 1 <_ ( D + 1 ) )
22 0le1 
 |-  0 <_ 1
23 22 a1i 
 |-  ( D e. ( NN \ []NN ) -> 0 <_ 1 )
24 2 nnred 
 |-  ( D e. ( NN \ []NN ) -> D e. RR )
25 peano2re 
 |-  ( D e. RR -> ( D + 1 ) e. RR )
26 24 25 syl 
 |-  ( D e. ( NN \ []NN ) -> ( D + 1 ) e. RR )
27 3 nnnn0d 
 |-  ( D e. ( NN \ []NN ) -> ( D + 1 ) e. NN0 )
28 27 nn0ge0d 
 |-  ( D e. ( NN \ []NN ) -> 0 <_ ( D + 1 ) )
29 1 23 26 28 sqrtled 
 |-  ( D e. ( NN \ []NN ) -> ( 1 <_ ( D + 1 ) <-> ( sqrt ` 1 ) <_ ( sqrt ` ( D + 1 ) ) ) )
30 21 29 mpbid 
 |-  ( D e. ( NN \ []NN ) -> ( sqrt ` 1 ) <_ ( sqrt ` ( D + 1 ) ) )
31 2 nnge1d 
 |-  ( D e. ( NN \ []NN ) -> 1 <_ D )
32 2 nnnn0d 
 |-  ( D e. ( NN \ []NN ) -> D e. NN0 )
33 32 nn0ge0d 
 |-  ( D e. ( NN \ []NN ) -> 0 <_ D )
34 1 23 24 33 sqrtled 
 |-  ( D e. ( NN \ []NN ) -> ( 1 <_ D <-> ( sqrt ` 1 ) <_ ( sqrt ` D ) ) )
35 31 34 mpbid 
 |-  ( D e. ( NN \ []NN ) -> ( sqrt ` 1 ) <_ ( sqrt ` D ) )
36 13 13 6 9 30 35 le2addd 
 |-  ( D e. ( NN \ []NN ) -> ( ( sqrt ` 1 ) + ( sqrt ` 1 ) ) <_ ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) )
37 1 14 10 20 36 ltletrd 
 |-  ( D e. ( NN \ []NN ) -> 1 < ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) )
38 pellfundge 
 |-  ( D e. ( NN \ []NN ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ ( PellFund ` D ) )
39 1 10 11 37 38 ltletrd 
 |-  ( D e. ( NN \ []NN ) -> 1 < ( PellFund ` D ) )