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

Proof

Step Hyp Ref Expression
1 natglobalincr.1 ⊢ ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) )
2 natglobalincr.2 ⊢ 𝑇 ∈ ℤ
3 elfzoelz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 ∈ ℤ )
4 3 peano2zd ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑘 + 1 ) ∈ ℤ )
5 elfz1 ⊢ ( ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑇 ∈ ℤ ) → ( 𝑡 ∈ ( ( 𝑘 + 1 ) ... 𝑇 ) ↔ ( 𝑡 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇 ) ) )
6 4 2 5 sylancl ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑡 ∈ ( ( 𝑘 + 1 ) ... 𝑇 ) ↔ ( 𝑡 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇 ) ) )
7 fveq2 ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
8 7 breq2d ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
9 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑏 ) )
10 9 breq2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) )
11 fveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
12 11 breq2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) ) )
13 fveq2 ⊢ ( 𝑎 = 𝑡 → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑡 ) )
14 13 breq2d ⊢ ( 𝑎 = 𝑡 → ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) ) )
15 1 rspec ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
16 df-br ⊢ ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ↔ ⟨ ( 𝐵 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑏 ) ⟩ ∈ < )
17 ltrelxr ⊢ < ⊆ ( ℝ* × ℝ* )
18 17 sseli ⊢ ( ⟨ ( 𝐵 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑏 ) ⟩ ∈ < → ⟨ ( 𝐵 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑏 ) ⟩ ∈ ( ℝ* × ℝ* ) )
19 16 18 sylbi ⊢ ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) → ⟨ ( 𝐵 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑏 ) ⟩ ∈ ( ℝ* × ℝ* ) )
20 opelxp1 ⊢ ( ⟨ ( 𝐵 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑏 ) ⟩ ∈ ( ℝ* × ℝ* ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
21 19 20 syl ⊢ ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
22 21 3ad2ant3 ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
23 opelxp2 ⊢ ( ⟨ ( 𝐵 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑏 ) ⟩ ∈ ( ℝ* × ℝ* ) → ( 𝐵 ‘ 𝑏 ) ∈ ℝ* )
24 19 23 syl ⊢ ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) → ( 𝐵 ‘ 𝑏 ) ∈ ℝ* )
25 24 3ad2ant3 ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑏 ) ∈ ℝ* )
26 0red ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → 0 ∈ ℝ )
27 simp1 ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → 𝑘 ∈ ( 0 ..^ 𝑇 ) )
28 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
29 peano2re ⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
30 27 3 28 29 4syl ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
31 simp21 ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → 𝑏 ∈ ℤ )
32 31 zred ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → 𝑏 ∈ ℝ )
33 elfzole1 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 0 ≤ 𝑘 )
34 28 ltp1d ⊢ ( 𝑘 ∈ ℤ → 𝑘 < ( 𝑘 + 1 ) )
35 3 34 syl ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 < ( 𝑘 + 1 ) )
36 0red ⊢ ( 𝑘 ∈ ℝ → 0 ∈ ℝ )
37 id ⊢ ( 𝑘 ∈ ℝ → 𝑘 ∈ ℝ )
38 36 37 29 3jca ⊢ ( 𝑘 ∈ ℝ → ( 0 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) )
39 leltletr ⊢ ( ( 0 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( ( 0 ≤ 𝑘 ∧ 𝑘 < ( 𝑘 + 1 ) ) → 0 ≤ ( 𝑘 + 1 ) ) )
40 3 28 38 39 4syl ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( ( 0 ≤ 𝑘 ∧ 𝑘 < ( 𝑘 + 1 ) ) → 0 ≤ ( 𝑘 + 1 ) ) )
41 33 35 40 mp2and ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 0 ≤ ( 𝑘 + 1 ) )
42 41 3ad2ant1 ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → 0 ≤ ( 𝑘 + 1 ) )
43 simp22 ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( 𝑘 + 1 ) ≤ 𝑏 )
44 26 30 32 42 43 letrd ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → 0 ≤ 𝑏 )
45 simp23 ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → 𝑏 < 𝑇 )
46 0zd ⊢ ( 𝑏 ∈ ℤ → 0 ∈ ℤ )
47 2 a1i ⊢ ( 𝑏 ∈ ℤ → 𝑇 ∈ ℤ )
48 elfzo ⊢ ( ( 𝑏 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑇 ∈ ℤ ) → ( 𝑏 ∈ ( 0 ..^ 𝑇 ) ↔ ( 0 ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ) )
49 46 47 48 mpd3an23 ⊢ ( 𝑏 ∈ ℤ → ( 𝑏 ∈ ( 0 ..^ 𝑇 ) ↔ ( 0 ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ) )
50 fveq2 ⊢ ( 𝑘 = 𝑏 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑏 ) )
51 fvoveq1 ⊢ ( 𝑘 = 𝑏 → ( 𝐵 ‘ ( 𝑘 + 1 ) ) = ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
52 50 51 breq12d ⊢ ( 𝑘 = 𝑏 → ( ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐵 ‘ 𝑏 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) ) )
53 52 1 vtoclri ⊢ ( 𝑏 ∈ ( 0 ..^ 𝑇 ) → ( 𝐵 ‘ 𝑏 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
54 49 53 biimtrrdi ⊢ ( 𝑏 ∈ ℤ → ( ( 0 ≤ 𝑏 ∧ 𝑏 < 𝑇 ) → ( 𝐵 ‘ 𝑏 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) ) )
55 31 54 syl ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( ( 0 ≤ 𝑏 ∧ 𝑏 < 𝑇 ) → ( 𝐵 ‘ 𝑏 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) ) )
56 44 45 55 mp2and ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑏 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
57 df-br ⊢ ( ( 𝐵 ‘ 𝑏 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) ↔ ⟨ ( 𝐵 ‘ 𝑏 ) , ( 𝐵 ‘ ( 𝑏 + 1 ) ) ⟩ ∈ < )
58 17 sseli ⊢ ( ⟨ ( 𝐵 ‘ 𝑏 ) , ( 𝐵 ‘ ( 𝑏 + 1 ) ) ⟩ ∈ < → ⟨ ( 𝐵 ‘ 𝑏 ) , ( 𝐵 ‘ ( 𝑏 + 1 ) ) ⟩ ∈ ( ℝ* × ℝ* ) )
59 57 58 sylbi ⊢ ( ( 𝐵 ‘ 𝑏 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) → ⟨ ( 𝐵 ‘ 𝑏 ) , ( 𝐵 ‘ ( 𝑏 + 1 ) ) ⟩ ∈ ( ℝ* × ℝ* ) )
60 opelxp2 ⊢ ( ⟨ ( 𝐵 ‘ 𝑏 ) , ( 𝐵 ‘ ( 𝑏 + 1 ) ) ⟩ ∈ ( ℝ* × ℝ* ) → ( 𝐵 ‘ ( 𝑏 + 1 ) ) ∈ ℝ* )
61 56 59 60 3syl ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ ( 𝑏 + 1 ) ) ∈ ℝ* )
62 simp3 ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) )
63 22 25 61 62 56 xrlttrd ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
64 elfzoel2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑇 ∈ ℤ )
65 elfzop1le2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑘 + 1 ) ≤ 𝑇 )
66 8 10 12 14 15 63 4 64 65 fzindd ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ ( 𝑡 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇 ) ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) )
67 6 66 sylbida ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( ( 𝑘 + 1 ) ... 𝑇 ) ) → ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 ) )
68 67 rgen2 ⊢ ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ∀ 𝑡 ∈ ( ( 𝑘 + 1 ) ... 𝑇 ) ( 𝐵 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑡 )