MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ostth2lem2 Structured version   Visualization version   GIF version

Theorem ostth2lem2 25775
Description: Lemma for ostth2 25778. (Contributed by Mario Carneiro, 10-Sep-2014.)
Hypotheses
Ref Expression
qrng.q 𝑄 = (ℂflds ℚ)
qabsabv.a 𝐴 = (AbsVal‘𝑄)
padic.j 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))
ostth.k 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))
ostth.1 (𝜑𝐹𝐴)
ostth2.2 (𝜑𝑁 ∈ (ℤ‘2))
ostth2.3 (𝜑 → 1 < (𝐹𝑁))
ostth2.4 𝑅 = ((log‘(𝐹𝑁)) / (log‘𝑁))
ostth2.5 (𝜑𝑀 ∈ (ℤ‘2))
ostth2.6 𝑆 = ((log‘(𝐹𝑀)) / (log‘𝑀))
ostth2.7 𝑇 = if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀))
Assertion
Ref Expression
ostth2lem2 ((𝜑𝑋 ∈ ℕ0𝑌 ∈ (0...((𝑀𝑋) − 1))) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
Distinct variable groups:   𝑥,𝑀   𝑥,𝑞,𝜑   𝑥,𝑇   𝑥,𝑋   𝐴,𝑞,𝑥   𝑥,𝑁   𝑥,𝑄   𝐹,𝑞   𝑅,𝑞   𝑥,𝐹
Allowed substitution hints:   𝑄(𝑞)   𝑅(𝑥)   𝑆(𝑥,𝑞)   𝑇(𝑞)   𝐽(𝑥,𝑞)   𝐾(𝑥,𝑞)   𝑀(𝑞)   𝑁(𝑞)   𝑋(𝑞)   𝑌(𝑥,𝑞)

Proof of Theorem ostth2lem2
Dummy variables 𝑘 𝑛 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6930 . . . . . . . . 9 (𝑥 = 0 → (𝑀𝑥) = (𝑀↑0))
21oveq1d 6937 . . . . . . . 8 (𝑥 = 0 → ((𝑀𝑥) − 1) = ((𝑀↑0) − 1))
32oveq2d 6938 . . . . . . 7 (𝑥 = 0 → (0...((𝑀𝑥) − 1)) = (0...((𝑀↑0) − 1)))
4 oveq2 6930 . . . . . . . . 9 (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0))
5 oveq2 6930 . . . . . . . . 9 (𝑥 = 0 → (𝑇𝑥) = (𝑇↑0))
64, 5oveq12d 6940 . . . . . . . 8 (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 0) · (𝑇↑0)))
76breq2d 4898 . . . . . . 7 (𝑥 = 0 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
83, 7raleqbidv 3326 . . . . . 6 (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
98imbi2d 332 . . . . 5 (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))))
10 oveq2 6930 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑀𝑥) = (𝑀𝑛))
1110oveq1d 6937 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑀𝑥) − 1) = ((𝑀𝑛) − 1))
1211oveq2d 6938 . . . . . . 7 (𝑥 = 𝑛 → (0...((𝑀𝑥) − 1)) = (0...((𝑀𝑛) − 1)))
13 oveq2 6930 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛))
14 oveq2 6930 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑇𝑥) = (𝑇𝑛))
1513, 14oveq12d 6940 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 𝑛) · (𝑇𝑛)))
1615breq2d 4898 . . . . . . 7 (𝑥 = 𝑛 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
1712, 16raleqbidv 3326 . . . . . 6 (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
1817imbi2d 332 . . . . 5 (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))))
19 oveq2 6930 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑀𝑥) = (𝑀↑(𝑛 + 1)))
2019oveq1d 6937 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑀𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1))
2120oveq2d 6938 . . . . . . 7 (𝑥 = (𝑛 + 1) → (0...((𝑀𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1)))
22 oveq2 6930 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1)))
23 oveq2 6930 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑇𝑥) = (𝑇↑(𝑛 + 1)))
2422, 23oveq12d 6940 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
2524breq2d 4898 . . . . . . 7 (𝑥 = (𝑛 + 1) → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
2621, 25raleqbidv 3326 . . . . . 6 (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
2726imbi2d 332 . . . . 5 (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
28 oveq2 6930 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀𝑥) = (𝑀𝑋))
2928oveq1d 6937 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑀𝑥) − 1) = ((𝑀𝑋) − 1))
3029oveq2d 6938 . . . . . . 7 (𝑥 = 𝑋 → (0...((𝑀𝑥) − 1)) = (0...((𝑀𝑋) − 1)))
31 oveq2 6930 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋))
32 oveq2 6930 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑇𝑥) = (𝑇𝑋))
3331, 32oveq12d 6940 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 𝑋) · (𝑇𝑋)))
3433breq2d 4898 . . . . . . 7 (𝑥 = 𝑋 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
3530, 34raleqbidv 3326 . . . . . 6 (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
3635imbi2d 332 . . . . 5 (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))))
37 ostth2.5 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘2))
38 eluz2nn 12032 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘2) → 𝑀 ∈ ℕ)
3937, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℕ)
4039nncnd 11392 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
4140exp0d 13321 . . . . . . . . . . 11 (𝜑 → (𝑀↑0) = 1)
4241oveq1d 6937 . . . . . . . . . 10 (𝜑 → ((𝑀↑0) − 1) = (1 − 1))
43 1m1e0 11447 . . . . . . . . . 10 (1 − 1) = 0
4442, 43syl6eq 2830 . . . . . . . . 9 (𝜑 → ((𝑀↑0) − 1) = 0)
4544oveq2d 6938 . . . . . . . 8 (𝜑 → (0...((𝑀↑0) − 1)) = (0...0))
4645eleq2d 2845 . . . . . . 7 (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈ (0...0)))
47 0le0 11483 . . . . . . . . . 10 0 ≤ 0
4847a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 0)
49 ostth.1 . . . . . . . . . 10 (𝜑𝐹𝐴)
50 qabsabv.a . . . . . . . . . . 11 𝐴 = (AbsVal‘𝑄)
51 qrng.q . . . . . . . . . . . 12 𝑄 = (ℂflds ℚ)
5251qrng0 25762 . . . . . . . . . . 11 0 = (0g𝑄)
5350, 52abv0 19223 . . . . . . . . . 10 (𝐹𝐴 → (𝐹‘0) = 0)
5449, 53syl 17 . . . . . . . . 9 (𝜑 → (𝐹‘0) = 0)
5540mul01d 10575 . . . . . . . . . . 11 (𝜑 → (𝑀 · 0) = 0)
5655oveq1d 6937 . . . . . . . . . 10 (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0)))
57 ostth2.7 . . . . . . . . . . . . . 14 𝑇 = if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀))
58 1re 10376 . . . . . . . . . . . . . . 15 1 ∈ ℝ
59 nnq 12109 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
6039, 59syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℚ)
6151qrngbas 25760 . . . . . . . . . . . . . . . . 17 ℚ = (Base‘𝑄)
6250, 61abvcl 19216 . . . . . . . . . . . . . . . 16 ((𝐹𝐴𝑀 ∈ ℚ) → (𝐹𝑀) ∈ ℝ)
6349, 60, 62syl2anc 579 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑀) ∈ ℝ)
64 ifcl 4351 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝐹𝑀) ∈ ℝ) → if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)) ∈ ℝ)
6558, 63, 64sylancr 581 . . . . . . . . . . . . . 14 (𝜑 → if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)) ∈ ℝ)
6657, 65syl5eqel 2863 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℝ)
6766recnd 10405 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℂ)
68 0nn0 11659 . . . . . . . . . . . 12 0 ∈ ℕ0
69 expcl 13196 . . . . . . . . . . . 12 ((𝑇 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝑇↑0) ∈ ℂ)
7067, 68, 69sylancl 580 . . . . . . . . . . 11 (𝜑 → (𝑇↑0) ∈ ℂ)
7170mul02d 10574 . . . . . . . . . 10 (𝜑 → (0 · (𝑇↑0)) = 0)
7256, 71eqtrd 2814 . . . . . . . . 9 (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0)
7348, 54, 723brtr4d 4918 . . . . . . . 8 (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))
74 elfz1eq 12669 . . . . . . . . . 10 (𝑘 ∈ (0...0) → 𝑘 = 0)
7574fveq2d 6450 . . . . . . . . 9 (𝑘 ∈ (0...0) → (𝐹𝑘) = (𝐹‘0))
7675breq1d 4896 . . . . . . . 8 (𝑘 ∈ (0...0) → ((𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)) ↔ (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0))))
7773, 76syl5ibrcom 239 . . . . . . 7 (𝜑 → (𝑘 ∈ (0...0) → (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
7846, 77sylbid 232 . . . . . 6 (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) → (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
7978ralrimiv 3147 . . . . 5 (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))
80 fveq2 6446 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
8180breq1d 4896 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ (𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
8281cbvralv 3367 . . . . . . . 8 (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
8349ad2antrr 716 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝐹𝐴)
84 elfzelz 12659 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ)
8584ad2antrl 718 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℤ)
86 zq 12101 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → 𝑘 ∈ ℚ)
8785, 86syl 17 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℚ)
8850, 61abvcl 19216 . . . . . . . . . . . 12 ((𝐹𝐴𝑘 ∈ ℚ) → (𝐹𝑘) ∈ ℝ)
8983, 87, 88syl2anc 579 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ∈ ℝ)
9039ad2antrr 716 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℕ)
91 simplr 759 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℕ0)
9290, 91nnexpcld 13351 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℕ)
9385, 92zmodcld 13010 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℕ0)
9493nn0zd 11832 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℤ)
95 zq 12101 . . . . . . . . . . . . . 14 ((𝑘 mod (𝑀𝑛)) ∈ ℤ → (𝑘 mod (𝑀𝑛)) ∈ ℚ)
9694, 95syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℚ)
9750, 61abvcl 19216 . . . . . . . . . . . . 13 ((𝐹𝐴 ∧ (𝑘 mod (𝑀𝑛)) ∈ ℚ) → (𝐹‘(𝑘 mod (𝑀𝑛))) ∈ ℝ)
9883, 96, 97syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑘 mod (𝑀𝑛))) ∈ ℝ)
9990, 59syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℚ)
10083, 99, 62syl2anc 579 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ∈ ℝ)
101100, 91reexpcld 13344 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ∈ ℝ)
10285zred 11834 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℝ)
103102, 92nndivred 11429 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 / (𝑀𝑛)) ∈ ℝ)
104103flcld 12918 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℤ)
105 zq 12101 . . . . . . . . . . . . . . 15 ((⌊‘(𝑘 / (𝑀𝑛))) ∈ ℤ → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ)
106104, 105syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ)
10750, 61abvcl 19216 . . . . . . . . . . . . . 14 ((𝐹𝐴 ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℝ)
10883, 106, 107syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℝ)
109101, 108remulcld 10407 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ∈ ℝ)
11098, 109readdcld 10406 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ∈ ℝ)
11190nnred 11391 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℝ)
112 nn0p1nn 11683 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
113112ad2antlr 717 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℕ)
114113nnred 11391 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℝ)
115111, 114remulcld 10407 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ)
11666ad2antrr 716 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑇 ∈ ℝ)
117 peano2nn0 11684 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
118117ad2antlr 717 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℕ0)
119116, 118reexpcld 13344 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ)
120115, 119remulcld 10407 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ)
121 nnq 12109 . . . . . . . . . . . . . . 15 ((𝑀𝑛) ∈ ℕ → (𝑀𝑛) ∈ ℚ)
12292, 121syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℚ)
123 qmulcl 12114 . . . . . . . . . . . . . 14 (((𝑀𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ)
124122, 106, 123syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ)
125 qex 12108 . . . . . . . . . . . . . . 15 ℚ ∈ V
126 cnfldadd 20147 . . . . . . . . . . . . . . . 16 + = (+g‘ℂfld)
12751, 126ressplusg 16385 . . . . . . . . . . . . . . 15 (ℚ ∈ V → + = (+g𝑄))
128125, 127ax-mp 5 . . . . . . . . . . . . . 14 + = (+g𝑄)
12950, 61, 128abvtri 19222 . . . . . . . . . . . . 13 ((𝐹𝐴 ∧ (𝑘 mod (𝑀𝑛)) ∈ ℚ ∧ ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))))
13083, 96, 124, 129syl3anc 1439 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))))
13192nnrpd 12179 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℝ+)
132 modval 12989 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℝ ∧ (𝑀𝑛) ∈ ℝ+) → (𝑘 mod (𝑀𝑛)) = (𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
133102, 131, 132syl2anc 579 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) = (𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
134133oveq1d 6937 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
135102recnd 10405 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℂ)
136 qcn 12110 . . . . . . . . . . . . . . . 16 (((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
137124, 136syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
138135, 137npcand 10738 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = 𝑘)
139134, 138eqtrd 2814 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = 𝑘)
140139fveq2d 6450 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) = (𝐹𝑘))
141 cnfldmul 20148 . . . . . . . . . . . . . . . . . 18 · = (.r‘ℂfld)
14251, 141ressmulr 16398 . . . . . . . . . . . . . . . . 17 (ℚ ∈ V → · = (.r𝑄))
143125, 142ax-mp 5 . . . . . . . . . . . . . . . 16 · = (.r𝑄)
14450, 61, 143abvmul 19221 . . . . . . . . . . . . . . 15 ((𝐹𝐴 ∧ (𝑀𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
14583, 122, 106, 144syl3anc 1439 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
14651, 50qabvexp 25767 . . . . . . . . . . . . . . . 16 ((𝐹𝐴𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑀𝑛)) = ((𝐹𝑀)↑𝑛))
14783, 99, 91, 146syl3anc 1439 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑀𝑛)) = ((𝐹𝑀)↑𝑛))
148147oveq1d 6937 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) = (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
149145, 148eqtrd 2814 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
150149oveq2d 6938 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))))
151130, 140, 1503brtr3d 4917 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))))
152116, 91reexpcld 13344 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ∈ ℝ)
153115, 152remulcld 10407 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ∈ ℝ)
154 nn0re 11652 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
155154ad2antlr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℝ)
156111, 155remulcld 10407 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 𝑛) ∈ ℝ)
157156, 152remulcld 10407 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · 𝑛) · (𝑇𝑛)) ∈ ℝ)
158111, 152remulcld 10407 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑇𝑛)) ∈ ℝ)
159 fveq2 6446 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑘 mod (𝑀𝑛)) → (𝐹𝑗) = (𝐹‘(𝑘 mod (𝑀𝑛))))
160159breq1d 4896 . . . . . . . . . . . . . . 15 (𝑗 = (𝑘 mod (𝑀𝑛)) → ((𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
161 simprr 763 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
162 zmodfz 13011 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑀𝑛) ∈ ℕ) → (𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)))
16385, 92, 162syl2anc 579 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)))
164160, 161, 163rspcdva 3517 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
165111, 101remulcld 10407 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · ((𝐹𝑀)↑𝑛)) ∈ ℝ)
166101recnd 10405 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ∈ ℂ)
167108recnd 10405 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
168166, 167mulcomd 10398 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) · ((𝐹𝑀)↑𝑛)))
16950, 61abvge0 19217 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐴𝑀 ∈ ℚ) → 0 ≤ (𝐹𝑀))
17083, 99, 169syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ (𝐹𝑀))
171100, 91, 170expge0d 13345 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ ((𝐹𝑀)↑𝑛))
172104zred 11834 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℝ)
173 elfzle1 12661 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘)
174173ad2antrl 718 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ 𝑘)
17592nnred 11391 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℝ)
17692nngt0d 11424 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 < (𝑀𝑛))
177 divge0 11246 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ℝ ∧ 0 ≤ 𝑘) ∧ ((𝑀𝑛) ∈ ℝ ∧ 0 < (𝑀𝑛))) → 0 ≤ (𝑘 / (𝑀𝑛)))
178102, 174, 175, 176, 177syl22anc 829 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ (𝑘 / (𝑀𝑛)))
179 flge0nn0 12940 . . . . . . . . . . . . . . . . . . . 20 (((𝑘 / (𝑀𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀𝑛))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0)
180103, 178, 179syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0)
18151, 50qabvle 25766 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐴 ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ (⌊‘(𝑘 / (𝑀𝑛))))
18283, 180, 181syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ (⌊‘(𝑘 / (𝑀𝑛))))
183 simprl 761 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)))
184 0z 11739 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ ℤ
18590, 118nnexpcld 13351 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ)
186185nnzd 11833 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ)
187 elfzm11 12729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ∈ ℤ ∧ (𝑀↑(𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1)))))
188184, 186, 187sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1)))))
189183, 188mpbid 224 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1))))
190189simp3d 1135 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 < (𝑀↑(𝑛 + 1)))
19190nncnd 11392 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℂ)
192191, 91expp1d 13328 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀𝑛) · 𝑀))
193190, 192breqtrd 4912 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 < ((𝑀𝑛) · 𝑀))
194 ltdivmul 11252 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑀𝑛) ∈ ℝ ∧ 0 < (𝑀𝑛))) → ((𝑘 / (𝑀𝑛)) < 𝑀𝑘 < ((𝑀𝑛) · 𝑀)))
195102, 111, 175, 176, 194syl112anc 1442 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 / (𝑀𝑛)) < 𝑀𝑘 < ((𝑀𝑛) · 𝑀)))
196193, 195mpbird 249 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 / (𝑀𝑛)) < 𝑀)
19790nnzd 11833 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℤ)
198 fllt 12926 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 / (𝑀𝑛)) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑘 / (𝑀𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀))
199103, 197, 198syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 / (𝑀𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀))
200196, 199mpbid 224 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀)
201172, 111, 200ltled 10524 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ≤ 𝑀)
202108, 172, 111, 182, 201letrd 10533 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ 𝑀)
203108, 111, 101, 171, 202lemul1ad 11317 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) · ((𝐹𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹𝑀)↑𝑛)))
204168, 203eqbrtrd 4908 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ≤ (𝑀 · ((𝐹𝑀)↑𝑛)))
20590nnnn0d 11702 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℕ0)
206205nn0ge0d 11705 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ 𝑀)
207 max1 12328 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → (𝐹𝑀) ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
208100, 58, 207sylancl 580 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
209208, 57syl6breqr 4928 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ≤ 𝑇)
210 leexp1a 13237 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ0) ∧ (0 ≤ (𝐹𝑀) ∧ (𝐹𝑀) ≤ 𝑇)) → ((𝐹𝑀)↑𝑛) ≤ (𝑇𝑛))
211100, 116, 91, 170, 209, 210syl32anc 1446 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ≤ (𝑇𝑛))
212101, 152, 111, 206, 211lemul2ad 11318 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · ((𝐹𝑀)↑𝑛)) ≤ (𝑀 · (𝑇𝑛)))
213109, 165, 158, 204, 212letrd 10533 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ≤ (𝑀 · (𝑇𝑛)))
21498, 109, 157, 158, 164, 213le2addd 10994 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
215 nn0cn 11653 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
216215ad2antlr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℂ)
217 1cnd 10371 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ∈ ℂ)
218191, 216, 217adddid 10401 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1)))
219191mulid1d 10394 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 1) = 𝑀)
220219oveq2d 6938 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀))
221218, 220eqtrd 2814 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀))
222221oveq1d 6937 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇𝑛)))
223191, 216mulcld 10397 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 𝑛) ∈ ℂ)
224152recnd 10405 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ∈ ℂ)
225223, 191, 224adddird 10402 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇𝑛)) = (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
226222, 225eqtrd 2814 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) = (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
227214, 226breqtrrd 4914 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)))
228 max2 12330 . . . . . . . . . . . . . . . 16 (((𝐹𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → 1 ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
229100, 58, 228sylancl 580 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
230229, 57syl6breqr 4928 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ≤ 𝑇)
231 nn0z 11752 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
232231ad2antlr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℤ)
233 uzid 12007 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
234232, 233syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ (ℤ𝑛))
235 peano2uz 12047 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ𝑛) → (𝑛 + 1) ∈ (ℤ𝑛))
236234, 235syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ (ℤ𝑛))
237116, 230, 236leexp2ad 13362 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)))
23890, 113nnmulcld 11428 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ)
239238nngt0d 11424 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 < (𝑀 · (𝑛 + 1)))
240 lemul2 11230 . . . . . . . . . . . . . 14 (((𝑇𝑛) ∈ ℝ ∧ (𝑇↑(𝑛 + 1)) ∈ ℝ ∧ ((𝑀 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑀 · (𝑛 + 1)))) → ((𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
241152, 119, 115, 239, 240syl112anc 1442 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
242237, 241mpbid 224 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
243110, 153, 120, 227, 242letrd 10533 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
24489, 110, 120, 151, 243letrd 10533 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
245244expr 450 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
246245ralrimdva 3151 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
24782, 246syl5bi 234 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
248247expcom 404 . . . . . 6 (𝑛 ∈ ℕ0 → (𝜑 → (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
249248a2d 29 . . . . 5 (𝑛 ∈ ℕ0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))) → (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
2509, 18, 27, 36, 79, 249nn0ind 11824 . . . 4 (𝑋 ∈ ℕ0 → (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
251250impcom 398 . . 3 ((𝜑𝑋 ∈ ℕ0) → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
252 fveq2 6446 . . . . 5 (𝑘 = 𝑌 → (𝐹𝑘) = (𝐹𝑌))
253252breq1d 4896 . . . 4 (𝑘 = 𝑌 → ((𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)) ↔ (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
254253rspccv 3508 . . 3 (∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)) → (𝑌 ∈ (0...((𝑀𝑋) − 1)) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
255251, 254syl 17 . 2 ((𝜑𝑋 ∈ ℕ0) → (𝑌 ∈ (0...((𝑀𝑋) − 1)) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
2562553impia 1106 1 ((𝜑𝑋 ∈ ℕ0𝑌 ∈ (0...((𝑀𝑋) − 1))) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2107  wral 3090  Vcvv 3398  ifcif 4307   class class class wbr 4886  cmpt 4965  cfv 6135  (class class class)co 6922  cc 10270  cr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277   < clt 10411  cle 10412  cmin 10606  -cneg 10607   / cdiv 11032  cn 11374  2c2 11430  0cn0 11642  cz 11728  cuz 11992  cq 12095  +crp 12137  ...cfz 12643  cfl 12910   mod cmo 12987  cexp 13178  cprime 15790   pCnt cpc 15945  s cress 16256  +gcplusg 16338  .rcmulr 16339  AbsValcabv 19208  fldccnfld 20142  logclog 24738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-tpos 7634  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-ico 12493  df-fz 12644  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-starv 16353  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-0g 16488  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-grp 17812  df-minusg 17813  df-subg 17975  df-cmn 18581  df-mgp 18877  df-ur 18889  df-ring 18936  df-cring 18937  df-oppr 19010  df-dvdsr 19028  df-unit 19029  df-invr 19059  df-dvr 19070  df-drng 19141  df-subrg 19170  df-abv 19209  df-cnfld 20143
This theorem is referenced by:  ostth2lem3  25776
  Copyright terms: Public domain W3C validator