| Step | Hyp | Ref
| Expression |
| 1 | | elfzoelz 13699 |
. . . . 5
⊢ (𝑘 ∈ (0..^𝑇) → 𝑘 ∈ ℤ) |
| 2 | 1 | peano2zd 12725 |
. . . 4
⊢ (𝑘 ∈ (0..^𝑇) → (𝑘 + 1) ∈ ℤ) |
| 3 | | natglobalincr.2 |
. . . 4
⊢ 𝑇 ∈ ℤ |
| 4 | | elfz1 13552 |
. . . 4
⊢ (((𝑘 + 1) ∈ ℤ ∧ 𝑇 ∈ ℤ) → (𝑡 ∈ ((𝑘 + 1)...𝑇) ↔ (𝑡 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇))) |
| 5 | 2, 3, 4 | sylancl 586 |
. . 3
⊢ (𝑘 ∈ (0..^𝑇) → (𝑡 ∈ ((𝑘 + 1)...𝑇) ↔ (𝑡 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇))) |
| 6 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = (𝑘 + 1) → (𝐵‘𝑎) = (𝐵‘(𝑘 + 1))) |
| 7 | 6 | breq2d 5155 |
. . . 4
⊢ (𝑎 = (𝑘 + 1) → ((𝐵‘𝑘) < (𝐵‘𝑎) ↔ (𝐵‘𝑘) < (𝐵‘(𝑘 + 1)))) |
| 8 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝐵‘𝑎) = (𝐵‘𝑏)) |
| 9 | 8 | breq2d 5155 |
. . . 4
⊢ (𝑎 = 𝑏 → ((𝐵‘𝑘) < (𝐵‘𝑎) ↔ (𝐵‘𝑘) < (𝐵‘𝑏))) |
| 10 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (𝐵‘𝑎) = (𝐵‘(𝑏 + 1))) |
| 11 | 10 | breq2d 5155 |
. . . 4
⊢ (𝑎 = (𝑏 + 1) → ((𝐵‘𝑘) < (𝐵‘𝑎) ↔ (𝐵‘𝑘) < (𝐵‘(𝑏 + 1)))) |
| 12 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = 𝑡 → (𝐵‘𝑎) = (𝐵‘𝑡)) |
| 13 | 12 | breq2d 5155 |
. . . 4
⊢ (𝑎 = 𝑡 → ((𝐵‘𝑘) < (𝐵‘𝑎) ↔ (𝐵‘𝑘) < (𝐵‘𝑡))) |
| 14 | | natglobalincr.1 |
. . . . 5
⊢
∀𝑘 ∈
(0..^𝑇)(𝐵‘𝑘) < (𝐵‘(𝑘 + 1)) |
| 15 | 14 | rspec 3250 |
. . . 4
⊢ (𝑘 ∈ (0..^𝑇) → (𝐵‘𝑘) < (𝐵‘(𝑘 + 1))) |
| 16 | | df-br 5144 |
. . . . . . . 8
⊢ ((𝐵‘𝑘) < (𝐵‘𝑏) ↔ 〈(𝐵‘𝑘), (𝐵‘𝑏)〉 ∈ < ) |
| 17 | | ltrelxr 11322 |
. . . . . . . . 9
⊢ <
⊆ (ℝ* × ℝ*) |
| 18 | 17 | sseli 3979 |
. . . . . . . 8
⊢
(〈(𝐵‘𝑘), (𝐵‘𝑏)〉 ∈ < → 〈(𝐵‘𝑘), (𝐵‘𝑏)〉 ∈ (ℝ* ×
ℝ*)) |
| 19 | 16, 18 | sylbi 217 |
. . . . . . 7
⊢ ((𝐵‘𝑘) < (𝐵‘𝑏) → 〈(𝐵‘𝑘), (𝐵‘𝑏)〉 ∈ (ℝ* ×
ℝ*)) |
| 20 | | opelxp1 5727 |
. . . . . . 7
⊢
(〈(𝐵‘𝑘), (𝐵‘𝑏)〉 ∈ (ℝ* ×
ℝ*) → (𝐵‘𝑘) ∈
ℝ*) |
| 21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝐵‘𝑘) < (𝐵‘𝑏) → (𝐵‘𝑘) ∈
ℝ*) |
| 22 | 21 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → (𝐵‘𝑘) ∈
ℝ*) |
| 23 | | opelxp2 5728 |
. . . . . . 7
⊢
(〈(𝐵‘𝑘), (𝐵‘𝑏)〉 ∈ (ℝ* ×
ℝ*) → (𝐵‘𝑏) ∈
ℝ*) |
| 24 | 19, 23 | syl 17 |
. . . . . 6
⊢ ((𝐵‘𝑘) < (𝐵‘𝑏) → (𝐵‘𝑏) ∈
ℝ*) |
| 25 | 24 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → (𝐵‘𝑏) ∈
ℝ*) |
| 26 | | 0red 11264 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → 0 ∈ ℝ) |
| 27 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → 𝑘 ∈ (0..^𝑇)) |
| 28 | | zre 12617 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) |
| 29 | | peano2re 11434 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
| 30 | 27, 1, 28, 29 | 4syl 19 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → (𝑘 + 1) ∈ ℝ) |
| 31 | | simp21 1207 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → 𝑏 ∈ ℤ) |
| 32 | 31 | zred 12722 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → 𝑏 ∈ ℝ) |
| 33 | | elfzole1 13707 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0..^𝑇) → 0 ≤ 𝑘) |
| 34 | 28 | ltp1d 12198 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℤ → 𝑘 < (𝑘 + 1)) |
| 35 | 1, 34 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0..^𝑇) → 𝑘 < (𝑘 + 1)) |
| 36 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℝ → 0 ∈
ℝ) |
| 37 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℝ → 𝑘 ∈
ℝ) |
| 38 | 36, 37, 29 | 3jca 1129 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℝ → (0 ∈
ℝ ∧ 𝑘 ∈
ℝ ∧ (𝑘 + 1)
∈ ℝ)) |
| 39 | | leltletr 11352 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝑘
∈ ℝ ∧ (𝑘 +
1) ∈ ℝ) → ((0 ≤ 𝑘 ∧ 𝑘 < (𝑘 + 1)) → 0 ≤ (𝑘 + 1))) |
| 40 | 1, 28, 38, 39 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0..^𝑇) → ((0 ≤ 𝑘 ∧ 𝑘 < (𝑘 + 1)) → 0 ≤ (𝑘 + 1))) |
| 41 | 33, 35, 40 | mp2and 699 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0..^𝑇) → 0 ≤ (𝑘 + 1)) |
| 42 | 41 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → 0 ≤ (𝑘 + 1)) |
| 43 | | simp22 1208 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → (𝑘 + 1) ≤ 𝑏) |
| 44 | 26, 30, 32, 42, 43 | letrd 11418 |
. . . . . . 7
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → 0 ≤ 𝑏) |
| 45 | | simp23 1209 |
. . . . . . 7
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → 𝑏 < 𝑇) |
| 46 | | 0zd 12625 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℤ → 0 ∈
ℤ) |
| 47 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℤ → 𝑇 ∈
ℤ) |
| 48 | | elfzo 13701 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑇 ∈
ℤ) → (𝑏 ∈
(0..^𝑇) ↔ (0 ≤
𝑏 ∧ 𝑏 < 𝑇))) |
| 49 | 46, 47, 48 | mpd3an23 1465 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℤ → (𝑏 ∈ (0..^𝑇) ↔ (0 ≤ 𝑏 ∧ 𝑏 < 𝑇))) |
| 50 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑏 → (𝐵‘𝑘) = (𝐵‘𝑏)) |
| 51 | | fvoveq1 7454 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑏 → (𝐵‘(𝑘 + 1)) = (𝐵‘(𝑏 + 1))) |
| 52 | 50, 51 | breq12d 5156 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑏 → ((𝐵‘𝑘) < (𝐵‘(𝑘 + 1)) ↔ (𝐵‘𝑏) < (𝐵‘(𝑏 + 1)))) |
| 53 | 52, 14 | vtoclri 3590 |
. . . . . . . . 9
⊢ (𝑏 ∈ (0..^𝑇) → (𝐵‘𝑏) < (𝐵‘(𝑏 + 1))) |
| 54 | 49, 53 | biimtrrdi 254 |
. . . . . . . 8
⊢ (𝑏 ∈ ℤ → ((0 ≤
𝑏 ∧ 𝑏 < 𝑇) → (𝐵‘𝑏) < (𝐵‘(𝑏 + 1)))) |
| 55 | 31, 54 | syl 17 |
. . . . . . 7
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → ((0 ≤ 𝑏 ∧ 𝑏 < 𝑇) → (𝐵‘𝑏) < (𝐵‘(𝑏 + 1)))) |
| 56 | 44, 45, 55 | mp2and 699 |
. . . . . 6
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → (𝐵‘𝑏) < (𝐵‘(𝑏 + 1))) |
| 57 | | df-br 5144 |
. . . . . . 7
⊢ ((𝐵‘𝑏) < (𝐵‘(𝑏 + 1)) ↔ 〈(𝐵‘𝑏), (𝐵‘(𝑏 + 1))〉 ∈ < ) |
| 58 | 17 | sseli 3979 |
. . . . . . 7
⊢
(〈(𝐵‘𝑏), (𝐵‘(𝑏 + 1))〉 ∈ < → 〈(𝐵‘𝑏), (𝐵‘(𝑏 + 1))〉 ∈ (ℝ*
× ℝ*)) |
| 59 | 57, 58 | sylbi 217 |
. . . . . 6
⊢ ((𝐵‘𝑏) < (𝐵‘(𝑏 + 1)) → 〈(𝐵‘𝑏), (𝐵‘(𝑏 + 1))〉 ∈ (ℝ*
× ℝ*)) |
| 60 | | opelxp2 5728 |
. . . . . 6
⊢
(〈(𝐵‘𝑏), (𝐵‘(𝑏 + 1))〉 ∈ (ℝ*
× ℝ*) → (𝐵‘(𝑏 + 1)) ∈
ℝ*) |
| 61 | 56, 59, 60 | 3syl 18 |
. . . . 5
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → (𝐵‘(𝑏 + 1)) ∈
ℝ*) |
| 62 | | simp3 1139 |
. . . . 5
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → (𝐵‘𝑘) < (𝐵‘𝑏)) |
| 63 | 22, 25, 61, 62, 56 | xrlttrd 13201 |
. . . 4
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑏 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑏 ∧ 𝑏 < 𝑇) ∧ (𝐵‘𝑘) < (𝐵‘𝑏)) → (𝐵‘𝑘) < (𝐵‘(𝑏 + 1))) |
| 64 | | elfzoel2 13698 |
. . . 4
⊢ (𝑘 ∈ (0..^𝑇) → 𝑇 ∈ ℤ) |
| 65 | | elfzop1le2 13712 |
. . . 4
⊢ (𝑘 ∈ (0..^𝑇) → (𝑘 + 1) ≤ 𝑇) |
| 66 | 7, 9, 11, 13, 15, 63, 2, 64, 65 | fzindd 12720 |
. . 3
⊢ ((𝑘 ∈ (0..^𝑇) ∧ (𝑡 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇)) → (𝐵‘𝑘) < (𝐵‘𝑡)) |
| 67 | 5, 66 | sylbida 592 |
. 2
⊢ ((𝑘 ∈ (0..^𝑇) ∧ 𝑡 ∈ ((𝑘 + 1)...𝑇)) → (𝐵‘𝑘) < (𝐵‘𝑡)) |
| 68 | 67 | rgen2 3199 |
1
⊢
∀𝑘 ∈
(0..^𝑇)∀𝑡 ∈ ((𝑘 + 1)...𝑇)(𝐵‘𝑘) < (𝐵‘𝑡) |