ostth2lem2 - Metamath Proof Explorer

	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	⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
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...((𝑀↑𝑋) − 1))) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))

Distinct variable groups: 𝑥,𝑀 𝑥,𝑞,𝜑 𝑥,𝑇 𝑥,𝑋 𝐴,𝑞,𝑥 𝑥,𝑁 𝑥,𝑄 𝐹,𝑞 𝑅,𝑞 𝑥,𝐹 Allowed substitution hints: 𝑄(𝑞) 𝑅(𝑥) 𝑆(𝑥,𝑞) 𝑇(𝑞) 𝐽(𝑥,𝑞) 𝐾(𝑥,𝑞) 𝑀(𝑞) 𝑁(𝑞) 𝑋(𝑞) 𝑌(𝑥,𝑞)

Proof of Theorem ostth2lem2 Dummy variables 𝑘 𝑛 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑀↑𝑥) = (𝑀↑0))
2	1	oveq1d 6937	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝑀↑𝑥) − 1) = ((𝑀↑0) − 1))
3	2	oveq2d 6938	. . . . . . 7 ⊢ (𝑥 = 0 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑0) − 1)))
4		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0))
5		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑇↑𝑥) = (𝑇↑0))
6	4, 5	oveq12d 6940	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 0) · (𝑇↑0)))
7	6	breq2d 4898	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
8	3, 7	raleqbidv 3326	. . . . . 6 ⊢ (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
9	8	imbi2d 332	. . . . 5 ⊢ (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))))
10		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑀↑𝑥) = (𝑀↑𝑛))
11	10	oveq1d 6937	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑛) − 1))
12	11	oveq2d 6938	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑛) − 1)))
13		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛))
14		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑇↑𝑥) = (𝑇↑𝑛))
15	13, 14	oveq12d 6940	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑛) · (𝑇↑𝑛)))
16	15	breq2d 4898	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
17	12, 16	raleqbidv 3326	. . . . . 6 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
18	17	imbi2d 332	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))))
19		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑀↑𝑥) = (𝑀↑(𝑛 + 1)))
20	19	oveq1d 6937	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → ((𝑀↑𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1))
21	20	oveq2d 6938	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1)))
22		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1)))
23		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑇↑𝑥) = (𝑇↑(𝑛 + 1)))
24	22, 23	oveq12d 6940	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
25	24	breq2d 4898	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
26	21, 25	raleqbidv 3326	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
27	26	imbi2d 332	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
28		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀↑𝑥) = (𝑀↑𝑋))
29	28	oveq1d 6937	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑋) − 1))
30	29	oveq2d 6938	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑋) − 1)))
31		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋))
32		oveq2 6930	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑇↑𝑥) = (𝑇↑𝑋))
33	31, 32	oveq12d 6940	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑋) · (𝑇↑𝑋)))
34	33	breq2d 4898	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
35	30, 34	raleqbidv 3326	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
36	35	imbi2d 332	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))))
37		ostth2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘2))
38		eluz2nn 12032	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℕ)
39	37, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
40	39	nncnd 11392	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℂ)
41	40	exp0d 13321	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑0) = 1)
42	41	oveq1d 6937	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀↑0) − 1) = (1 − 1))
43		1m1e0 11447	. . . . . . . . . 10 ⊢ (1 − 1) = 0
44	42, 43	syl6eq 2830	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀↑0) − 1) = 0)
45	44	oveq2d 6938	. . . . . . . 8 ⊢ (𝜑 → (0...((𝑀↑0) − 1)) = (0...0))
46	45	eleq2d 2845	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈ (0...0)))
47		0le0 11483	. . . . . . . . . 10 ⊢ 0 ≤ 0
48	47	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 0)
49		ostth.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ 𝐴)
50		qabsabv.a	. . . . . . . . . . 11 ⊢ 𝐴 = (AbsVal‘𝑄)
51		qrng.q	. . . . . . . . . . . 12 ⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
52	51	qrng0 25762	. . . . . . . . . . 11 ⊢ 0 = (0_g‘𝑄)
53	50, 52	abv0 19223	. . . . . . . . . 10 ⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0)
54	49, 53	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) = 0)
55	40	mul01d 10575	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · 0) = 0)
56	55	oveq1d 6937	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0)))
57		ostth2.7	. . . . . . . . . . . . . 14 ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))
58		1re 10376	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
59		nnq 12109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
60	39, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℚ)
61	51	qrngbas 25760	. . . . . . . . . . . . . . . . 17 ⊢ ℚ = (Base‘𝑄)
62	50, 61	abvcl 19216	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℝ)
63	49, 60, 62	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ)
64		ifcl 4351	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (𝐹‘𝑀) ∈ ℝ) → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ)
65	58, 63, 64	sylancr 581	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ)
66	57, 65	syl5eqel 2863	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ ℝ)
67	66	recnd 10405	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
68		0nn0 11659	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ₀
69		expcl 13196	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 0 ∈ ℕ₀) → (𝑇↑0) ∈ ℂ)
70	67, 68, 69	sylancl 580	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇↑0) ∈ ℂ)
71	70	mul02d 10574	. . . . . . . . . 10 ⊢ (𝜑 → (0 · (𝑇↑0)) = 0)
72	56, 71	eqtrd 2814	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0)
73	48, 54, 72	3brtr4d 4918	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))
74		elfz1eq 12669	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...0) → 𝑘 = 0)
75	74	fveq2d 6450	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...0) → (𝐹‘𝑘) = (𝐹‘0))
76	75	breq1d 4896	. . . . . . . 8 ⊢ (𝑘 ∈ (0...0) → ((𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)) ↔ (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0))))
77	73, 76	syl5ibrcom 239	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (0...0) → (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
78	46, 77	sylbid 232	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) → (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
79	78	ralrimiv 3147	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))
80		fveq2 6446	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗))
81	80	breq1d 4896	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
82	81	cbvralv 3367	. . . . . . . 8 ⊢ (∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
83	49	ad2antrr 716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝐹 ∈ 𝐴)
84		elfzelz 12659	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ)
85	84	ad2antrl 718	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℤ)
86		zq 12101	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℚ)
87	85, 86	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℚ)
88	50, 61	abvcl 19216	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑘 ∈ ℚ) → (𝐹‘𝑘) ∈ ℝ)
89	83, 87, 88	syl2anc 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ∈ ℝ)
90	39	ad2antrr 716	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℕ)
91		simplr 759	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℕ₀)
92	90, 91	nnexpcld 13351	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℕ)
93	85, 92	zmodcld 13010	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℕ₀)
94	93	nn0zd 11832	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℤ)
95		zq 12101	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod (𝑀↑𝑛)) ∈ ℤ → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ)
96	94, 95	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ)
97	50, 61	abvcl 19216	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ∈ ℝ)
98	83, 96, 97	syl2anc 579	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ∈ ℝ)
99	90, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℚ)
100	83, 99, 62	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ∈ ℝ)
101	100, 91	reexpcld 13344	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℝ)
102	85	zred 11834	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℝ)
103	102, 92	nndivred 11429	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) ∈ ℝ)
104	103	flcld 12918	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ)
105		zq 12101	. . . . . . . . . . . . . . 15 ⊢ ((⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ)
106	104, 105	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ)
107	50, 61	abvcl 19216	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ)
108	83, 106, 107	syl2anc 579	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ)
109	101, 108	remulcld 10407	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ∈ ℝ)
110	98, 109	readdcld 10406	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ∈ ℝ)
111	90	nnred 11391	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℝ)
112		nn0p1nn 11683	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
113	112	ad2antlr 717	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ)
114	113	nnred 11391	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℝ)
115	111, 114	remulcld 10407	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ)
116	66	ad2antrr 716	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑇 ∈ ℝ)
117		peano2nn0 11684	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ₀)
118	117	ad2antlr 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ₀)
119	116, 118	reexpcld 13344	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ)
120	115, 119	remulcld 10407	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ)
121		nnq 12109	. . . . . . . . . . . . . . 15 ⊢ ((𝑀↑𝑛) ∈ ℕ → (𝑀↑𝑛) ∈ ℚ)
122	92, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℚ)
123		qmulcl 12114	. . . . . . . . . . . . . 14 ⊢ (((𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ)
124	122, 106, 123	syl2anc 579	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ)
125		qex 12108	. . . . . . . . . . . . . . 15 ⊢ ℚ ∈ V
126		cnfldadd 20147	. . . . . . . . . . . . . . . 16 ⊢ + = (+_g‘ℂ_fld)
127	51, 126	ressplusg 16385	. . . . . . . . . . . . . . 15 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ + = (+_g‘𝑄)
129	50, 61, 128	abvtri 19222	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ ∧ ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))))
130	83, 96, 124, 129	syl3anc 1439	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))))
131	92	nnrpd 12179	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ⁺)
132		modval 12989	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℝ ∧ (𝑀↑𝑛) ∈ ℝ⁺) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
133	102, 131, 132	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
134	133	oveq1d 6937	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
135	102	recnd 10405	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℂ)
136		qcn 12110	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
137	124, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
138	135, 137	npcand 10738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘)
139	134, 138	eqtrd 2814	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘)
140	139	fveq2d 6450	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = (𝐹‘𝑘))
141		cnfldmul 20148	. . . . . . . . . . . . . . . . . 18 ⊢ · = (._r‘ℂ_fld)
142	51, 141	ressmulr 16398	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ · = (._r‘𝑄)
144	50, 61, 143	abvmul 19221	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
145	83, 122, 106, 144	syl3anc 1439	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
146	51, 50	qabvexp 25767	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ₀) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))
147	83, 99, 91, 146	syl3anc 1439	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))
148	147	oveq1d 6937	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
149	145, 148	eqtrd 2814	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
150	149	oveq2d 6938	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))))
151	130, 140, 150	3brtr3d 4917	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))))
152	116, 91	reexpcld 13344	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℝ)
153	115, 152	remulcld 10407	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ∈ ℝ)
154		nn0re 11652	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
155	154	ad2antlr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℝ)
156	111, 155	remulcld 10407	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℝ)
157	156, 152	remulcld 10407	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) · (𝑇↑𝑛)) ∈ ℝ)
158	111, 152	remulcld 10407	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑇↑𝑛)) ∈ ℝ)
159		fveq2 6446	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → (𝐹‘𝑗) = (𝐹‘(𝑘 mod (𝑀↑𝑛))))
160	159	breq1d 4896	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → ((𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
161		simprr 763	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
162		zmodfz 13011	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ (𝑀↑𝑛) ∈ ℕ) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1)))
163	85, 92, 162	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1)))
164	160, 161, 163	rspcdva 3517	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
165	111, 101	remulcld 10407	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ∈ ℝ)
166	101	recnd 10405	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℂ)
167	108	recnd 10405	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
168	166, 167	mulcomd 10398	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)))
169	50, 61	abvge0 19217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → 0 ≤ (𝐹‘𝑀))
170	83, 99, 169	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝐹‘𝑀))
171	100, 91, 170	expge0d 13345	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ ((𝐹‘𝑀)↑𝑛))
172	104	zred 11834	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℝ)
173		elfzle1 12661	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘)
174	173	ad2antrl 718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑘)
175	92	nnred 11391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ)
176	92	nngt0d 11424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀↑𝑛))
177		divge0 11246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ℝ ∧ 0 ≤ 𝑘) ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → 0 ≤ (𝑘 / (𝑀↑𝑛)))
178	102, 174, 175, 176, 177	syl22anc 829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝑘 / (𝑀↑𝑛)))
179		flge0nn0 12940	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀↑𝑛))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀)
180	103, 178, 179	syl2anc 579	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀)
181	51, 50	qabvle 25766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ (⌊‘(𝑘 / (𝑀↑𝑛))))
182	83, 180, 181	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ (⌊‘(𝑘 / (𝑀↑𝑛))))
183		simprl 761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)))
184		0z 11739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℤ
185	90, 118	nnexpcld 13351	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ)
186	185	nnzd 11833	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ)
187		elfzm11 12729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 ∈ ℤ ∧ (𝑀↑(𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1)))))
188	184, 186, 187	sylancr 581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1)))))
189	183, 188	mpbid 224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1))))
190	189	simp3d 1135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < (𝑀↑(𝑛 + 1)))
191	90	nncnd 11392	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℂ)
192	191, 91	expp1d 13328	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀↑𝑛) · 𝑀))
193	190, 192	breqtrd 4912	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < ((𝑀↑𝑛) · 𝑀))
194		ltdivmul 11252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ 𝑘 < ((𝑀↑𝑛) · 𝑀)))
195	102, 111, 175, 176, 194	syl112anc 1442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ 𝑘 < ((𝑀↑𝑛) · 𝑀)))
196	193, 195	mpbird 249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) < 𝑀)
197	90	nnzd 11833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℤ)
198		fllt 12926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀))
199	103, 197, 198	syl2anc 579	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀))
200	196, 199	mpbid 224	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀)
201	172, 111, 200	ltled 10524	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ≤ 𝑀)
202	108, 172, 111, 182, 201	letrd 10533	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ 𝑀)
203	108, 111, 101, 171, 202	lemul1ad 11317	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛)))
204	168, 203	eqbrtrd 4908	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛)))
205	90	nnnn0d 11702	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℕ₀)
206	205	nn0ge0d 11705	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑀)
207		max1 12328	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
208	100, 58, 207	sylancl 580	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
209	208, 57	syl6breqr 4928	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ 𝑇)
210		leexp1a 13237	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) ∧ (0 ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ 𝑇)) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛))
211	100, 116, 91, 170, 209, 210	syl32anc 1446	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛))
212	101, 152, 111, 206, 211	lemul2ad 11318	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · (𝑇↑𝑛)))
213	109, 165, 158, 204, 212	letrd 10533	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · (𝑇↑𝑛)))
214	98, 109, 157, 158, 164, 213	le2addd 10994	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
215		nn0cn 11653	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
216	215	ad2antlr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℂ)
217		1cnd 10371	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ∈ ℂ)
218	191, 216, 217	adddid 10401	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1)))
219	191	mulid1d 10394	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 1) = 𝑀)
220	219	oveq2d 6938	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀))
221	218, 220	eqtrd 2814	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀))
222	221	oveq1d 6937	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)))
223	191, 216	mulcld 10397	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℂ)
224	152	recnd 10405	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℂ)
225	223, 191, 224	adddird 10402	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
226	222, 225	eqtrd 2814	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
227	214, 226	breqtrrd 4914	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)))
228		max2 12330	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
229	100, 58, 228	sylancl 580	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
230	229, 57	syl6breqr 4928	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ 𝑇)
231		nn0z 11752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℤ)
232	231	ad2antlr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℤ)
233		uzid 12007	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ_≥‘𝑛))
234	232, 233	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ (ℤ_≥‘𝑛))
235		peano2uz 12047	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘𝑛) → (𝑛 + 1) ∈ (ℤ_≥‘𝑛))
236	234, 235	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ (ℤ_≥‘𝑛))
237	116, 230, 236	leexp2ad 13362	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)))
238	90, 113	nnmulcld 11428	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ)
239	238	nngt0d 11424	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀 · (𝑛 + 1)))
240		lemul2 11230	. . . . . . . . . . . . . 14 ⊢ (((𝑇↑𝑛) ∈ ℝ ∧ (𝑇↑(𝑛 + 1)) ∈ ℝ ∧ ((𝑀 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑀 · (𝑛 + 1)))) → ((𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
241	152, 119, 115, 239, 240	syl112anc 1442	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
242	237, 241	mpbid 224	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
243	110, 153, 120, 227, 242	letrd 10533	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
244	89, 110, 120, 151, 243	letrd 10533	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
245	244	expr 450	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
246	245	ralrimdva 3151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
247	82, 246	syl5bi 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
248	247	expcom 404	. . . . . 6 ⊢ (𝑛 ∈ ℕ₀ → (𝜑 → (∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
249	248	a2d 29	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))) → (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
250	9, 18, 27, 36, 79, 249	nn0ind 11824	. . . 4 ⊢ (𝑋 ∈ ℕ₀ → (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
251	250	impcom 398	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀) → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))
252		fveq2 6446	. . . . 5 ⊢ (𝑘 = 𝑌 → (𝐹‘𝑘) = (𝐹‘𝑌))
253	252	breq1d 4896	. . . 4 ⊢ (𝑘 = 𝑌 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) ↔ (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
254	253	rspccv 3508	. . 3 ⊢ (∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) → (𝑌 ∈ (0...((𝑀↑𝑋) − 1)) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
255	251, 254	syl 17	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀) → (𝑌 ∈ (0...((𝑀↑𝑋) − 1)) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
256	255	3impia 1106	1 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀ ∧ 𝑌 ∈ (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 ℕ₀cn0 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

W3C validator