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

Theorem ostth2lem2 27612
Description: Lemma for ostth2 27615. (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 7427 . . . . . . . . 9 (𝑥 = 0 → (𝑀𝑥) = (𝑀↑0))
21oveq1d 7434 . . . . . . . 8 (𝑥 = 0 → ((𝑀𝑥) − 1) = ((𝑀↑0) − 1))
32oveq2d 7435 . . . . . . 7 (𝑥 = 0 → (0...((𝑀𝑥) − 1)) = (0...((𝑀↑0) − 1)))
4 oveq2 7427 . . . . . . . . 9 (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0))
5 oveq2 7427 . . . . . . . . 9 (𝑥 = 0 → (𝑇𝑥) = (𝑇↑0))
64, 5oveq12d 7437 . . . . . . . 8 (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 0) · (𝑇↑0)))
76breq2d 5161 . . . . . . 7 (𝑥 = 0 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
83, 7raleqbidv 3329 . . . . . 6 (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
98imbi2d 339 . . . . 5 (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))))
10 oveq2 7427 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑀𝑥) = (𝑀𝑛))
1110oveq1d 7434 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑀𝑥) − 1) = ((𝑀𝑛) − 1))
1211oveq2d 7435 . . . . . . 7 (𝑥 = 𝑛 → (0...((𝑀𝑥) − 1)) = (0...((𝑀𝑛) − 1)))
13 oveq2 7427 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛))
14 oveq2 7427 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑇𝑥) = (𝑇𝑛))
1513, 14oveq12d 7437 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 𝑛) · (𝑇𝑛)))
1615breq2d 5161 . . . . . . 7 (𝑥 = 𝑛 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
1712, 16raleqbidv 3329 . . . . . 6 (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
1817imbi2d 339 . . . . 5 (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))))
19 oveq2 7427 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑀𝑥) = (𝑀↑(𝑛 + 1)))
2019oveq1d 7434 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑀𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1))
2120oveq2d 7435 . . . . . . 7 (𝑥 = (𝑛 + 1) → (0...((𝑀𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1)))
22 oveq2 7427 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1)))
23 oveq2 7427 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑇𝑥) = (𝑇↑(𝑛 + 1)))
2422, 23oveq12d 7437 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
2524breq2d 5161 . . . . . . 7 (𝑥 = (𝑛 + 1) → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
2621, 25raleqbidv 3329 . . . . . 6 (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
2726imbi2d 339 . . . . 5 (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
28 oveq2 7427 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀𝑥) = (𝑀𝑋))
2928oveq1d 7434 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑀𝑥) − 1) = ((𝑀𝑋) − 1))
3029oveq2d 7435 . . . . . . 7 (𝑥 = 𝑋 → (0...((𝑀𝑥) − 1)) = (0...((𝑀𝑋) − 1)))
31 oveq2 7427 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋))
32 oveq2 7427 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑇𝑥) = (𝑇𝑋))
3331, 32oveq12d 7437 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 𝑋) · (𝑇𝑋)))
3433breq2d 5161 . . . . . . 7 (𝑥 = 𝑋 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
3530, 34raleqbidv 3329 . . . . . 6 (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
3635imbi2d 339 . . . . 5 (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))))
37 ostth2.5 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘2))
38 eluz2nn 12901 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘2) → 𝑀 ∈ ℕ)
3937, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℕ)
4039nncnd 12261 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
4140exp0d 14140 . . . . . . . . . . 11 (𝜑 → (𝑀↑0) = 1)
4241oveq1d 7434 . . . . . . . . . 10 (𝜑 → ((𝑀↑0) − 1) = (1 − 1))
43 1m1e0 12317 . . . . . . . . . 10 (1 − 1) = 0
4442, 43eqtrdi 2781 . . . . . . . . 9 (𝜑 → ((𝑀↑0) − 1) = 0)
4544oveq2d 7435 . . . . . . . 8 (𝜑 → (0...((𝑀↑0) − 1)) = (0...0))
4645eleq2d 2811 . . . . . . 7 (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈ (0...0)))
47 0le0 12346 . . . . . . . . . 10 0 ≤ 0
4847a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 0)
49 ostth.1 . . . . . . . . . 10 (𝜑𝐹𝐴)
50 qabsabv.a . . . . . . . . . . 11 𝐴 = (AbsVal‘𝑄)
51 qrng.q . . . . . . . . . . . 12 𝑄 = (ℂflds ℚ)
5251qrng0 27599 . . . . . . . . . . 11 0 = (0g𝑄)
5350, 52abv0 20723 . . . . . . . . . 10 (𝐹𝐴 → (𝐹‘0) = 0)
5449, 53syl 17 . . . . . . . . 9 (𝜑 → (𝐹‘0) = 0)
5540mul01d 11445 . . . . . . . . . . 11 (𝜑 → (𝑀 · 0) = 0)
5655oveq1d 7434 . . . . . . . . . 10 (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0)))
57 ostth2.7 . . . . . . . . . . . . . 14 𝑇 = if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀))
58 1re 11246 . . . . . . . . . . . . . . 15 1 ∈ ℝ
59 nnq 12979 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
6039, 59syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℚ)
6151qrngbas 27597 . . . . . . . . . . . . . . . . 17 ℚ = (Base‘𝑄)
6250, 61abvcl 20716 . . . . . . . . . . . . . . . 16 ((𝐹𝐴𝑀 ∈ ℚ) → (𝐹𝑀) ∈ ℝ)
6349, 60, 62syl2anc 582 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑀) ∈ ℝ)
64 ifcl 4575 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝐹𝑀) ∈ ℝ) → if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)) ∈ ℝ)
6558, 63, 64sylancr 585 . . . . . . . . . . . . . 14 (𝜑 → if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)) ∈ ℝ)
6657, 65eqeltrid 2829 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℝ)
6766recnd 11274 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℂ)
68 0nn0 12520 . . . . . . . . . . . 12 0 ∈ ℕ0
69 expcl 14080 . . . . . . . . . . . 12 ((𝑇 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝑇↑0) ∈ ℂ)
7067, 68, 69sylancl 584 . . . . . . . . . . 11 (𝜑 → (𝑇↑0) ∈ ℂ)
7170mul02d 11444 . . . . . . . . . 10 (𝜑 → (0 · (𝑇↑0)) = 0)
7256, 71eqtrd 2765 . . . . . . . . 9 (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0)
7348, 54, 723brtr4d 5181 . . . . . . . 8 (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))
74 elfz1eq 13547 . . . . . . . . . 10 (𝑘 ∈ (0...0) → 𝑘 = 0)
7574fveq2d 6900 . . . . . . . . 9 (𝑘 ∈ (0...0) → (𝐹𝑘) = (𝐹‘0))
7675breq1d 5159 . . . . . . . 8 (𝑘 ∈ (0...0) → ((𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)) ↔ (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0))))
7773, 76syl5ibrcom 246 . . . . . . 7 (𝜑 → (𝑘 ∈ (0...0) → (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
7846, 77sylbid 239 . . . . . 6 (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) → (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
7978ralrimiv 3134 . . . . 5 (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))
80 fveq2 6896 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
8180breq1d 5159 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ (𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
8281cbvralvw 3224 . . . . . . . 8 (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
8349ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝐹𝐴)
84 elfzelz 13536 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ)
8584ad2antrl 726 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℤ)
86 zq 12971 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → 𝑘 ∈ ℚ)
8785, 86syl 17 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℚ)
8850, 61abvcl 20716 . . . . . . . . . . . 12 ((𝐹𝐴𝑘 ∈ ℚ) → (𝐹𝑘) ∈ ℝ)
8983, 87, 88syl2anc 582 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ∈ ℝ)
9039ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℕ)
91 simplr 767 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℕ0)
9290, 91nnexpcld 14243 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℕ)
9385, 92zmodcld 13893 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℕ0)
9493nn0zd 12617 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℤ)
95 zq 12971 . . . . . . . . . . . . . 14 ((𝑘 mod (𝑀𝑛)) ∈ ℤ → (𝑘 mod (𝑀𝑛)) ∈ ℚ)
9694, 95syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℚ)
9750, 61abvcl 20716 . . . . . . . . . . . . 13 ((𝐹𝐴 ∧ (𝑘 mod (𝑀𝑛)) ∈ ℚ) → (𝐹‘(𝑘 mod (𝑀𝑛))) ∈ ℝ)
9883, 96, 97syl2anc 582 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑘 mod (𝑀𝑛))) ∈ ℝ)
9990, 59syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℚ)
10083, 99, 62syl2anc 582 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ∈ ℝ)
101100, 91reexpcld 14163 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ∈ ℝ)
10285zred 12699 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℝ)
103102, 92nndivred 12299 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 / (𝑀𝑛)) ∈ ℝ)
104103flcld 13799 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℤ)
105 zq 12971 . . . . . . . . . . . . . . 15 ((⌊‘(𝑘 / (𝑀𝑛))) ∈ ℤ → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ)
106104, 105syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ)
10750, 61abvcl 20716 . . . . . . . . . . . . . 14 ((𝐹𝐴 ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℝ)
10883, 106, 107syl2anc 582 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℝ)
109101, 108remulcld 11276 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ∈ ℝ)
11098, 109readdcld 11275 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ∈ ℝ)
11190nnred 12260 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℝ)
112 nn0p1nn 12544 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
113112ad2antlr 725 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℕ)
114113nnred 12260 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℝ)
115111, 114remulcld 11276 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ)
11666ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑇 ∈ ℝ)
117 peano2nn0 12545 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
118117ad2antlr 725 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℕ0)
119116, 118reexpcld 14163 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ)
120115, 119remulcld 11276 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ)
121 nnq 12979 . . . . . . . . . . . . . . 15 ((𝑀𝑛) ∈ ℕ → (𝑀𝑛) ∈ ℚ)
12292, 121syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℚ)
123 qmulcl 12984 . . . . . . . . . . . . . 14 (((𝑀𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ)
124122, 106, 123syl2anc 582 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ)
125 qex 12978 . . . . . . . . . . . . . . 15 ℚ ∈ V
126 cnfldadd 21302 . . . . . . . . . . . . . . . 16 + = (+g‘ℂfld)
12751, 126ressplusg 17274 . . . . . . . . . . . . . . 15 (ℚ ∈ V → + = (+g𝑄))
128125, 127ax-mp 5 . . . . . . . . . . . . . 14 + = (+g𝑄)
12950, 61, 128abvtri 20722 . . . . . . . . . . . . 13 ((𝐹𝐴 ∧ (𝑘 mod (𝑀𝑛)) ∈ ℚ ∧ ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))))
13083, 96, 124, 129syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))))
13192nnrpd 13049 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℝ+)
132 modval 13872 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℝ ∧ (𝑀𝑛) ∈ ℝ+) → (𝑘 mod (𝑀𝑛)) = (𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
133102, 131, 132syl2anc 582 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) = (𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
134133oveq1d 7434 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
135102recnd 11274 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℂ)
136 qcn 12980 . . . . . . . . . . . . . . . 16 (((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
137124, 136syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
138135, 137npcand 11607 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = 𝑘)
139134, 138eqtrd 2765 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = 𝑘)
140139fveq2d 6900 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) = (𝐹𝑘))
141 cnfldmul 21304 . . . . . . . . . . . . . . . . . 18 · = (.r‘ℂfld)
14251, 141ressmulr 17291 . . . . . . . . . . . . . . . . 17 (ℚ ∈ V → · = (.r𝑄))
143125, 142ax-mp 5 . . . . . . . . . . . . . . . 16 · = (.r𝑄)
14450, 61, 143abvmul 20721 . . . . . . . . . . . . . . 15 ((𝐹𝐴 ∧ (𝑀𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
14583, 122, 106, 144syl3anc 1368 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
14651, 50qabvexp 27604 . . . . . . . . . . . . . . . 16 ((𝐹𝐴𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑀𝑛)) = ((𝐹𝑀)↑𝑛))
14783, 99, 91, 146syl3anc 1368 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑀𝑛)) = ((𝐹𝑀)↑𝑛))
148147oveq1d 7434 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) = (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
149145, 148eqtrd 2765 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
150149oveq2d 7435 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))))
151130, 140, 1503brtr3d 5180 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))))
152116, 91reexpcld 14163 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ∈ ℝ)
153115, 152remulcld 11276 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ∈ ℝ)
154 nn0re 12514 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
155154ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℝ)
156111, 155remulcld 11276 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 𝑛) ∈ ℝ)
157156, 152remulcld 11276 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · 𝑛) · (𝑇𝑛)) ∈ ℝ)
158111, 152remulcld 11276 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑇𝑛)) ∈ ℝ)
159 fveq2 6896 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑘 mod (𝑀𝑛)) → (𝐹𝑗) = (𝐹‘(𝑘 mod (𝑀𝑛))))
160159breq1d 5159 . . . . . . . . . . . . . . 15 (𝑗 = (𝑘 mod (𝑀𝑛)) → ((𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
161 simprr 771 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
162 zmodfz 13894 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑀𝑛) ∈ ℕ) → (𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)))
16385, 92, 162syl2anc 582 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)))
164160, 161, 163rspcdva 3607 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
165111, 101remulcld 11276 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · ((𝐹𝑀)↑𝑛)) ∈ ℝ)
166101recnd 11274 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ∈ ℂ)
167108recnd 11274 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
168166, 167mulcomd 11267 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) · ((𝐹𝑀)↑𝑛)))
16950, 61abvge0 20717 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐴𝑀 ∈ ℚ) → 0 ≤ (𝐹𝑀))
17083, 99, 169syl2anc 582 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ (𝐹𝑀))
171100, 91, 170expge0d 14164 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ ((𝐹𝑀)↑𝑛))
172104zred 12699 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℝ)
173 elfzle1 13539 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘)
174173ad2antrl 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ 𝑘)
17592nnred 12260 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℝ)
17692nngt0d 12294 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 < (𝑀𝑛))
177 divge0 12116 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ℝ ∧ 0 ≤ 𝑘) ∧ ((𝑀𝑛) ∈ ℝ ∧ 0 < (𝑀𝑛))) → 0 ≤ (𝑘 / (𝑀𝑛)))
178102, 174, 175, 176, 177syl22anc 837 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ (𝑘 / (𝑀𝑛)))
179 flge0nn0 13821 . . . . . . . . . . . . . . . . . . . 20 (((𝑘 / (𝑀𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀𝑛))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0)
180103, 178, 179syl2anc 582 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0)
18151, 50qabvle 27603 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐴 ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ (⌊‘(𝑘 / (𝑀𝑛))))
18283, 180, 181syl2anc 582 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ (⌊‘(𝑘 / (𝑀𝑛))))
183 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)))
184 0z 12602 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ ℤ
18590, 118nnexpcld 14243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ)
186185nnzd 12618 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ)
187 elfzm11 13607 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ∈ ℤ ∧ (𝑀↑(𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1)))))
188184, 186, 187sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1)))))
189183, 188mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1))))
190189simp3d 1141 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 < (𝑀↑(𝑛 + 1)))
19190nncnd 12261 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℂ)
192191, 91expp1d 14147 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀𝑛) · 𝑀))
193190, 192breqtrd 5175 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 < ((𝑀𝑛) · 𝑀))
194 ltdivmul 12122 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑀𝑛) ∈ ℝ ∧ 0 < (𝑀𝑛))) → ((𝑘 / (𝑀𝑛)) < 𝑀𝑘 < ((𝑀𝑛) · 𝑀)))
195102, 111, 175, 176, 194syl112anc 1371 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 / (𝑀𝑛)) < 𝑀𝑘 < ((𝑀𝑛) · 𝑀)))
196193, 195mpbird 256 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 / (𝑀𝑛)) < 𝑀)
19790nnzd 12618 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℤ)
198 fllt 13807 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 / (𝑀𝑛)) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑘 / (𝑀𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀))
199103, 197, 198syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 / (𝑀𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀))
200196, 199mpbid 231 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀)
201172, 111, 200ltled 11394 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ≤ 𝑀)
202108, 172, 111, 182, 201letrd 11403 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ 𝑀)
203108, 111, 101, 171, 202lemul1ad 12186 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) · ((𝐹𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹𝑀)↑𝑛)))
204168, 203eqbrtrd 5171 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ≤ (𝑀 · ((𝐹𝑀)↑𝑛)))
20590nnnn0d 12565 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℕ0)
206205nn0ge0d 12568 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ 𝑀)
207 max1 13199 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → (𝐹𝑀) ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
208100, 58, 207sylancl 584 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
209208, 57breqtrrdi 5191 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ≤ 𝑇)
210 leexp1a 14175 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ0) ∧ (0 ≤ (𝐹𝑀) ∧ (𝐹𝑀) ≤ 𝑇)) → ((𝐹𝑀)↑𝑛) ≤ (𝑇𝑛))
211100, 116, 91, 170, 209, 210syl32anc 1375 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ≤ (𝑇𝑛))
212101, 152, 111, 206, 211lemul2ad 12187 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · ((𝐹𝑀)↑𝑛)) ≤ (𝑀 · (𝑇𝑛)))
213109, 165, 158, 204, 212letrd 11403 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ≤ (𝑀 · (𝑇𝑛)))
21498, 109, 157, 158, 164, 213le2addd 11865 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
215 nn0cn 12515 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
216215ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℂ)
217 1cnd 11241 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ∈ ℂ)
218191, 216, 217adddid 11270 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1)))
219191mulridd 11263 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 1) = 𝑀)
220219oveq2d 7435 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀))
221218, 220eqtrd 2765 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀))
222221oveq1d 7434 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇𝑛)))
223191, 216mulcld 11266 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 𝑛) ∈ ℂ)
224152recnd 11274 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ∈ ℂ)
225223, 191, 224adddird 11271 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇𝑛)) = (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
226222, 225eqtrd 2765 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) = (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
227214, 226breqtrrd 5177 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)))
228 max2 13201 . . . . . . . . . . . . . . . 16 (((𝐹𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → 1 ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
229100, 58, 228sylancl 584 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
230229, 57breqtrrdi 5191 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ≤ 𝑇)
231 nn0z 12616 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
232231ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℤ)
233 uzid 12870 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
234232, 233syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ (ℤ𝑛))
235 peano2uz 12918 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ𝑛) → (𝑛 + 1) ∈ (ℤ𝑛))
236234, 235syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ (ℤ𝑛))
237116, 230, 236leexp2ad 14252 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)))
23890, 113nnmulcld 12298 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ)
239238nngt0d 12294 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 < (𝑀 · (𝑛 + 1)))
240 lemul2 12100 . . . . . . . . . . . . . 14 (((𝑇𝑛) ∈ ℝ ∧ (𝑇↑(𝑛 + 1)) ∈ ℝ ∧ ((𝑀 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑀 · (𝑛 + 1)))) → ((𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
241152, 119, 115, 239, 240syl112anc 1371 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
242237, 241mpbid 231 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
243110, 153, 120, 227, 242letrd 11403 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
24489, 110, 120, 151, 243letrd 11403 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
245244expr 455 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
246245ralrimdva 3143 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
24782, 246biimtrid 241 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
248247expcom 412 . . . . . 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 12690 . . . 4 (𝑋 ∈ ℕ0 → (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
251250impcom 406 . . 3 ((𝜑𝑋 ∈ ℕ0) → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
252 fveq2 6896 . . . . 5 (𝑘 = 𝑌 → (𝐹𝑘) = (𝐹𝑌))
253252breq1d 5159 . . . 4 (𝑘 = 𝑌 → ((𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)) ↔ (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
254253rspccv 3603 . . 3 (∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)) → (𝑌 ∈ (0...((𝑀𝑋) − 1)) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
255251, 254syl 17 . 2 ((𝜑𝑋 ∈ ℕ0) → (𝑌 ∈ (0...((𝑀𝑋) − 1)) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
2562553impia 1114 1 ((𝜑𝑋 ∈ ℕ0𝑌 ∈ (0...((𝑀𝑋) − 1))) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3050  Vcvv 3461  ifcif 4530   class class class wbr 5149  cmpt 5232  cfv 6549  (class class class)co 7419  cc 11138  cr 11139  0cc0 11140  1c1 11141   + caddc 11143   · cmul 11145   < clt 11280  cle 11281  cmin 11476  -cneg 11477   / cdiv 11903  cn 12245  2c2 12300  0cn0 12505  cz 12591  cuz 12855  cq 12965  +crp 13009  ...cfz 13519  cfl 13791   mod cmo 13870  cexp 14062  cprime 16645   pCnt cpc 16808  s cress 17212  +gcplusg 17236  .rcmulr 17237  AbsValcabv 20708  fldccnfld 21296  logclog 26533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-pre-sup 11218  ax-addf 11219  ax-mulf 11220
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-tpos 8232  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9467  df-inf 9468  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12506  df-z 12592  df-dec 12711  df-uz 12856  df-q 12966  df-rp 13010  df-ico 13365  df-fz 13520  df-fl 13793  df-mod 13871  df-seq 14003  df-exp 14063  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-mulr 17250  df-starv 17251  df-tset 17255  df-ple 17256  df-ds 17258  df-unif 17259  df-0g 17426  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-grp 18901  df-minusg 18902  df-subg 19086  df-cmn 19749  df-abl 19750  df-mgp 20087  df-rng 20105  df-ur 20134  df-ring 20187  df-cring 20188  df-oppr 20285  df-dvdsr 20308  df-unit 20309  df-invr 20339  df-dvr 20352  df-subrng 20495  df-subrg 20520  df-drng 20638  df-abv 20709  df-cnfld 21297
This theorem is referenced by:  ostth2lem3  27613
  Copyright terms: Public domain W3C validator