| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 0 → (𝑀↑𝑥) = (𝑀↑0)) | 
| 2 | 1 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑥 = 0 → ((𝑀↑𝑥) − 1) = ((𝑀↑0) − 1)) | 
| 3 | 2 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = 0 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑0) − 1))) | 
| 4 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0)) | 
| 5 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 0 → (𝑇↑𝑥) = (𝑇↑0)) | 
| 6 | 4, 5 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 0) · (𝑇↑0))) | 
| 7 | 6 | breq2d 5155 | . . . . . . 7
⊢ (𝑥 = 0 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))) | 
| 8 | 3, 7 | raleqbidv 3346 | . . . . . 6
⊢ (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))) | 
| 9 | 8 | imbi2d 340 | . . . . 5
⊢ (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))) | 
| 10 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑀↑𝑥) = (𝑀↑𝑛)) | 
| 11 | 10 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑛) − 1)) | 
| 12 | 11 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = 𝑛 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑛) − 1))) | 
| 13 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛)) | 
| 14 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑇↑𝑥) = (𝑇↑𝑛)) | 
| 15 | 13, 14 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑛) · (𝑇↑𝑛))) | 
| 16 | 15 | breq2d 5155 | . . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) | 
| 17 | 12, 16 | raleqbidv 3346 | . . . . . 6
⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) | 
| 18 | 17 | imbi2d 340 | . . . . 5
⊢ (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))) | 
| 19 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (𝑀↑𝑥) = (𝑀↑(𝑛 + 1))) | 
| 20 | 19 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → ((𝑀↑𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1)) | 
| 21 | 20 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1))) | 
| 22 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1))) | 
| 23 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (𝑇↑𝑥) = (𝑇↑(𝑛 + 1))) | 
| 24 | 22, 23 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))) | 
| 25 | 24 | breq2d 5155 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))) | 
| 26 | 21, 25 | raleqbidv 3346 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))) | 
| 27 | 26 | imbi2d 340 | . . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))) | 
| 28 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑀↑𝑥) = (𝑀↑𝑋)) | 
| 29 | 28 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑋) − 1)) | 
| 30 | 29 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑋) − 1))) | 
| 31 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋)) | 
| 32 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑇↑𝑥) = (𝑇↑𝑋)) | 
| 33 | 31, 32 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑋) · (𝑇↑𝑋))) | 
| 34 | 33 | breq2d 5155 | . . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))) | 
| 35 | 30, 34 | raleqbidv 3346 | . . . . . 6
⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))) | 
| 36 | 35 | imbi2d 340 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))) | 
| 37 |  | ostth2.5 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘2)) | 
| 38 |  | eluz2nn 12924 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘2) → 𝑀 ∈ ℕ) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 40 | 39 | nncnd 12282 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 41 | 40 | exp0d 14180 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀↑0) = 1) | 
| 42 | 41 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑀↑0) − 1) = (1 −
1)) | 
| 43 |  | 1m1e0 12338 | . . . . . . . . . 10
⊢ (1
− 1) = 0 | 
| 44 | 42, 43 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝜑 → ((𝑀↑0) − 1) = 0) | 
| 45 | 44 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → (0...((𝑀↑0) − 1)) =
(0...0)) | 
| 46 | 45 | eleq2d 2827 | . . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈
(0...0))) | 
| 47 |  | 0le0 12367 | . . . . . . . . . 10
⊢ 0 ≤
0 | 
| 48 | 47 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 0 ≤ 0) | 
| 49 |  | ostth.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ 𝐴) | 
| 50 |  | qabsabv.a | . . . . . . . . . . 11
⊢ 𝐴 = (AbsVal‘𝑄) | 
| 51 |  | qrng.q | . . . . . . . . . . . 12
⊢ 𝑄 = (ℂfld
↾s ℚ) | 
| 52 | 51 | qrng0 27665 | . . . . . . . . . . 11
⊢ 0 =
(0g‘𝑄) | 
| 53 | 50, 52 | abv0 20824 | . . . . . . . . . 10
⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0) | 
| 54 | 49, 53 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘0) = 0) | 
| 55 | 40 | mul01d 11460 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀 · 0) = 0) | 
| 56 | 55 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0))) | 
| 57 |  | ostth2.7 | . . . . . . . . . . . . . 14
⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) | 
| 58 |  | 1re 11261 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ | 
| 59 |  | nnq 13004 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℚ) | 
| 60 | 39, 59 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℚ) | 
| 61 | 51 | qrngbas 27663 | . . . . . . . . . . . . . . . . 17
⊢ ℚ =
(Base‘𝑄) | 
| 62 | 50, 61 | abvcl 20817 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℝ) | 
| 63 | 49, 60, 62 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) | 
| 64 |  | ifcl 4571 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ (𝐹‘𝑀) ∈ ℝ) → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ) | 
| 65 | 58, 63, 64 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝜑 → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ) | 
| 66 | 57, 65 | eqeltrid 2845 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ ℝ) | 
| 67 | 66 | recnd 11289 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℂ) | 
| 68 |  | 0nn0 12541 | . . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 | 
| 69 |  | expcl 14120 | . . . . . . . . . . . 12
⊢ ((𝑇 ∈ ℂ ∧ 0 ∈
ℕ0) → (𝑇↑0) ∈ ℂ) | 
| 70 | 67, 68, 69 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑇↑0) ∈ ℂ) | 
| 71 | 70 | mul02d 11459 | . . . . . . . . . 10
⊢ (𝜑 → (0 · (𝑇↑0)) = 0) | 
| 72 | 56, 71 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0) | 
| 73 | 48, 54, 72 | 3brtr4d 5175 | . . . . . . . 8
⊢ (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0))) | 
| 74 |  | elfz1eq 13575 | . . . . . . . . . 10
⊢ (𝑘 ∈ (0...0) → 𝑘 = 0) | 
| 75 | 74 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...0) → (𝐹‘𝑘) = (𝐹‘0)) | 
| 76 | 75 | breq1d 5153 | . . . . . . . 8
⊢ (𝑘 ∈ (0...0) → ((𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)) ↔ (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))) | 
| 77 | 73, 76 | syl5ibrcom 247 | . . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (0...0) → (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))) | 
| 78 | 46, 77 | sylbid 240 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) → (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))) | 
| 79 | 78 | ralrimiv 3145 | . . . . 5
⊢ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))) | 
| 80 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) | 
| 81 | 80 | breq1d 5153 | . . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) | 
| 82 | 81 | cbvralvw 3237 | . . . . . . . 8
⊢
(∀𝑘 ∈
(0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))) | 
| 83 | 49 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝐹 ∈ 𝐴) | 
| 84 |  | elfzelz 13564 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ) | 
| 85 | 84 | ad2antrl 728 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℤ) | 
| 86 |  | zq 12996 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℚ) | 
| 87 | 85, 86 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℚ) | 
| 88 | 50, 61 | abvcl 20817 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑘 ∈ ℚ) → (𝐹‘𝑘) ∈ ℝ) | 
| 89 | 83, 87, 88 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ∈ ℝ) | 
| 90 | 39 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℕ) | 
| 91 |  | simplr 769 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℕ0) | 
| 92 | 90, 91 | nnexpcld 14284 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℕ) | 
| 93 | 85, 92 | zmodcld 13932 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈
ℕ0) | 
| 94 | 93 | nn0zd 12639 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℤ) | 
| 95 |  | zq 12996 | . . . . . . . . . . . . . 14
⊢ ((𝑘 mod (𝑀↑𝑛)) ∈ ℤ → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ) | 
| 96 | 94, 95 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ) | 
| 97 | 50, 61 | abvcl 20817 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ∈ ℝ) | 
| 98 | 83, 96, 97 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ∈ ℝ) | 
| 99 | 90, 59 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℚ) | 
| 100 | 83, 99, 62 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ∈ ℝ) | 
| 101 | 100, 91 | reexpcld 14203 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℝ) | 
| 102 | 85 | zred 12722 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℝ) | 
| 103 | 102, 92 | nndivred 12320 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) ∈ ℝ) | 
| 104 | 103 | flcld 13838 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ) | 
| 105 |  | zq 12996 | . . . . . . . . . . . . . . 15
⊢
((⌊‘(𝑘 /
(𝑀↑𝑛))) ∈ ℤ →
(⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) | 
| 107 | 50, 61 | abvcl 20817 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ) | 
| 108 | 83, 106, 107 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ) | 
| 109 | 101, 108 | remulcld 11291 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ∈ ℝ) | 
| 110 | 98, 109 | readdcld 11290 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ∈ ℝ) | 
| 111 | 90 | nnred 12281 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℝ) | 
| 112 |  | nn0p1nn 12565 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) | 
| 113 | 112 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ) | 
| 114 | 113 | nnred 12281 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℝ) | 
| 115 | 111, 114 | remulcld 11291 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ) | 
| 116 | 66 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑇 ∈ ℝ) | 
| 117 |  | peano2nn0 12566 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ0) | 
| 118 | 117 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈
ℕ0) | 
| 119 | 116, 118 | reexpcld 14203 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ) | 
| 120 | 115, 119 | remulcld 11291 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ) | 
| 121 |  | nnq 13004 | . . . . . . . . . . . . . . 15
⊢ ((𝑀↑𝑛) ∈ ℕ → (𝑀↑𝑛) ∈ ℚ) | 
| 122 | 92, 121 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℚ) | 
| 123 |  | qmulcl 13009 | . . . . . . . . . . . . . 14
⊢ (((𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ) | 
| 124 | 122, 106,
123 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ) | 
| 125 |  | qex 13003 | . . . . . . . . . . . . . . 15
⊢ ℚ
∈ V | 
| 126 |  | cnfldadd 21370 | . . . . . . . . . . . . . . . 16
⊢  + =
(+g‘ℂfld) | 
| 127 | 51, 126 | ressplusg 17334 | . . . . . . . . . . . . . . 15
⊢ (ℚ
∈ V → + = (+g‘𝑄)) | 
| 128 | 125, 127 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢  + =
(+g‘𝑄) | 
| 129 | 50, 61, 128 | abvtri 20823 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ ∧ ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))) | 
| 130 | 83, 96, 124, 129 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))) | 
| 131 | 92 | nnrpd 13075 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈
ℝ+) | 
| 132 |  | modval 13911 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℝ ∧ (𝑀↑𝑛) ∈ ℝ+) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) | 
| 133 | 102, 131,
132 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) | 
| 134 | 133 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) | 
| 135 | 102 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℂ) | 
| 136 |  | qcn 13005 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ) | 
| 137 | 124, 136 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ) | 
| 138 | 135, 137 | npcand 11624 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘) | 
| 139 | 134, 138 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘) | 
| 140 | 139 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = (𝐹‘𝑘)) | 
| 141 |  | cnfldmul 21372 | . . . . . . . . . . . . . . . . . 18
⊢  ·
= (.r‘ℂfld) | 
| 142 | 51, 141 | ressmulr 17351 | . . . . . . . . . . . . . . . . 17
⊢ (ℚ
∈ V → · = (.r‘𝑄)) | 
| 143 | 125, 142 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢  ·
= (.r‘𝑄) | 
| 144 | 50, 61, 143 | abvmul 20822 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) | 
| 145 | 83, 122, 106, 144 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) | 
| 146 | 51, 50 | qabvexp 27670 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛)) | 
| 147 | 83, 99, 91, 146 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛)) | 
| 148 | 147 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) | 
| 149 | 145, 148 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) | 
| 150 | 149 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))) | 
| 151 | 130, 140,
150 | 3brtr3d 5174 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))) | 
| 152 | 116, 91 | reexpcld 14203 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℝ) | 
| 153 | 115, 152 | remulcld 11291 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ∈ ℝ) | 
| 154 |  | nn0re 12535 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) | 
| 155 | 154 | ad2antlr 727 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℝ) | 
| 156 | 111, 155 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℝ) | 
| 157 | 156, 152 | remulcld 11291 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) · (𝑇↑𝑛)) ∈ ℝ) | 
| 158 | 111, 152 | remulcld 11291 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑇↑𝑛)) ∈ ℝ) | 
| 159 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → (𝐹‘𝑗) = (𝐹‘(𝑘 mod (𝑀↑𝑛)))) | 
| 160 | 159 | breq1d 5153 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → ((𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) | 
| 161 |  | simprr 773 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))) | 
| 162 |  | zmodfz 13933 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ (𝑀↑𝑛) ∈ ℕ) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1))) | 
| 163 | 85, 92, 162 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1))) | 
| 164 | 160, 161,
163 | rspcdva 3623 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))) | 
| 165 | 111, 101 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ∈ ℝ) | 
| 166 | 101 | recnd 11289 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℂ) | 
| 167 | 108 | recnd 11289 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ) | 
| 168 | 166, 167 | mulcomd 11282 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛))) | 
| 169 | 50, 61 | abvge0 20818 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → 0 ≤ (𝐹‘𝑀)) | 
| 170 | 83, 99, 169 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝐹‘𝑀)) | 
| 171 | 100, 91, 170 | expge0d 14204 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ ((𝐹‘𝑀)↑𝑛)) | 
| 172 | 104 | zred 12722 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℝ) | 
| 173 |  | elfzle1 13567 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘) | 
| 174 | 173 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑘) | 
| 175 | 92 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ) | 
| 176 | 92 | nngt0d 12315 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀↑𝑛)) | 
| 177 |  | divge0 12137 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑘 ∈ ℝ ∧ 0 ≤
𝑘) ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → 0 ≤ (𝑘 / (𝑀↑𝑛))) | 
| 178 | 102, 174,
175, 176, 177 | syl22anc 839 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝑘 / (𝑀↑𝑛))) | 
| 179 |  | flge0nn0 13860 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀↑𝑛))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈
ℕ0) | 
| 180 | 103, 178,
179 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈
ℕ0) | 
| 181 | 51, 50 | qabvle 27669 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ0) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ (⌊‘(𝑘 / (𝑀↑𝑛)))) | 
| 182 | 83, 180, 181 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ (⌊‘(𝑘 / (𝑀↑𝑛)))) | 
| 183 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) | 
| 184 |  | 0z 12624 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
ℤ | 
| 185 | 90, 118 | nnexpcld 14284 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ) | 
| 186 | 185 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ) | 
| 187 |  | elfzm11 13635 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((0
∈ ℤ ∧ (𝑀↑(𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1))))) | 
| 188 | 184, 186,
187 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1))))) | 
| 189 | 183, 188 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1)))) | 
| 190 | 189 | simp3d 1145 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < (𝑀↑(𝑛 + 1))) | 
| 191 | 90 | nncnd 12282 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℂ) | 
| 192 | 191, 91 | expp1d 14187 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀↑𝑛) · 𝑀)) | 
| 193 | 190, 192 | breqtrd 5169 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < ((𝑀↑𝑛) · 𝑀)) | 
| 194 |  | ltdivmul 12143 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ 𝑘 < ((𝑀↑𝑛) · 𝑀))) | 
| 195 | 102, 111,
175, 176, 194 | syl112anc 1376 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ 𝑘 < ((𝑀↑𝑛) · 𝑀))) | 
| 196 | 193, 195 | mpbird 257 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) < 𝑀) | 
| 197 | 90 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℤ) | 
| 198 |  | fllt 13846 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀)) | 
| 199 | 103, 197,
198 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀)) | 
| 200 | 196, 199 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀) | 
| 201 | 172, 111,
200 | ltled 11409 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ≤ 𝑀) | 
| 202 | 108, 172,
111, 182, 201 | letrd 11418 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ 𝑀) | 
| 203 | 108, 111,
101, 171, 202 | lemul1ad 12207 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛))) | 
| 204 | 168, 203 | eqbrtrd 5165 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛))) | 
| 205 | 90 | nnnn0d 12587 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈
ℕ0) | 
| 206 | 205 | nn0ge0d 12590 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑀) | 
| 207 |  | max1 13227 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ)
→ (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))) | 
| 208 | 100, 58, 207 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))) | 
| 209 | 208, 57 | breqtrrdi 5185 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ 𝑇) | 
| 210 |  | leexp1a 14215 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ0) ∧ (0 ≤
(𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ 𝑇)) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛)) | 
| 211 | 100, 116,
91, 170, 209, 210 | syl32anc 1380 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛)) | 
| 212 | 101, 152,
111, 206, 211 | lemul2ad 12208 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · (𝑇↑𝑛))) | 
| 213 | 109, 165,
158, 204, 212 | letrd 11418 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · (𝑇↑𝑛))) | 
| 214 | 98, 109, 157, 158, 164, 213 | le2addd 11882 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛)))) | 
| 215 |  | nn0cn 12536 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) | 
| 216 | 215 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℂ) | 
| 217 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ∈
ℂ) | 
| 218 | 191, 216,
217 | adddid 11285 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1))) | 
| 219 | 191 | mulridd 11278 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 1) = 𝑀) | 
| 220 | 219 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀)) | 
| 221 | 218, 220 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀)) | 
| 222 | 221 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛))) | 
| 223 | 191, 216 | mulcld 11281 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℂ) | 
| 224 | 152 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℂ) | 
| 225 | 223, 191,
224 | adddird 11286 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛)))) | 
| 226 | 222, 225 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛)))) | 
| 227 | 214, 226 | breqtrrd 5171 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛))) | 
| 228 |  | max2 13229 | . . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ)
→ 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))) | 
| 229 | 100, 58, 228 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))) | 
| 230 | 229, 57 | breqtrrdi 5185 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ 𝑇) | 
| 231 |  | nn0z 12638 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) | 
| 232 | 231 | ad2antlr 727 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℤ) | 
| 233 |  | uzid 12893 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) | 
| 234 | 232, 233 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ (ℤ≥‘𝑛)) | 
| 235 |  | peano2uz 12943 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (𝑛 + 1) ∈
(ℤ≥‘𝑛)) | 
| 236 | 234, 235 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈
(ℤ≥‘𝑛)) | 
| 237 | 116, 230,
236 | leexp2ad 14293 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1))) | 
| 238 | 90, 113 | nnmulcld 12319 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ) | 
| 239 | 238 | nngt0d 12315 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀 · (𝑛 + 1))) | 
| 240 |  | lemul2 12120 | . . . . . . . . . . . . . 14
⊢ (((𝑇↑𝑛) ∈ ℝ ∧ (𝑇↑(𝑛 + 1)) ∈ ℝ ∧ ((𝑀 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑀 · (𝑛 + 1)))) → ((𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))) | 
| 241 | 152, 119,
115, 239, 240 | syl112anc 1376 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))) | 
| 242 | 237, 241 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))) | 
| 243 | 110, 153,
120, 227, 242 | letrd 11418 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))) | 
| 244 | 89, 110, 120, 151, 243 | letrd 11418 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))) | 
| 245 | 244 | expr 456 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))) | 
| 246 | 245 | ralrimdva 3154 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(∀𝑗 ∈
(0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))) | 
| 247 | 82, 246 | biimtrid 242 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(∀𝑘 ∈
(0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))) | 
| 248 | 247 | expcom 413 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
→ (𝜑 →
(∀𝑘 ∈
(0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))) | 
| 249 | 248 | a2d 29 | . . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((𝜑 →
∀𝑘 ∈
(0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))) → (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))) | 
| 250 | 9, 18, 27, 36, 79, 249 | nn0ind 12713 | . . . 4
⊢ (𝑋 ∈ ℕ0
→ (𝜑 →
∀𝑘 ∈
(0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))) | 
| 251 | 250 | impcom 407 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ0) →
∀𝑘 ∈
(0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))) | 
| 252 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 𝑌 → (𝐹‘𝑘) = (𝐹‘𝑌)) | 
| 253 | 252 | breq1d 5153 | . . . 4
⊢ (𝑘 = 𝑌 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) ↔ (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))) | 
| 254 | 253 | rspccv 3619 | . . 3
⊢
(∀𝑘 ∈
(0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) → (𝑌 ∈ (0...((𝑀↑𝑋) − 1)) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))) | 
| 255 | 251, 254 | syl 17 | . 2
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ0) → (𝑌 ∈ (0...((𝑀↑𝑋) − 1)) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))) | 
| 256 | 255 | 3impia 1118 | 1
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ (0...((𝑀↑𝑋) − 1))) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))) |