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 ⊢ ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ∀ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) )
Assertion natlocalincr ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) )

Proof

Step Hyp Ref Expression
1 natlocalincr.1 ⊢ ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ∀ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) )
2 ovex ⊢ ( 𝑘 + 1 ) ∈ V
3 2 isseti ⊢ ∃ 𝑡 𝑡 = ( 𝑘 + 1 )
4 rsp ⊢ ( ∀ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) → ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) )
5 4 ralimi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ∀ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) )
6 1z ⊢ 1 ∈ ℤ
7 fzoaddel ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 1 ∈ ℤ ) → ( 𝑘 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑇 + 1 ) ) )
8 6 7 mpan2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑘 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑇 + 1 ) ) )
9 0p1e1 ⊢ ( 0 + 1 ) = 1
10 9 oveq1i ⊢ ( ( 0 + 1 ) ..^ ( 𝑇 + 1 ) ) = ( 1 ..^ ( 𝑇 + 1 ) )
11 8 10 eleqtrdi ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑘 + 1 ) ∈ ( 1 ..^ ( 𝑇 + 1 ) ) )
12 eleq1 ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) )
13 11 12 syl5ibrcom ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑡 = ( 𝑘 + 1 ) → 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) )
14 13 imim1d ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) → ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) ) )
15 14 ralimia ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) )
16 1 5 15 mp2b ⊢ ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) )
17 elfzoelz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 ∈ ℤ )
18 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
19 ltp1 ⊢ ( 𝑘 ∈ ℝ → 𝑘 < ( 𝑘 + 1 ) )
20 17 18 19 3syl ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 < ( 𝑘 + 1 ) )
21 breq2 ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 ↔ 𝑘 < ( 𝑘 + 1 ) ) )
22 20 21 syl5ibrcom ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑡 = ( 𝑘 + 1 ) → 𝑘 < 𝑡 ) )
23 ax-2 ⊢ ( ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) → ( ( 𝑡 = ( 𝑘 + 1 ) → 𝑘 < 𝑡 ) → ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) )
24 22 23 syl5com ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) → ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) )
25 24 ralimia ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) )
26 fveq2 ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑡 ) = ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
27 26 breq2d ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ↔ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
28 27 biimpd ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
29 28 a2i ⊢ ( ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) → ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
30 29 ralimi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
31 16 25 30 mp2b ⊢ ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
32 31 rspec ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
33 32 eximdv ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( ∃ 𝑡 𝑡 = ( 𝑘 + 1 ) → ∃ 𝑡 ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
34 3 33 mpi ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ∃ 𝑡 ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
35 ax5e ⊢ ( ∃ 𝑡 ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
36 34 35 syl ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
37 36 rgen ⊢ ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) )