Metamath Proof Explorer

Theorem natglobalincr

Description: Local monotonicity on half-open integer range implies global monotonicity. Inference form. (Contributed by Ender Ting, 23-Nov-2024)

Ref Expression
Hypotheses natglobalincr.1 
|- A. k e. ( 0 ..^ T ) ( B ` k ) < ( B ` ( k + 1 ) )
natglobalincr.2 
|- T e. ZZ
Assertion natglobalincr 
|- A. k e. ( 0 ..^ T ) A. t e. ( ( k + 1 ) ... T ) ( B ` k ) < ( B ` t )

Proof

Step Hyp Ref Expression
1 natglobalincr.1 
 |-  A. k e. ( 0 ..^ T ) ( B ` k ) < ( B ` ( k + 1 ) )
2 natglobalincr.2 
 |-  T e. ZZ
3 elfzoelz 
 |-  ( k e. ( 0 ..^ T ) -> k e. ZZ )
4 3 peano2zd 
 |-  ( k e. ( 0 ..^ T ) -> ( k + 1 ) e. ZZ )
5 elfz1 
 |-  ( ( ( k + 1 ) e. ZZ /\ T e. ZZ ) -> ( t e. ( ( k + 1 ) ... T ) <-> ( t e. ZZ /\ ( k + 1 ) <_ t /\ t <_ T ) ) )
6 4 2 5 sylancl 
 |-  ( k e. ( 0 ..^ T ) -> ( t e. ( ( k + 1 ) ... T ) <-> ( t e. ZZ /\ ( k + 1 ) <_ t /\ t <_ T ) ) )
7 fveq2 
 |-  ( a = ( k + 1 ) -> ( B ` a ) = ( B ` ( k + 1 ) ) )
8 7 breq2d 
 |-  ( a = ( k + 1 ) -> ( ( B ` k ) < ( B ` a ) <-> ( B ` k ) < ( B ` ( k + 1 ) ) ) )
9 fveq2 
 |-  ( a = b -> ( B ` a ) = ( B ` b ) )
10 9 breq2d 
 |-  ( a = b -> ( ( B ` k ) < ( B ` a ) <-> ( B ` k ) < ( B ` b ) ) )
11 fveq2 
 |-  ( a = ( b + 1 ) -> ( B ` a ) = ( B ` ( b + 1 ) ) )
12 11 breq2d 
 |-  ( a = ( b + 1 ) -> ( ( B ` k ) < ( B ` a ) <-> ( B ` k ) < ( B ` ( b + 1 ) ) ) )
13 fveq2 
 |-  ( a = t -> ( B ` a ) = ( B ` t ) )
14 13 breq2d 
 |-  ( a = t -> ( ( B ` k ) < ( B ` a ) <-> ( B ` k ) < ( B ` t ) ) )
15 1 rspec 
 |-  ( k e. ( 0 ..^ T ) -> ( B ` k ) < ( B ` ( k + 1 ) ) )
16 df-br 
 |-  ( ( B ` k ) < ( B ` b ) <-> <. ( B ` k ) , ( B ` b ) >. e. < )
17 ltrelxr 
 |-  < C_ ( RR* X. RR* )
18 17 sseli 
 |-  ( <. ( B ` k ) , ( B ` b ) >. e. < -> <. ( B ` k ) , ( B ` b ) >. e. ( RR* X. RR* ) )
19 16 18 sylbi 
 |-  ( ( B ` k ) < ( B ` b ) -> <. ( B ` k ) , ( B ` b ) >. e. ( RR* X. RR* ) )
20 opelxp1 
 |-  ( <. ( B ` k ) , ( B ` b ) >. e. ( RR* X. RR* ) -> ( B ` k ) e. RR* )
21 19 20 syl 
 |-  ( ( B ` k ) < ( B ` b ) -> ( B ` k ) e. RR* )
22 21 3ad2ant3 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( B ` k ) e. RR* )
23 opelxp2 
 |-  ( <. ( B ` k ) , ( B ` b ) >. e. ( RR* X. RR* ) -> ( B ` b ) e. RR* )
24 19 23 syl 
 |-  ( ( B ` k ) < ( B ` b ) -> ( B ` b ) e. RR* )
25 24 3ad2ant3 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( B ` b ) e. RR* )
26 0red 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> 0 e. RR )
27 simp1 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> k e. ( 0 ..^ T ) )
28 zre 
 |-  ( k e. ZZ -> k e. RR )
29 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
30 27 3 28 29 4syl 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( k + 1 ) e. RR )
31 simp21 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> b e. ZZ )
32 31 zred 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> b e. RR )
33 elfzole1 
 |-  ( k e. ( 0 ..^ T ) -> 0 <_ k )
34 28 ltp1d 
 |-  ( k e. ZZ -> k < ( k + 1 ) )
