Metamath Proof Explorer

Theorem qabvle

Description: By using induction on N , we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q 
|- Q = ( CCfld |`s QQ )
qabsabv.a 
|- A = ( AbsVal ` Q )
Assertion qabvle 
|- ( ( F e. A /\ N e. NN0 ) -> ( F ` N ) <_ N )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qabsabv.a 
 |-  A = ( AbsVal ` Q )
3 fveq2 
 |-  ( k = 0 -> ( F ` k ) = ( F ` 0 ) )
4 id 
 |-  ( k = 0 -> k = 0 )
5 3 4 breq12d 
 |-  ( k = 0 -> ( ( F ` k ) <_ k <-> ( F ` 0 ) <_ 0 ) )
6 5 imbi2d 
 |-  ( k = 0 -> ( ( F e. A -> ( F ` k ) <_ k ) <-> ( F e. A -> ( F ` 0 ) <_ 0 ) ) )
7 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
8 id 
 |-  ( k = n -> k = n )
9 7 8 breq12d 
 |-  ( k = n -> ( ( F ` k ) <_ k <-> ( F ` n ) <_ n ) )
10 9 imbi2d 
 |-  ( k = n -> ( ( F e. A -> ( F ` k ) <_ k ) <-> ( F e. A -> ( F ` n ) <_ n ) ) )
11 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
12 id 
 |-  ( k = ( n + 1 ) -> k = ( n + 1 ) )
13 11 12 breq12d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) <_ k <-> ( F ` ( n + 1 ) ) <_ ( n + 1 ) ) )
14 13 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( F e. A -> ( F ` k ) <_ k ) <-> ( F e. A -> ( F ` ( n + 1 ) ) <_ ( n + 1 ) ) ) )
15 fveq2 
 |-  ( k = N -> ( F ` k ) = ( F ` N ) )
16 id 
 |-  ( k = N -> k = N )
17 15 16 breq12d 
 |-  ( k = N -> ( ( F ` k ) <_ k <-> ( F ` N ) <_ N ) )
18 17 imbi2d 
 |-  ( k = N -> ( ( F e. A -> ( F ` k ) <_ k ) <-> ( F e. A -> ( F ` N ) <_ N ) ) )
19 1 qrng0 
 |-  0 = ( 0g ` Q )
20 2 19 abv0 
 |-  ( F e. A -> ( F ` 0 ) = 0 )
21 0le0 
 |-  0 <_ 0
22 20 21 eqbrtrdi 
 |-  ( F e. A -> ( F ` 0 ) <_ 0 )
23 nn0p1nn 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN )
24 23 ad2antrl 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( n + 1 ) e. NN )
25 nnq 
 |-  ( ( n + 1 ) e. NN -> ( n + 1 ) e. QQ )
26 24 25 syl 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( n + 1 ) e. QQ )
27 1 qrngbas 
 |-  QQ = ( Base ` Q )
28 2 27 abvcl 
 |-  ( ( F e. A /\ ( n + 1 ) e. QQ ) -> ( F ` ( n + 1 ) ) e. RR )
29 26 28 syldan 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( F ` ( n + 1 ) ) e. RR )
30 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
31 30 ad2antrl 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> n e. ZZ )
32 zq 
 |-  ( n e. ZZ -> n e. QQ )
33 31 32 syl 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> n e. QQ )
34 2 27 abvcl 
 |-  ( ( F e. A /\ n e. QQ ) -> ( F ` n ) e. RR )
35 33 34 syldan 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( F ` n ) e. RR )
36 peano2re 
 |-  ( ( F ` n ) e. RR -> ( ( F ` n ) + 1 ) e. RR )
37 35 36 syl 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( ( F ` n ) + 1 ) e. RR )
38 31 zred 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> n e. RR )
39 peano2re 
 |-  ( n e. RR -> ( n + 1 ) e. RR )
40 38 39 syl 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( n + 1 ) e. RR )
41 simpl 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> F e. A )
42 1z 
 |-  1 e. ZZ
43 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
44 42 43 mp1i 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> 1 e. QQ )
45 qex 
 |-  QQ e. _V
46 cnfldadd 
 |-  + = ( +g ` CCfld )
47 1 46 ressplusg 
 |-  ( QQ e. _V -> + = ( +g ` Q ) )
48 45 47 ax-mp 
 |-  + = ( +g ` Q )
49 2 27 48 abvtri 
 |-  ( ( F e. A /\ n e. QQ /\ 1 e. QQ ) -> ( F ` ( n + 1 ) ) <_ ( ( F ` n ) + ( F ` 1 ) ) )
50 41 33 44 49 syl3anc 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( F ` ( n + 1 ) ) <_ ( ( F ` n ) + ( F ` 1 ) ) )
51 ax-1ne0 
 |-  1 =/= 0
52 1 qrng1 
 |-  1 = ( 1r ` Q )
53 2 52 19 abv1z 
 |-  ( ( F e. A /\ 1 =/= 0 ) -> ( F ` 1 ) = 1 )
54 51 53 mpan2 
 |-  ( F e. A -> ( F ` 1 ) = 1 )
55 54 adantr 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( F ` 1 ) = 1 )
56 55 oveq2d 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( ( F ` n ) + ( F ` 1 ) ) = ( ( F ` n ) + 1 ) )
57 50 56 breqtrd 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( F ` ( n + 1 ) ) <_ ( ( F ` n ) + 1 ) )
58 1red 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> 1 e. RR )
59 simprr 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( F ` n ) <_ n )
60 35 38 58 59 leadd1dd 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( ( F ` n ) + 1 ) <_ ( n + 1 ) )
61 29 37 40 57 60 letrd 
 |-  ( ( F e. A /\ ( n e. NN0 /\ ( F ` n ) <_ n ) ) -> ( F ` ( n + 1 ) ) <_ ( n + 1 ) )
62 61 expr 
 |-  ( ( F e. A /\ n e. NN0 ) -> ( ( F ` n ) <_ n -> ( F ` ( n + 1 ) ) <_ ( n + 1 ) ) )
63 62 expcom 
 |-  ( n e. NN0 -> ( F e. A -> ( ( F ` n ) <_ n -> ( F ` ( n + 1 ) ) <_ ( n + 1 ) ) ) )
64 63 a2d 
 |-  ( n e. NN0 -> ( ( F e. A -> ( F ` n ) <_ n ) -> ( F e. A -> ( F ` ( n + 1 ) ) <_ ( n + 1 ) ) ) )
65 6 10 14 18 22 64 nn0ind 
 |-  ( N e. NN0 -> ( F e. A -> ( F ` N ) <_ N ) )
66 65 impcom 
 |-  ( ( F e. A /\ N e. NN0 ) -> ( F ` N ) <_ N )