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

Proof

Step Hyp Ref Expression
1 natlocalincr.1 ⊢ ∀ k ∈ 0 ..^ T ∀ t ∈ 1 ..^ T + 1 k < t → B ⁡ k < B ⁡ t
2 ovex ⊢ k + 1 ∈ V
3 2 isseti ⊢ ∃ t t = k + 1
4 rsp ⊢ ∀ t ∈ 1 ..^ T + 1 k < t → B ⁡ k < B ⁡ t → t ∈ 1 ..^ T + 1 → k < t → B ⁡ k < B ⁡ t
5 4 ralimi ⊢ ∀ k ∈ 0 ..^ T ∀ t ∈ 1 ..^ T + 1 k < t → B ⁡ k < B ⁡ t → ∀ k ∈ 0 ..^ T t ∈ 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 ..^ T t ∈ 1 ..^ T + 1 → k < t → B ⁡ k < B ⁡ t → ∀ k ∈ 0 ..^ T t = k + 1 → k < t → B ⁡ k < B ⁡ t
16 1 5 15 mp2b ⊢ ∀ k ∈ 0 ..^ T t = 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 ..^ T t = k + 1 → k < t → B ⁡ k < B ⁡ t → ∀ k ∈ 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 ⊢ ∀ k ∈ 0 ..^ T t = k + 1 → B ⁡ k < B ⁡ t → ∀ k ∈ 0 ..^ T t = k + 1 → B ⁡ k < B ⁡ k + 1
31 16 25 30 mp2b ⊢ ∀ k ∈ 0 ..^ T t = 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 → ∃ t t = k + 1 → ∃ t B ⁡ k < B ⁡ k + 1
34 3 33 mpi ⊢ k ∈ 0 ..^ T → ∃ t B ⁡ k < B ⁡ k + 1
35 ax5e ⊢ ∃ t B ⁡ 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 ..^ T B ⁡ k < B ⁡ k + 1