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

Theorem ostth2lem2 25522
Description: Lemma for ostth2 25525. (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 6821 . . . . . . . . 9 (𝑥 = 0 → (𝑀𝑥) = (𝑀↑0))
21oveq1d 6828 . . . . . . . 8 (𝑥 = 0 → ((𝑀𝑥) − 1) = ((𝑀↑0) − 1))
32oveq2d 6829 . . . . . . 7 (𝑥 = 0 → (0...((𝑀𝑥) − 1)) = (0...((𝑀↑0) − 1)))
4 oveq2 6821 . . . . . . . . 9 (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0))
5 oveq2 6821 . . . . . . . . 9 (𝑥 = 0 → (𝑇𝑥) = (𝑇↑0))
64, 5oveq12d 6831 . . . . . . . 8 (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 0) · (𝑇↑0)))
76breq2d 4816 . . . . . . 7 (𝑥 = 0 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
83, 7raleqbidv 3291 . . . . . 6 (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
98imbi2d 329 . . . . 5 (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))))
10 oveq2 6821 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑀𝑥) = (𝑀𝑛))
1110oveq1d 6828 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑀𝑥) − 1) = ((𝑀𝑛) − 1))
1211oveq2d 6829 . . . . . . 7 (𝑥 = 𝑛 → (0...((𝑀𝑥) − 1)) = (0...((𝑀𝑛) − 1)))
13 oveq2 6821 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛))
14 oveq2 6821 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑇𝑥) = (𝑇𝑛))
1513, 14oveq12d 6831 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 𝑛) · (𝑇𝑛)))
1615breq2d 4816 . . . . . . 7 (𝑥 = 𝑛 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
1712, 16raleqbidv 3291 . . . . . 6 (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
1817imbi2d 329 . . . . 5 (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))))
19 oveq2 6821 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑀𝑥) = (𝑀↑(𝑛 + 1)))
2019oveq1d 6828 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑀𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1))
2120oveq2d 6829 . . . . . . 7 (𝑥 = (𝑛 + 1) → (0...((𝑀𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1)))
22 oveq2 6821 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1)))
23 oveq2 6821 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑇𝑥) = (𝑇↑(𝑛 + 1)))
2422, 23oveq12d 6831 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
2524breq2d 4816 . . . . . . 7 (𝑥 = (𝑛 + 1) → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
2621, 25raleqbidv 3291 . . . . . 6 (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
2726imbi2d 329 . . . . 5 (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
28 oveq2 6821 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀𝑥) = (𝑀𝑋))
2928oveq1d 6828 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑀𝑥) − 1) = ((𝑀𝑋) − 1))
3029oveq2d 6829 . . . . . . 7 (𝑥 = 𝑋 → (0...((𝑀𝑥) − 1)) = (0...((𝑀𝑋) − 1)))
31 oveq2 6821 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋))
32 oveq2 6821 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑇𝑥) = (𝑇𝑋))
3331, 32oveq12d 6831 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 𝑋) · (𝑇𝑋)))
3433breq2d 4816 . . . . . . 7 (𝑥 = 𝑋 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
3530, 34raleqbidv 3291 . . . . . 6 (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
3635imbi2d 329 . . . . 5 (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))))
37 ostth2.5 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘2))
38 eluz2nn 11919 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘2) → 𝑀 ∈ ℕ)
3937, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℕ)
4039nncnd 11228 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
4140exp0d 13196 . . . . . . . . . . 11 (𝜑 → (𝑀↑0) = 1)
4241oveq1d 6828 . . . . . . . . . 10 (𝜑 → ((𝑀↑0) − 1) = (1 − 1))
43 1m1e0 11281 . . . . . . . . . 10 (1 − 1) = 0
4442, 43syl6eq 2810 . . . . . . . . 9 (𝜑 → ((𝑀↑0) − 1) = 0)
4544oveq2d 6829 . . . . . . . 8 (𝜑 → (0...((𝑀↑0) − 1)) = (0...0))
4645eleq2d 2825 . . . . . . 7 (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈ (0...0)))
47 0le0 11302 . . . . . . . . . 10 0 ≤ 0
4847a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 0)
49 ostth.1 . . . . . . . . . 10 (𝜑𝐹𝐴)
50 qabsabv.a . . . . . . . . . . 11 𝐴 = (AbsVal‘𝑄)
51 qrng.q . . . . . . . . . . . 12 𝑄 = (ℂflds ℚ)
5251qrng0 25509 . . . . . . . . . . 11 0 = (0g𝑄)
5350, 52abv0 19033 . . . . . . . . . 10 (𝐹𝐴 → (𝐹‘0) = 0)
5449, 53syl 17 . . . . . . . . 9 (𝜑 → (𝐹‘0) = 0)
5540mul01d 10427 . . . . . . . . . . 11 (𝜑 → (𝑀 · 0) = 0)
5655oveq1d 6828 . . . . . . . . . 10 (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0)))
57 ostth2.7 . . . . . . . . . . . . . 14 𝑇 = if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀))
58 1re 10231 . . . . . . . . . . . . . . 15 1 ∈ ℝ
59 nnq 11994 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
6039, 59syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℚ)
6151qrngbas 25507 . . . . . . . . . . . . . . . . 17 ℚ = (Base‘𝑄)
6250, 61abvcl 19026 . . . . . . . . . . . . . . . 16 ((𝐹𝐴𝑀 ∈ ℚ) → (𝐹𝑀) ∈ ℝ)
6349, 60, 62syl2anc 696 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑀) ∈ ℝ)
64 ifcl 4274 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝐹𝑀) ∈ ℝ) → if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)) ∈ ℝ)
6558, 63, 64sylancr 698 . . . . . . . . . . . . . 14 (𝜑 → if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)) ∈ ℝ)
6657, 65syl5eqel 2843 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℝ)
6766recnd 10260 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℂ)
68 0nn0 11499 . . . . . . . . . . . 12 0 ∈ ℕ0
69 expcl 13072 . . . . . . . . . . . 12 ((𝑇 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝑇↑0) ∈ ℂ)
7067, 68, 69sylancl 697 . . . . . . . . . . 11 (𝜑 → (𝑇↑0) ∈ ℂ)
7170mul02d 10426 . . . . . . . . . 10 (𝜑 → (0 · (𝑇↑0)) = 0)
7256, 71eqtrd 2794 . . . . . . . . 9 (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0)
7348, 54, 723brtr4d 4836 . . . . . . . 8 (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))
74 elfz1eq 12545 . . . . . . . . . 10 (𝑘 ∈ (0...0) → 𝑘 = 0)
7574fveq2d 6356 . . . . . . . . 9 (𝑘 ∈ (0...0) → (𝐹𝑘) = (𝐹‘0))
7675breq1d 4814 . . . . . . . 8 (𝑘 ∈ (0...0) → ((𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)) ↔ (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0))))
7773, 76syl5ibrcom 237 . . . . . . 7 (𝜑 → (𝑘 ∈ (0...0) → (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
7846, 77sylbid 230 . . . . . 6 (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) → (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
7978ralrimiv 3103 . . . . 5 (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))
80 fveq2 6352 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
8180breq1d 4814 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ (𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
8281cbvralv 3310 . . . . . . . 8 (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
8349ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝐹𝐴)
84 elfzelz 12535 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ)
8584ad2antrl 766 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℤ)
86 zq 11987 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → 𝑘 ∈ ℚ)
8785, 86syl 17 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℚ)
8850, 61abvcl 19026 . . . . . . . . . . . 12 ((𝐹𝐴𝑘 ∈ ℚ) → (𝐹𝑘) ∈ ℝ)
8983, 87, 88syl2anc 696 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ∈ ℝ)
9039ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℕ)
91 simplr 809 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℕ0)
9290, 91nnexpcld 13224 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℕ)
9385, 92zmodcld 12885 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℕ0)
9493nn0zd 11672 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℤ)
95 zq 11987 . . . . . . . . . . . . . 14 ((𝑘 mod (𝑀𝑛)) ∈ ℤ → (𝑘 mod (𝑀𝑛)) ∈ ℚ)
9694, 95syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℚ)
9750, 61abvcl 19026 . . . . . . . . . . . . 13 ((𝐹𝐴 ∧ (𝑘 mod (𝑀𝑛)) ∈ ℚ) → (𝐹‘(𝑘 mod (𝑀𝑛))) ∈ ℝ)
9883, 96, 97syl2anc 696 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑘 mod (𝑀𝑛))) ∈ ℝ)
9990, 59syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℚ)
10083, 99, 62syl2anc 696 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ∈ ℝ)
101100, 91reexpcld 13219 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ∈ ℝ)
10285zred 11674 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℝ)
103102, 92nndivred 11261 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 / (𝑀𝑛)) ∈ ℝ)
104103flcld 12793 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℤ)
105 zq 11987 . . . . . . . . . . . . . . 15 ((⌊‘(𝑘 / (𝑀𝑛))) ∈ ℤ → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ)
106104, 105syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ)
10750, 61abvcl 19026 . . . . . . . . . . . . . 14 ((𝐹𝐴 ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℝ)
10883, 106, 107syl2anc 696 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℝ)
109101, 108remulcld 10262 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ∈ ℝ)
11098, 109readdcld 10261 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ∈ ℝ)
11190nnred 11227 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℝ)
112 nn0p1nn 11524 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
113112ad2antlr 765 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℕ)
114113nnred 11227 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℝ)
115111, 114remulcld 10262 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ)
11666ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑇 ∈ ℝ)
117 peano2nn0 11525 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
118117ad2antlr 765 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℕ0)
119116, 118reexpcld 13219 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ)
120115, 119remulcld 10262 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ)
121 nnq 11994 . . . . . . . . . . . . . . 15 ((𝑀𝑛) ∈ ℕ → (𝑀𝑛) ∈ ℚ)
12292, 121syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℚ)
123 qmulcl 11999 . . . . . . . . . . . . . 14 (((𝑀𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ)
124122, 106, 123syl2anc 696 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ)
125 qex 11993 . . . . . . . . . . . . . . 15 ℚ ∈ V
126 cnfldadd 19953 . . . . . . . . . . . . . . . 16 + = (+g‘ℂfld)
12751, 126ressplusg 16195 . . . . . . . . . . . . . . 15 (ℚ ∈ V → + = (+g𝑄))
128125, 127ax-mp 5 . . . . . . . . . . . . . 14 + = (+g𝑄)
12950, 61, 128abvtri 19032 . . . . . . . . . . . . 13 ((𝐹𝐴 ∧ (𝑘 mod (𝑀𝑛)) ∈ ℚ ∧ ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))))
13083, 96, 124, 129syl3anc 1477 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))))
13192nnrpd 12063 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℝ+)
132 modval 12864 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℝ ∧ (𝑀𝑛) ∈ ℝ+) → (𝑘 mod (𝑀𝑛)) = (𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
133102, 131, 132syl2anc 696 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) = (𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
134133oveq1d 6828 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
135102recnd 10260 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℂ)
136 qcn 11995 . . . . . . . . . . . . . . . 16 (((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
137124, 136syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
138135, 137npcand 10588 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = 𝑘)
139134, 138eqtrd 2794 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = 𝑘)
140139fveq2d 6356 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) = (𝐹𝑘))
141 cnfldmul 19954 . . . . . . . . . . . . . . . . . 18 · = (.r‘ℂfld)
14251, 141ressmulr 16208 . . . . . . . . . . . . . . . . 17 (ℚ ∈ V → · = (.r𝑄))
143125, 142ax-mp 5 . . . . . . . . . . . . . . . 16 · = (.r𝑄)
14450, 61, 143abvmul 19031 . . . . . . . . . . . . . . 15 ((𝐹𝐴 ∧ (𝑀𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
14583, 122, 106, 144syl3anc 1477 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
14651, 50qabvexp 25514 . . . . . . . . . . . . . . . 16 ((𝐹𝐴𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑀𝑛)) = ((𝐹𝑀)↑𝑛))
14783, 99, 91, 146syl3anc 1477 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑀𝑛)) = ((𝐹𝑀)↑𝑛))
148147oveq1d 6828 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) = (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
149145, 148eqtrd 2794 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
150149oveq2d 6829 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))))
151130, 140, 1503brtr3d 4835 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))))
152116, 91reexpcld 13219 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ∈ ℝ)
153115, 152remulcld 10262 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ∈ ℝ)
154 nn0re 11493 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
155154ad2antlr 765 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℝ)
156111, 155remulcld 10262 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 𝑛) ∈ ℝ)
157156, 152remulcld 10262 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · 𝑛) · (𝑇𝑛)) ∈ ℝ)
158111, 152remulcld 10262 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑇𝑛)) ∈ ℝ)
159 fveq2 6352 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑘 mod (𝑀𝑛)) → (𝐹𝑗) = (𝐹‘(𝑘 mod (𝑀𝑛))))
160159breq1d 4814 . . . . . . . . . . . . . . 15 (𝑗 = (𝑘 mod (𝑀𝑛)) → ((𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
161 simprr 813 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
162 zmodfz 12886 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑀𝑛) ∈ ℕ) → (𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)))
16385, 92, 162syl2anc 696 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)))
164160, 161, 163rspcdva 3455 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
165111, 101remulcld 10262 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · ((𝐹𝑀)↑𝑛)) ∈ ℝ)
166101recnd 10260 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ∈ ℂ)
167108recnd 10260 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
168166, 167mulcomd 10253 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) · ((𝐹𝑀)↑𝑛)))
16950, 61abvge0 19027 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐴𝑀 ∈ ℚ) → 0 ≤ (𝐹𝑀))
17083, 99, 169syl2anc 696 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ (𝐹𝑀))
171100, 91, 170expge0d 13220 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ ((𝐹𝑀)↑𝑛))
172104zred 11674 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℝ)
173 elfzle1 12537 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘)
174173ad2antrl 766 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ 𝑘)
17592nnred 11227 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℝ)
17692nngt0d 11256 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 < (𝑀𝑛))
177 divge0 11084 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ℝ ∧ 0 ≤ 𝑘) ∧ ((𝑀𝑛) ∈ ℝ ∧ 0 < (𝑀𝑛))) → 0 ≤ (𝑘 / (𝑀𝑛)))
178102, 174, 175, 176, 177syl22anc 1478 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ (𝑘 / (𝑀𝑛)))
179 flge0nn0 12815 . . . . . . . . . . . . . . . . . . . 20 (((𝑘 / (𝑀𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀𝑛))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0)
180103, 178, 179syl2anc 696 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0)
18151, 50qabvle 25513 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐴 ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ (⌊‘(𝑘 / (𝑀𝑛))))
18283, 180, 181syl2anc 696 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ (⌊‘(𝑘 / (𝑀𝑛))))
183 simprl 811 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)))
184 0z 11580 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ ℤ
18590, 118nnexpcld 13224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ)
186185nnzd 11673 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ)
187 elfzm11 12604 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ∈ ℤ ∧ (𝑀↑(𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1)))))
188184, 186, 187sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1)))))
189183, 188mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1))))
190189simp3d 1139 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 < (𝑀↑(𝑛 + 1)))
19190nncnd 11228 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℂ)
192191, 91expp1d 13203 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀𝑛) · 𝑀))
193190, 192breqtrd 4830 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 < ((𝑀𝑛) · 𝑀))
194 ltdivmul 11090 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑀𝑛) ∈ ℝ ∧ 0 < (𝑀𝑛))) → ((𝑘 / (𝑀𝑛)) < 𝑀𝑘 < ((𝑀𝑛) · 𝑀)))
195102, 111, 175, 176, 194syl112anc 1481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 / (𝑀𝑛)) < 𝑀𝑘 < ((𝑀𝑛) · 𝑀)))
196193, 195mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 / (𝑀𝑛)) < 𝑀)
19790nnzd 11673 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℤ)
198 fllt 12801 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 / (𝑀𝑛)) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑘 / (𝑀𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀))
199103, 197, 198syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 / (𝑀𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀))
200196, 199mpbid 222 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀)
201172, 111, 200ltled 10377 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ≤ 𝑀)
202108, 172, 111, 182, 201letrd 10386 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ 𝑀)
203108, 111, 101, 171, 202lemul1ad 11155 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) · ((𝐹𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹𝑀)↑𝑛)))
204168, 203eqbrtrd 4826 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ≤ (𝑀 · ((𝐹𝑀)↑𝑛)))
20590nnnn0d 11543 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℕ0)
206205nn0ge0d 11546 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ 𝑀)
207 max1 12209 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → (𝐹𝑀) ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
208100, 58, 207sylancl 697 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
209208, 57syl6breqr 4846 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ≤ 𝑇)
210 leexp1a 13113 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ0) ∧ (0 ≤ (𝐹𝑀) ∧ (𝐹𝑀) ≤ 𝑇)) → ((𝐹𝑀)↑𝑛) ≤ (𝑇𝑛))
211100, 116, 91, 170, 209, 210syl32anc 1485 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ≤ (𝑇𝑛))
212101, 152, 111, 206, 211lemul2ad 11156 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · ((𝐹𝑀)↑𝑛)) ≤ (𝑀 · (𝑇𝑛)))
213109, 165, 158, 204, 212letrd 10386 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ≤ (𝑀 · (𝑇𝑛)))
21498, 109, 157, 158, 164, 213le2addd 10838 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
215 nn0cn 11494 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
216215ad2antlr 765 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℂ)
217 1cnd 10248 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ∈ ℂ)
218191, 216, 217adddid 10256 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1)))
219191mulid1d 10249 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 1) = 𝑀)
220219oveq2d 6829 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀))
221218, 220eqtrd 2794 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀))
222221oveq1d 6828 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇𝑛)))
223191, 216mulcld 10252 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 𝑛) ∈ ℂ)
224152recnd 10260 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ∈ ℂ)
225223, 191, 224adddird 10257 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇𝑛)) = (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
226222, 225eqtrd 2794 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) = (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
227214, 226breqtrrd 4832 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)))
228 max2 12211 . . . . . . . . . . . . . . . 16 (((𝐹𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → 1 ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
229100, 58, 228sylancl 697 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
230229, 57syl6breqr 4846 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ≤ 𝑇)
231 nn0z 11592 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
232231ad2antlr 765 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℤ)
233 uzid 11894 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
234232, 233syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ (ℤ𝑛))
235 peano2uz 11934 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ𝑛) → (𝑛 + 1) ∈ (ℤ𝑛))
236234, 235syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ (ℤ𝑛))
237116, 230, 236leexp2ad 13235 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)))
23890, 113nnmulcld 11260 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ)
239238nngt0d 11256 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 < (𝑀 · (𝑛 + 1)))
240 lemul2 11068 . . . . . . . . . . . . . 14 (((𝑇𝑛) ∈ ℝ ∧ (𝑇↑(𝑛 + 1)) ∈ ℝ ∧ ((𝑀 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑀 · (𝑛 + 1)))) → ((𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
241152, 119, 115, 239, 240syl112anc 1481 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
242237, 241mpbid 222 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
243110, 153, 120, 227, 242letrd 10386 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
24489, 110, 120, 151, 243letrd 10386 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
245244expr 644 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
246245ralrimdva 3107 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
24782, 246syl5bi 232 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
248247expcom 450 . . . . . 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 11664 . . . 4 (𝑋 ∈ ℕ0 → (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
251250impcom 445 . . 3 ((𝜑𝑋 ∈ ℕ0) → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
252 fveq2 6352 . . . . 5 (𝑘 = 𝑌 → (𝐹𝑘) = (𝐹𝑌))
253252breq1d 4814 . . . 4 (𝑘 = 𝑌 → ((𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)) ↔ (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
254253rspccv 3446 . . 3 (∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)) → (𝑌 ∈ (0...((𝑀𝑋) − 1)) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
255251, 254syl 17 . 2 ((𝜑𝑋 ∈ ℕ0) → (𝑌 ∈ (0...((𝑀𝑋) − 1)) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
2562553impia 1110 1 ((𝜑𝑋 ∈ ℕ0𝑌 ∈ (0...((𝑀𝑋) − 1))) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wral 3050  Vcvv 3340  ifcif 4230   class class class wbr 4804  cmpt 4881  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133   < clt 10266  cle 10267  cmin 10458  -cneg 10459   / cdiv 10876  cn 11212  2c2 11262  0cn0 11484  cz 11569  cuz 11879  cq 11981  +crp 12025  ...cfz 12519  cfl 12785   mod cmo 12862  cexp 13054  cprime 15587   pCnt cpc 15743  s cress 16060  +gcplusg 16143  .rcmulr 16144  AbsValcabv 19018  fldccnfld 19948  logclog 24500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-tpos 7521  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-inf 8514  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-ico 12374  df-fz 12520  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-0g 16304  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-grp 17626  df-minusg 17627  df-subg 17792  df-cmn 18395  df-mgp 18690  df-ur 18702  df-ring 18749  df-cring 18750  df-oppr 18823  df-dvdsr 18841  df-unit 18842  df-invr 18872  df-dvr 18883  df-drng 18951  df-subrg 18980  df-abv 19019  df-cnfld 19949
This theorem is referenced by:  ostth2lem3  25523
  Copyright terms: Public domain W3C validator