Metamath Proof Explorer

Theorem natlocalincr

Description: Global monotonicity on half-open range implies local monotonicity. Inference form. (Contributed by Ender Ting, 22-Nov-2024)

Ref Expression
Hypothesis natlocalincr.1 
|- A. k e. ( 0 ..^ T ) A. t e. ( 1 ..^ ( T + 1 ) ) ( k < t -> ( B ` k ) < ( B ` t ) )
Assertion natlocalincr 
|- A. k e. ( 0 ..^ T ) ( B ` k ) < ( B ` ( k + 1 ) )

Proof

Step Hyp Ref Expression
1 natlocalincr.1 
 |-  A. k e. ( 0 ..^ T ) A. t e. ( 1 ..^ ( T + 1 ) ) ( k < t -> ( B ` k ) < ( B ` t ) )
2 ovex 
 |-  ( k + 1 ) e. _V
3 2 isseti 
 |-  E. t t = ( k + 1 )
4 rsp 
 |-  ( A. t e. ( 1 ..^ ( T + 1 ) ) ( k < t -> ( B ` k ) < ( B ` t ) ) -> ( t e. ( 1 ..^ ( T + 1 ) ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) )
5 4 ralimi 
 |-  ( A. k e. ( 0 ..^ T ) A. t e. ( 1 ..^ ( T + 1 ) ) ( k < t -> ( B ` k ) < ( B ` t ) ) -> A. k e. ( 0 ..^ T ) ( t e. ( 1 ..^ ( T + 1 ) ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) )
6 1z 
 |-  1 e. ZZ
7 fzoaddel 
 |-  ( ( k e. ( 0 ..^ T ) /\ 1 e. ZZ ) -> ( k + 1 ) e. ( ( 0 + 1 ) ..^ ( T + 1 ) ) )
8 6 7 mpan2 
 |-  ( k e. ( 0 ..^ T ) -> ( k + 1 ) e. ( ( 0 + 1 ) ..^ ( T + 1 ) ) )
9 0p1e1 
 |-  ( 0 + 1 ) = 1
10 9 oveq1i 
 |-  ( ( 0 + 1 ) ..^ ( T + 1 ) ) = ( 1 ..^ ( T + 1 ) )
11 8 10 eleqtrdi 
 |-  ( k e. ( 0 ..^ T ) -> ( k + 1 ) e. ( 1 ..^ ( T + 1 ) ) )
12 eleq1 
 |-  ( t = ( k + 1 ) -> ( t e. ( 1 ..^ ( T + 1 ) ) <-> ( k + 1 ) e. ( 1 ..^ ( T + 1 ) ) ) )
13 11 12 syl5ibrcom 
 |-  ( k e. ( 0 ..^ T ) -> ( t = ( k + 1 ) -> t e. ( 1 ..^ ( T + 1 ) ) ) )
14 13 imim1d 
 |-  ( k e. ( 0 ..^ T ) -> ( ( t e. ( 1 ..^ ( T + 1 ) ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) -> ( t = ( k + 1 ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) ) )
15 14 ralimia 
 |-  ( A. k e. ( 0 ..^ T ) ( t e. ( 1 ..^ ( T + 1 ) ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) -> A. k e. ( 0 ..^ T ) ( t = ( k + 1 ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) )
16 1 5 15 mp2b 
 |-  A. k e. ( 0 ..^ T ) ( t = ( k + 1 ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) )
17 elfzoelz 
 |-  ( k e. ( 0 ..^ T ) -> k e. ZZ )
18 zre 
 |-  ( k e. ZZ -> k e. RR )
19 ltp1 
 |-  ( k e. RR -> k < ( k + 1 ) )
20 17 18 19 3syl 
 |-  ( k e. ( 0 ..^ T ) -> k < ( k + 1 ) )
21 breq2 
 |-  ( t = ( k + 1 ) -> ( k < t <-> k < ( k + 1 ) ) )
22 20 21 syl5ibrcom 
 |-  ( k e. ( 0 ..^ T ) -> ( t = ( k + 1 ) -> k < t ) )
23 ax-2 
 |-  ( ( t = ( k + 1 ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) -> ( ( t = ( k + 1 ) -> k < t ) -> ( t = ( k + 1 ) -> ( B ` k ) < ( B ` t ) ) ) )
24 22 23 syl5com 
 |-  ( k e. ( 0 ..^ T ) -> ( ( t = ( k + 1 ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) -> ( t = ( k + 1 ) -> ( B ` k ) < ( B ` t ) ) ) )
25 24 ralimia 
 |-  ( A. k e. ( 0 ..^ T ) ( t = ( k + 1 ) -> ( k < t -> ( B ` k ) < ( B ` t ) ) ) -> A. k e. ( 0 ..^ T ) ( t = ( k + 1 ) -> ( B ` k ) < ( B ` t ) ) )
26 fveq2 
 |-  ( t = ( k + 1 ) -> ( B ` t ) = ( B ` ( k + 1 ) ) )
27 26 breq2d 
 |-  ( t = ( k + 1 ) -> ( ( B ` k ) < ( B ` t ) <-> ( B ` k ) < ( B ` ( k + 1 ) ) ) )
28 27 biimpd 
 |-  ( t = ( k + 1 ) -> ( ( B ` k ) < ( B ` t ) -> ( B ` k ) < ( B ` ( k + 1 ) ) ) )
29 28 a2i 
 |-  ( ( t = ( k + 1 ) -> ( B ` k ) < ( B ` t ) ) -> ( t = ( k + 1 ) -> ( B ` k ) < ( B ` ( k + 1 ) ) ) )
30 29 ralimi 
 |-  ( A. k e. ( 0 ..^ T ) ( t = ( k + 1 ) -> ( B ` k ) < ( B ` t ) ) -> A. k e. ( 0 ..^ T ) ( t = ( k + 1 ) -> ( B ` k ) < ( B ` ( k + 1 ) ) ) )
31 16 25 30 mp2b 
 |-  A. k e. ( 0 ..^ T ) ( t = ( k + 1 ) -> ( B ` k ) < ( B ` ( k + 1 ) ) )
32 31 rspec 
 |-  ( k e. ( 0 ..^ T ) -> ( t = ( k + 1 ) -> ( B ` k ) < ( B ` ( k + 1 ) ) ) )
33 32 eximdv 
 |-  ( k e. ( 0 ..^ T ) -> ( E. t t = ( k + 1 ) -> E. t ( B ` k ) < ( B ` ( k + 1 ) ) ) )
34 3 33 mpi 
 |-  ( k e. ( 0 ..^ T ) -> E. t ( B ` k ) < ( B ` ( k + 1 ) ) )
35 ax5e 
 |-  ( E. t ( B ` k ) < ( B ` ( k + 1 ) ) -> ( B ` k ) < ( B ` ( k + 1 ) ) )
36 34 35 syl 
 |-  ( k e. ( 0 ..^ T ) -> ( B ` k ) < ( B ` ( k + 1 ) ) )
37 36 rgen 
 |-  A. k e. ( 0 ..^ T ) ( B ` k ) < ( B ` ( k + 1 ) )