35 3 34 syl 
 |-  ( k e. ( 0 ..^ T ) -> k < ( k + 1 ) )
36 0red 
 |-  ( k e. RR -> 0 e. RR )
37 id 
 |-  ( k e. RR -> k e. RR )
38 36 37 29 3jca 
 |-  ( k e. RR -> ( 0 e. RR /\ k e. RR /\ ( k + 1 ) e. RR ) )
39 leltletr 
 |-  ( ( 0 e. RR /\ k e. RR /\ ( k + 1 ) e. RR ) -> ( ( 0 <_ k /\ k < ( k + 1 ) ) -> 0 <_ ( k + 1 ) ) )
40 3 28 38 39 4syl 
 |-  ( k e. ( 0 ..^ T ) -> ( ( 0 <_ k /\ k < ( k + 1 ) ) -> 0 <_ ( k + 1 ) ) )
41 33 35 40 mp2and 
 |-  ( k e. ( 0 ..^ T ) -> 0 <_ ( k + 1 ) )
42 41 3ad2ant1 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> 0 <_ ( k + 1 ) )
43 simp22 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( k + 1 ) <_ b )
44 26 30 32 42 43 letrd 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> 0 <_ b )
45 simp23 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> b < T )
46 0zd 
 |-  ( b e. ZZ -> 0 e. ZZ )
47 2 a1i 
 |-  ( b e. ZZ -> T e. ZZ )
48 elfzo 
 |-  ( ( b e. ZZ /\ 0 e. ZZ /\ T e. ZZ ) -> ( b e. ( 0 ..^ T ) <-> ( 0 <_ b /\ b < T ) ) )
49 46 47 48 mpd3an23 
 |-  ( b e. ZZ -> ( b e. ( 0 ..^ T ) <-> ( 0 <_ b /\ b < T ) ) )
50 fveq2 
 |-  ( k = b -> ( B ` k ) = ( B ` b ) )
51 fvoveq1 
 |-  ( k = b -> ( B ` ( k + 1 ) ) = ( B ` ( b + 1 ) ) )
52 50 51 breq12d 
 |-  ( k = b -> ( ( B ` k ) < ( B ` ( k + 1 ) ) <-> ( B ` b ) < ( B ` ( b + 1 ) ) ) )
53 52 1 vtoclri 
 |-  ( b e. ( 0 ..^ T ) -> ( B ` b ) < ( B ` ( b + 1 ) ) )
54 49 53 biimtrrdi 
 |-  ( b e. ZZ -> ( ( 0 <_ b /\ b < T ) -> ( B ` b ) < ( B ` ( b + 1 ) ) ) )
55 31 54 syl 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( ( 0 <_ b /\ b < T ) -> ( B ` b ) < ( B ` ( b + 1 ) ) ) )
56 44 45 55 mp2and 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( B ` b ) < ( B ` ( b + 1 ) ) )
57 df-br 
 |-  ( ( B ` b ) < ( B ` ( b + 1 ) ) <-> <. ( B ` b ) , ( B ` ( b + 1 ) ) >. e. < )
58 17 sseli 
 |-  ( <. ( B ` b ) , ( B ` ( b + 1 ) ) >. e. < -> <. ( B ` b ) , ( B ` ( b + 1 ) ) >. e. ( RR* X. RR* ) )
59 57 58 sylbi 
 |-  ( ( B ` b ) < ( B ` ( b + 1 ) ) -> <. ( B ` b ) , ( B ` ( b + 1 ) ) >. e. ( RR* X. RR* ) )
60 opelxp2 
 |-  ( <. ( B ` b ) , ( B ` ( b + 1 ) ) >. e. ( RR* X. RR* ) -> ( B ` ( b + 1 ) ) e. RR* )
61 56 59 60 3syl 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( B ` ( b + 1 ) ) e. RR* )
62 simp3 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( B ` k ) < ( B ` b ) )
63 22 25 61 62 56 xrlttrd 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) < ( B ` b ) ) -> ( B ` k ) < ( B ` ( b + 1 ) ) )
64 elfzoel2 
 |-  ( k e. ( 0 ..^ T ) -> T e. ZZ )
65 elfzop1le2 
 |-  ( k e. ( 0 ..^ T ) -> ( k + 1 ) <_ T )
66 8 10 12 14 15 63 4 64 65 fzindd 
 |-  ( ( k e. ( 0 ..^ T ) /\ ( t e. ZZ /\ ( k + 1 ) <_ t /\ t <_ T ) ) -> ( B ` k ) < ( B ` t ) )
67 6 66 sylbida 
 |-  ( ( k e. ( 0 ..^ T ) /\ t e. ( ( k + 1 ) ... T ) ) -> ( B ` k ) < ( B ` t ) )
68 67 rgen2 
 |-  A. k e. ( 0 ..^ T ) A. t e. ( ( k + 1 ) ... T ) ( B ` k ) < ( B ` t )