Metamath Proof Explorer

Theorem pell14qrgapw

Description: Positive Pell solutions are bounded away from 1, with a friendlier bound. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrgapw 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 2 < A )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 2 e. RR )
3 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
4 3 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> D e. NN )
5 4 nnrpd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> D e. RR+ )
6 1rp 
 |-  1 e. RR+
7 6 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 1 e. RR+ )
8 5 7 rpaddcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( D + 1 ) e. RR+ )
9 8 rpsqrtcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( sqrt ` ( D + 1 ) ) e. RR+ )
10 9 rpred 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( sqrt ` ( D + 1 ) ) e. RR )
11 5 rpsqrtcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( sqrt ` D ) e. RR+ )
12 11 rpred 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( sqrt ` D ) e. RR )
13 10 12 readdcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) e. RR )
14 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
15 14 3adant3 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> A e. RR )
16 df-2 
 |-  2 = ( 1 + 1 )
17 1red 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 1 e. RR )
18 4 nnred 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> D e. RR )
19 peano2re 
 |-  ( D e. RR -> ( D + 1 ) e. RR )
20 18 19 syl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( D + 1 ) e. RR )
21 4 nnge1d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 1 <_ D )
22 18 ltp1d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> D < ( D + 1 ) )
23 17 18 20 21 22 lelttrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 1 < ( D + 1 ) )
24 sq1 
 |-  ( 1 ^ 2 ) = 1
25 24 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( 1 ^ 2 ) = 1 )
26 4 nncnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> D e. CC )
27 peano2cn 
 |-  ( D e. CC -> ( D + 1 ) e. CC )
28 26 27 syl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( D + 1 ) e. CC )
29 28 sqsqrtd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( ( sqrt ` ( D + 1 ) ) ^ 2 ) = ( D + 1 ) )
30 23 25 29 3brtr4d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( 1 ^ 2 ) < ( ( sqrt ` ( D + 1 ) ) ^ 2 ) )
31 0le1 
 |-  0 <_ 1
32 31 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 0 <_ 1 )
33 9 rpge0d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 0 <_ ( sqrt ` ( D + 1 ) ) )
34 17 10 32 33 lt2sqd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( 1 < ( sqrt ` ( D + 1 ) ) <-> ( 1 ^ 2 ) < ( ( sqrt ` ( D + 1 ) ) ^ 2 ) ) )
35 30 34 mpbird 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 1 < ( sqrt ` ( D + 1 ) ) )
36 26 sqsqrtd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( ( sqrt ` D ) ^ 2 ) = D )
37 21 25 36 3brtr4d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( 1 ^ 2 ) <_ ( ( sqrt ` D ) ^ 2 ) )
38 11 rpge0d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 0 <_ ( sqrt ` D ) )
39 17 12 32 38 le2sqd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( 1 <_ ( sqrt ` D ) <-> ( 1 ^ 2 ) <_ ( ( sqrt ` D ) ^ 2 ) ) )
40 37 39 mpbird 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 1 <_ ( sqrt ` D ) )
41 17 17 10 12 35 40 ltleaddd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( 1 + 1 ) < ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) )
42 16 41 eqbrtrid 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 2 < ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) )
43 pell14qrgap 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A )
44 2 13 15 42 43 ltletrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 2 < A )