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 27601

Description: Lemma for ostth2 27604. (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 7366	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑀↑𝑥) = (𝑀↑0))
2	1	oveq1d 7373	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝑀↑𝑥) − 1) = ((𝑀↑0) − 1))
3	2	oveq2d 7374	. . . . . . 7 ⊢ (𝑥 = 0 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑0) − 1)))
4		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0))
5		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑇↑𝑥) = (𝑇↑0))
6	4, 5	oveq12d 7376	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 0) · (𝑇↑0)))
7	6	breq2d 5110	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
8	3, 7	raleqbidv 3316	. . . . . 6 ⊢ (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
9	8	imbi2d 340	. . . . 5 ⊢ (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))))
10		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑀↑𝑥) = (𝑀↑𝑛))
11	10	oveq1d 7373	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑛) − 1))
12	11	oveq2d 7374	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑛) − 1)))
13		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛))
14		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑇↑𝑥) = (𝑇↑𝑛))
15	13, 14	oveq12d 7376	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑛) · (𝑇↑𝑛)))
16	15	breq2d 5110	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
17	12, 16	raleqbidv 3316	. . . . . 6 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
18	17	imbi2d 340	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))))
19		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑀↑𝑥) = (𝑀↑(𝑛 + 1)))
20	19	oveq1d 7373	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → ((𝑀↑𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1))
21	20	oveq2d 7374	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1)))
22		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1)))
23		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑇↑𝑥) = (𝑇↑(𝑛 + 1)))
24	22, 23	oveq12d 7376	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
25	24	breq2d 5110	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
26	21, 25	raleqbidv 3316	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
27	26	imbi2d 340	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
28		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀↑𝑥) = (𝑀↑𝑋))
29	28	oveq1d 7373	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑋) − 1))
30	29	oveq2d 7374	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑋) − 1)))
31		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋))
32		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑇↑𝑥) = (𝑇↑𝑋))
33	31, 32	oveq12d 7376	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑋) · (𝑇↑𝑋)))
34	33	breq2d 5110	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
35	30, 34	raleqbidv 3316	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
36	35	imbi2d 340	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))))
37		ostth2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘2))
38		eluz2nn 12801	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℕ)
39	37, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
40	39	nncnd 12161	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℂ)
41	40	exp0d 14063	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑0) = 1)
42	41	oveq1d 7373	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀↑0) − 1) = (1 − 1))
43		1m1e0 12217	. . . . . . . . . 10 ⊢ (1 − 1) = 0
44	42, 43	eqtrdi 2787	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀↑0) − 1) = 0)
45	44	oveq2d 7374	. . . . . . . 8 ⊢ (𝜑 → (0...((𝑀↑0) − 1)) = (0...0))
46	45	eleq2d 2822	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈ (0...0)))
47		0le0 12246	. . . . . . . . . 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 27588	. . . . . . . . . . 11 ⊢ 0 = (0_g‘𝑄)
53	50, 52	abv0 20756	. . . . . . . . . 10 ⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0)
54	49, 53	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) = 0)
55	40	mul01d 11332	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · 0) = 0)
56	55	oveq1d 7373	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0)))
57		ostth2.7	. . . . . . . . . . . . . 14 ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))
58		1re 11132	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
59		nnq 12875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
60	39, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℚ)
61	51	qrngbas 27586	. . . . . . . . . . . . . . . . 17 ⊢ ℚ = (Base‘𝑄)
62	50, 61	abvcl 20749	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℝ)
63	49, 60, 62	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ)
64		ifcl 4525	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (𝐹‘𝑀) ∈ ℝ) → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ)
65	58, 63, 64	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ)
66	57, 65	eqeltrid 2840	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ ℝ)
67	66	recnd 11160	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
68		0nn0 12416	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ₀
69		expcl 14002	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 0 ∈ ℕ₀) → (𝑇↑0) ∈ ℂ)
70	67, 68, 69	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇↑0) ∈ ℂ)
71	70	mul02d 11331	. . . . . . . . . 10 ⊢ (𝜑 → (0 · (𝑇↑0)) = 0)
72	56, 71	eqtrd 2771	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0)
73	48, 54, 72	3brtr4d 5130	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))
74		elfz1eq 13451	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...0) → 𝑘 = 0)
75	74	fveq2d 6838	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...0) → (𝐹‘𝑘) = (𝐹‘0))
76	75	breq1d 5108	. . . . . . . 8 ⊢ (𝑘 ∈ (0...0) → ((𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)) ↔ (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0))))
77	73, 76	syl5ibrcom 247	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (0...0) → (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
78	46, 77	sylbid 240	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) → (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
79	78	ralrimiv 3127	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))
80		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗))
81	80	breq1d 5108	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
82	81	cbvralvw 3214	. . . . . . . 8 ⊢ (∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
83	49	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝐹 ∈ 𝐴)
84		elfzelz 13440	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ)
85	84	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℤ)
86		zq 12867	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℚ)
87	85, 86	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℚ)
88	50, 61	abvcl 20749	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑘 ∈ ℚ) → (𝐹‘𝑘) ∈ ℝ)
89	83, 87, 88	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ∈ ℝ)
90	39	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℕ)
91		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℕ₀)
92	90, 91	nnexpcld 14168	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℕ)
93	85, 92	zmodcld 13812	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℕ₀)
94	93	nn0zd 12513	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℤ)
95		zq 12867	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod (𝑀↑𝑛)) ∈ ℤ → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ)
96	94, 95	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ)
97	50, 61	abvcl 20749	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ∈ ℝ)
98	83, 96, 97	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ∈ ℝ)
99	90, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℚ)
100	83, 99, 62	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ∈ ℝ)
101	100, 91	reexpcld 14086	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℝ)
102	85	zred 12596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℝ)
103	102, 92	nndivred 12199	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) ∈ ℝ)
104	103	flcld 13718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ)
105		zq 12867	. . . . . . . . . . . . . . 15 ⊢ ((⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ)
106	104, 105	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ)
107	50, 61	abvcl 20749	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ)
108	83, 106, 107	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ)
109	101, 108	remulcld 11162	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ∈ ℝ)
110	98, 109	readdcld 11161	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ∈ ℝ)
111	90	nnred 12160	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℝ)
112		nn0p1nn 12440	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
113	112	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ)
114	113	nnred 12160	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℝ)
115	111, 114	remulcld 11162	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ)
116	66	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑇 ∈ ℝ)
117		peano2nn0 12441	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ₀)
118	117	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ₀)
119	116, 118	reexpcld 14086	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ)
120	115, 119	remulcld 11162	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ)
121		nnq 12875	. . . . . . . . . . . . . . 15 ⊢ ((𝑀↑𝑛) ∈ ℕ → (𝑀↑𝑛) ∈ ℚ)
122	92, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℚ)
123		qmulcl 12880	. . . . . . . . . . . . . 14 ⊢ (((𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ)
124	122, 106, 123	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ)
125		qex 12874	. . . . . . . . . . . . . . 15 ⊢ ℚ ∈ V
126		cnfldadd 21315	. . . . . . . . . . . . . . . 16 ⊢ + = (+_g‘ℂ_fld)
127	51, 126	ressplusg 17211	. . . . . . . . . . . . . . 15 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ + = (+_g‘𝑄)
129	50, 61, 128	abvtri 20755	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ ∧ ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))))
130	83, 96, 124, 129	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))))
131	92	nnrpd 12947	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ⁺)
132		modval 13791	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℝ ∧ (𝑀↑𝑛) ∈ ℝ⁺) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
133	102, 131, 132	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
134	133	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
135	102	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℂ)
136		qcn 12876	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
137	124, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
138	135, 137	npcand 11496	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘)
139	134, 138	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘)
140	139	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = (𝐹‘𝑘))
141		cnfldmul 21317	. . . . . . . . . . . . . . . . . 18 ⊢ · = (._r‘ℂ_fld)
142	51, 141	ressmulr 17227	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ · = (._r‘𝑄)
144	50, 61, 143	abvmul 20754	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
145	83, 122, 106, 144	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
146	51, 50	qabvexp 27593	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ₀) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))
147	83, 99, 91, 146	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))
148	147	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
149	145, 148	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
150	149	oveq2d 7374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))))
151	130, 140, 150	3brtr3d 5129	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))))
152	116, 91	reexpcld 14086	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℝ)
153	115, 152	remulcld 11162	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ∈ ℝ)
154		nn0re 12410	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
155	154	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℝ)
156	111, 155	remulcld 11162	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℝ)
157	156, 152	remulcld 11162	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) · (𝑇↑𝑛)) ∈ ℝ)
158	111, 152	remulcld 11162	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑇↑𝑛)) ∈ ℝ)
159		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → (𝐹‘𝑗) = (𝐹‘(𝑘 mod (𝑀↑𝑛))))
160	159	breq1d 5108	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → ((𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
161		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
162		zmodfz 13813	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ (𝑀↑𝑛) ∈ ℕ) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1)))
163	85, 92, 162	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1)))
164	160, 161, 163	rspcdva 3577	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
165	111, 101	remulcld 11162	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ∈ ℝ)
166	101	recnd 11160	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℂ)
167	108	recnd 11160	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
168	166, 167	mulcomd 11153	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)))
169	50, 61	abvge0 20750	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → 0 ≤ (𝐹‘𝑀))
170	83, 99, 169	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝐹‘𝑀))
171	100, 91, 170	expge0d 14087	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ ((𝐹‘𝑀)↑𝑛))
172	104	zred 12596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℝ)
173		elfzle1 13443	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘)
174	173	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑘)
175	92	nnred 12160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ)
176	92	nngt0d 12194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀↑𝑛))
177		divge0 12011	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ℝ ∧ 0 ≤ 𝑘) ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → 0 ≤ (𝑘 / (𝑀↑𝑛)))
178	102, 174, 175, 176, 177	syl22anc 838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝑘 / (𝑀↑𝑛)))
179		flge0nn0 13740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀↑𝑛))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀)
180	103, 178, 179	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀)
181	51, 50	qabvle 27592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ (⌊‘(𝑘 / (𝑀↑𝑛))))
182	83, 180, 181	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ (⌊‘(𝑘 / (𝑀↑𝑛))))
183		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)))
184		0z 12499	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℤ
185	90, 118	nnexpcld 14168	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ)
186	185	nnzd 12514	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ)
187		elfzm11 13511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 ∈ ℤ ∧ (𝑀↑(𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1)))))
188	184, 186, 187	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1)))))
189	183, 188	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1))))
190	189	simp3d 1144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < (𝑀↑(𝑛 + 1)))
191	90	nncnd 12161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℂ)
192	191, 91	expp1d 14070	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀↑𝑛) · 𝑀))
193	190, 192	breqtrd 5124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < ((𝑀↑𝑛) · 𝑀))
194		ltdivmul 12017	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ 𝑘 < ((𝑀↑𝑛) · 𝑀)))
195	102, 111, 175, 176, 194	syl112anc 1376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ 𝑘 < ((𝑀↑𝑛) · 𝑀)))
196	193, 195	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) < 𝑀)
197	90	nnzd 12514	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℤ)
198		fllt 13726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀))
199	103, 197, 198	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀))
200	196, 199	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀)
201	172, 111, 200	ltled 11281	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ≤ 𝑀)
202	108, 172, 111, 182, 201	letrd 11290	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ 𝑀)
203	108, 111, 101, 171, 202	lemul1ad 12081	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛)))
204	168, 203	eqbrtrd 5120	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛)))
205	90	nnnn0d 12462	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℕ₀)
206	205	nn0ge0d 12465	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑀)
207		max1 13100	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
208	100, 58, 207	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
209	208, 57	breqtrrdi 5140	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ 𝑇)
210		leexp1a 14098	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) ∧ (0 ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ 𝑇)) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛))
211	100, 116, 91, 170, 209, 210	syl32anc 1380	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛))
212	101, 152, 111, 206, 211	lemul2ad 12082	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · (𝑇↑𝑛)))
213	109, 165, 158, 204, 212	letrd 11290	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · (𝑇↑𝑛)))
214	98, 109, 157, 158, 164, 213	le2addd 11756	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
215		nn0cn 12411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
216	215	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℂ)
217		1cnd 11127	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ∈ ℂ)
218	191, 216, 217	adddid 11156	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1)))
219	191	mulridd 11149	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 1) = 𝑀)
220	219	oveq2d 7374	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀))
221	218, 220	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀))
222	221	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)))
223	191, 216	mulcld 11152	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℂ)
224	152	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℂ)
225	223, 191, 224	adddird 11157	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
226	222, 225	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
227	214, 226	breqtrrd 5126	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)))
228		max2 13102	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
229	100, 58, 228	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
230	229, 57	breqtrrdi 5140	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ 𝑇)
231		nn0z 12512	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℤ)
232	231	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℤ)
233		uzid 12766	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ_≥‘𝑛))
234	232, 233	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ (ℤ_≥‘𝑛))
235		peano2uz 12814	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘𝑛) → (𝑛 + 1) ∈ (ℤ_≥‘𝑛))
236	234, 235	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ (ℤ_≥‘𝑛))
237	116, 230, 236	leexp2ad 14177	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)))
238	90, 113	nnmulcld 12198	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ)
239	238	nngt0d 12194	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀 · (𝑛 + 1)))
240		lemul2 11994	. . . . . . . . . . . . . 14 ⊢ (((𝑇↑𝑛) ∈ ℝ ∧ (𝑇↑(𝑛 + 1)) ∈ ℝ ∧ ((𝑀 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑀 · (𝑛 + 1)))) → ((𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
241	152, 119, 115, 239, 240	syl112anc 1376	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
242	237, 241	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
243	110, 153, 120, 227, 242	letrd 11290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
244	89, 110, 120, 151, 243	letrd 11290	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
245	244	expr 456	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
246	245	ralrimdva 3136	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
247	82, 246	biimtrid 242	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
248	247	expcom 413	. . . . . 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 12587	. . . 4 ⊢ (𝑋 ∈ ℕ₀ → (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
251	250	impcom 407	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀) → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))
252		fveq2 6834	. . . . 5 ⊢ (𝑘 = 𝑌 → (𝐹‘𝑘) = (𝐹‘𝑌))
253	252	breq1d 5108	. . . 4 ⊢ (𝑘 = 𝑌 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) ↔ (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
254	253	rspccv 3573	. . 3 ⊢ (∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) → (𝑌 ∈ (0...((𝑀↑𝑋) − 1)) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
255	251, 254	syl 17	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀) → (𝑌 ∈ (0...((𝑀↑𝑋) − 1)) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
256	255	3impia 1117	1 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀ ∧ 𝑌 ∈ (0...((𝑀↑𝑋) − 1))) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∀wral 3051 Vcvv 3440 ifcif 4479 class class class wbr 5098 ↦ cmpt 5179 ‘cfv 6492 (class class class)co 7358 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 < clt 11166 ≤ cle 11167 − cmin 11364 -cneg 11365 / cdiv 11794 ℕcn 12145 2c2 12200 ℕ₀cn0 12401 ℤcz 12488 ℤ_≥cuz 12751 ℚcq 12861 ℝ⁺crp 12905 ...cfz 13423 ⌊cfl 13710 mod cmo 13789 ↑cexp 13984 ℙcprime 16598 pCnt cpc 16764 ↾_s cress 17157 +_gcplusg 17177 ._rcmulr 17178 AbsValcabv 20741 ℂ_fldccnfld 21309 logclog 26519

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104 ax-addf 11105 ax-mulf 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-tpos 8168 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-er 8635 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-inf 9346 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-q 12862 df-rp 12906 df-ico 13267 df-fz 13424 df-fl 13712 df-mod 13790 df-seq 13925 df-exp 13985 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-starv 17192 df-tset 17196 df-ple 17197 df-ds 17199 df-unif 17200 df-0g 17361 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-grp 18866 df-minusg 18867 df-subg 19053 df-cmn 19711 df-abl 19712 df-mgp 20076 df-rng 20088 df-ur 20117 df-ring 20170 df-cring 20171 df-oppr 20273 df-dvdsr 20293 df-unit 20294 df-invr 20324 df-dvr 20337 df-subrng 20479 df-subrg 20503 df-drng 20664 df-abv 20742 df-cnfld 21310

This theorem is referenced by: ostth2lem3 27602

W3C validator