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 ⊢∀k∈0..^T∀t∈1..^T+1k<t→B⁡k<B⁡t
Assertion natlocalincr ⊢∀k∈0..^TB⁡k<B⁡k+1

Proof

Step Hyp Ref Expression
1 natlocalincr.1 ⊢∀k∈0..^T∀t∈1..^T+1k<t→B⁡k<B⁡t
2 ovex ⊢k+1∈V
3 2 isseti ⊢∃tt=k+1
4 rsp ⊢∀t∈1..^T+1k<t→B⁡k<B⁡t→t∈1..^T+1→k<t→B⁡k<B⁡t
5 4 ralimi ⊢∀k∈0..^T∀t∈1..^T+1k<t→B⁡k<B⁡t→∀k∈0..^Tt∈1..^T+1→k<t→B⁡k<B⁡t
6 1z ⊢1∈ℤ
7 fzoaddel ⊢k∈0..^T∧1∈ℤ→k+1∈0+1..^T+1
8 6 7 mpan2 ⊢k∈0..^T→k+1∈0+1..^T+1
9 0p1e1 ⊢0+1=1
10 9 oveq1i ⊢0+1..^T+1=1..^T+1
11 8 10 eleqtrdi ⊢k∈0..^T→k+1∈1..^T+1
12 eleq1 ⊢t=k+1→t∈1..^T+1↔k+1∈1..^T+1
13 11 12 syl5ibrcom ⊢k∈0..^T→t=k+1→t∈1..^T+1
14 13 imim1d ⊢k∈0..^T→t∈1..^T+1→k<t→B⁡k<B⁡t→t=k+1→k<t→B⁡k<B⁡t
15 14 ralimia ⊢∀k∈0..^Tt∈1..^T+1→k<t→B⁡k<B⁡t→∀k∈0..^Tt=k+1→k<t→B⁡k<B⁡t
16 1 5 15 mp2b ⊢∀k∈0..^Tt=k+1→k<t→B⁡k<B⁡t
17 elfzoelz ⊢k∈0..^T→k∈ℤ
18 zre ⊢k∈ℤ→k∈ℝ
19 ltp1 ⊢k∈ℝ→k<k+1
20 17 18 19 3syl ⊢k∈0..^T→k<k+1
21 breq2 ⊢t=k+1→k<t↔k<k+1
22 20 21 syl5ibrcom ⊢k∈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∈0..^T→t=k+1→k<t→B⁡k<B⁡t→t=k+1→B⁡k<B⁡t
25 24 ralimia ⊢∀k∈0..^Tt=k+1→k<t→B⁡k<B⁡t→∀k∈0..^Tt=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 ⊢∀k∈0..^Tt=k+1→B⁡k<B⁡t→∀k∈0..^Tt=k+1→B⁡k<B⁡k+1
31 16 25 30 mp2b ⊢∀k∈0..^Tt=k+1→B⁡k<B⁡k+1
32 31 rspec ⊢k∈0..^T→t=k+1→B⁡k<B⁡k+1
33 32 eximdv ⊢k∈0..^T→∃tt=k+1→∃tB⁡k<B⁡k+1
34 3 33 mpi ⊢k∈0..^T→∃tB⁡k<B⁡k+1
35 ax5e ⊢∃tB⁡k<B⁡k+1→B⁡k<B⁡k+1
36 34 35 syl ⊢k∈0..^T→B⁡k<B⁡k+1
37 36 rgen ⊢∀k∈0..^TB⁡k<B⁡k+1