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 27545

Description: Lemma for ostth2 27548. (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 7395	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑀↑𝑥) = (𝑀↑0))
2	1	oveq1d 7402	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝑀↑𝑥) − 1) = ((𝑀↑0) − 1))
3	2	oveq2d 7403	. . . . . . 7 ⊢ (𝑥 = 0 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑0) − 1)))
4		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0))
5		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑇↑𝑥) = (𝑇↑0))
6	4, 5	oveq12d 7405	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 0) · (𝑇↑0)))
7	6	breq2d 5119	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
8	3, 7	raleqbidv 3319	. . . . . 6 ⊢ (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
9	8	imbi2d 340	. . . . 5 ⊢ (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))))
10		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑀↑𝑥) = (𝑀↑𝑛))
11	10	oveq1d 7402	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑛) − 1))
12	11	oveq2d 7403	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑛) − 1)))
13		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛))
14		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑇↑𝑥) = (𝑇↑𝑛))
15	13, 14	oveq12d 7405	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑛) · (𝑇↑𝑛)))
16	15	breq2d 5119	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
17	12, 16	raleqbidv 3319	. . . . . 6 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
18	17	imbi2d 340	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))))
19		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑀↑𝑥) = (𝑀↑(𝑛 + 1)))
20	19	oveq1d 7402	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → ((𝑀↑𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1))
21	20	oveq2d 7403	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1)))
22		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1)))
23		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑇↑𝑥) = (𝑇↑(𝑛 + 1)))
24	22, 23	oveq12d 7405	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
25	24	breq2d 5119	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
26	21, 25	raleqbidv 3319	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
27	26	imbi2d 340	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
28		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀↑𝑥) = (𝑀↑𝑋))
29	28	oveq1d 7402	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑋) − 1))
30	29	oveq2d 7403	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑋) − 1)))
31		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋))
32		oveq2 7395	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑇↑𝑥) = (𝑇↑𝑋))
33	31, 32	oveq12d 7405	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑋) · (𝑇↑𝑋)))
34	33	breq2d 5119	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
35	30, 34	raleqbidv 3319	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
36	35	imbi2d 340	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))))
37		ostth2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘2))
38		eluz2nn 12847	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℕ)
39	37, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
40	39	nncnd 12202	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℂ)
41	40	exp0d 14105	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑0) = 1)
42	41	oveq1d 7402	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀↑0) − 1) = (1 − 1))
43		1m1e0 12258	. . . . . . . . . 10 ⊢ (1 − 1) = 0
44	42, 43	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀↑0) − 1) = 0)
45	44	oveq2d 7403	. . . . . . . 8 ⊢ (𝜑 → (0...((𝑀↑0) − 1)) = (0...0))
46	45	eleq2d 2814	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈ (0...0)))
47		0le0 12287	. . . . . . . . . 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 27532	. . . . . . . . . . 11 ⊢ 0 = (0_g‘𝑄)
53	50, 52	abv0 20732	. . . . . . . . . 10 ⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0)
54	49, 53	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) = 0)
55	40	mul01d 11373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · 0) = 0)
56	55	oveq1d 7402	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0)))
57		ostth2.7	. . . . . . . . . . . . . 14 ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))
58		1re 11174	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
59		nnq 12921	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
60	39, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℚ)
61	51	qrngbas 27530	. . . . . . . . . . . . . . . . 17 ⊢ ℚ = (Base‘𝑄)
62	50, 61	abvcl 20725	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℝ)
63	49, 60, 62	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ)
64		ifcl 4534	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (𝐹‘𝑀) ∈ ℝ) → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ)
65	58, 63, 64	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ)
66	57, 65	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ ℝ)
67	66	recnd 11202	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
68		0nn0 12457	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ₀
69		expcl 14044	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 0 ∈ ℕ₀) → (𝑇↑0) ∈ ℂ)
70	67, 68, 69	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇↑0) ∈ ℂ)
71	70	mul02d 11372	. . . . . . . . . 10 ⊢ (𝜑 → (0 · (𝑇↑0)) = 0)
72	56, 71	eqtrd 2764	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0)
73	48, 54, 72	3brtr4d 5139	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))
74		elfz1eq 13496	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...0) → 𝑘 = 0)
75	74	fveq2d 6862	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...0) → (𝐹‘𝑘) = (𝐹‘0))
76	75	breq1d 5117	. . . . . . . 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 3124	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))
80		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗))
81	80	breq1d 5117	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
82	81	cbvralvw 3215	. . . . . . . 8 ⊢ (∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
83	49	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝐹 ∈ 𝐴)
84		elfzelz 13485	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ)
85	84	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℤ)
86		zq 12913	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℚ)
87	85, 86	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℚ)
88	50, 61	abvcl 20725	. . . . . . . . . . . 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 14210	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℕ)
93	85, 92	zmodcld 13854	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℕ₀)
94	93	nn0zd 12555	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℤ)
95		zq 12913	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod (𝑀↑𝑛)) ∈ ℤ → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ)
96	94, 95	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ)
97	50, 61	abvcl 20725	. . . . . . . . . . . . 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 14128	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℝ)
102	85	zred 12638	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℝ)
103	102, 92	nndivred 12240	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) ∈ ℝ)
104	103	flcld 13760	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ)
105		zq 12913	. . . . . . . . . . . . . . 15 ⊢ ((⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ)
106	104, 105	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ)
107	50, 61	abvcl 20725	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ)
108	83, 106, 107	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ)
109	101, 108	remulcld 11204	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ∈ ℝ)
110	98, 109	readdcld 11203	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ∈ ℝ)
111	90	nnred 12201	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℝ)
112		nn0p1nn 12481	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
113	112	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ)
114	113	nnred 12201	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℝ)
115	111, 114	remulcld 11204	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ)
116	66	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑇 ∈ ℝ)
117		peano2nn0 12482	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ₀)
118	117	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ₀)
119	116, 118	reexpcld 14128	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ)
120	115, 119	remulcld 11204	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ)
121		nnq 12921	. . . . . . . . . . . . . . 15 ⊢ ((𝑀↑𝑛) ∈ ℕ → (𝑀↑𝑛) ∈ ℚ)
122	92, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℚ)
123		qmulcl 12926	. . . . . . . . . . . . . 14 ⊢ (((𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ)
124	122, 106, 123	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ)
125		qex 12920	. . . . . . . . . . . . . . 15 ⊢ ℚ ∈ V
126		cnfldadd 21270	. . . . . . . . . . . . . . . 16 ⊢ + = (+_g‘ℂ_fld)
127	51, 126	ressplusg 17254	. . . . . . . . . . . . . . 15 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ + = (+_g‘𝑄)
129	50, 61, 128	abvtri 20731	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ ∧ ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))))
130	83, 96, 124, 129	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))))
131	92	nnrpd 12993	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ⁺)
132		modval 13833	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℝ ∧ (𝑀↑𝑛) ∈ ℝ⁺) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
133	102, 131, 132	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
134	133	oveq1d 7402	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
135	102	recnd 11202	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℂ)
136		qcn 12922	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
137	124, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
138	135, 137	npcand 11537	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘)
139	134, 138	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘)
140	139	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = (𝐹‘𝑘))
141		cnfldmul 21272	. . . . . . . . . . . . . . . . . 18 ⊢ · = (._r‘ℂ_fld)
142	51, 141	ressmulr 17270	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ · = (._r‘𝑄)
144	50, 61, 143	abvmul 20730	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
145	83, 122, 106, 144	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
146	51, 50	qabvexp 27537	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ₀) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))
147	83, 99, 91, 146	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))
148	147	oveq1d 7402	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
149	145, 148	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
150	149	oveq2d 7403	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))))
151	130, 140, 150	3brtr3d 5138	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))))
152	116, 91	reexpcld 14128	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℝ)
153	115, 152	remulcld 11204	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ∈ ℝ)
154		nn0re 12451	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
155	154	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℝ)
156	111, 155	remulcld 11204	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℝ)
157	156, 152	remulcld 11204	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) · (𝑇↑𝑛)) ∈ ℝ)
158	111, 152	remulcld 11204	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑇↑𝑛)) ∈ ℝ)
159		fveq2 6858	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → (𝐹‘𝑗) = (𝐹‘(𝑘 mod (𝑀↑𝑛))))
160	159	breq1d 5117	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → ((𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
161		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
162		zmodfz 13855	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ (𝑀↑𝑛) ∈ ℕ) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1)))
163	85, 92, 162	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1)))
164	160, 161, 163	rspcdva 3589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
165	111, 101	remulcld 11204	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ∈ ℝ)
166	101	recnd 11202	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℂ)
167	108	recnd 11202	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
168	166, 167	mulcomd 11195	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)))
169	50, 61	abvge0 20726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → 0 ≤ (𝐹‘𝑀))
170	83, 99, 169	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝐹‘𝑀))
171	100, 91, 170	expge0d 14129	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ ((𝐹‘𝑀)↑𝑛))
172	104	zred 12638	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℝ)
173		elfzle1 13488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘)
174	173	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑘)
175	92	nnred 12201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ)
176	92	nngt0d 12235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀↑𝑛))
177		divge0 12052	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ℝ ∧ 0 ≤ 𝑘) ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → 0 ≤ (𝑘 / (𝑀↑𝑛)))
178	102, 174, 175, 176, 177	syl22anc 838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝑘 / (𝑀↑𝑛)))
179		flge0nn0 13782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀↑𝑛))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀)
180	103, 178, 179	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀)
181	51, 50	qabvle 27536	. . . . . . . . . . . . . . . . . . 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 12540	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℤ
185	90, 118	nnexpcld 14210	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ)
186	185	nnzd 12556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ)
187		elfzm11 13556	. . . . . . . . . . . . . . . . . . . . . . . . 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 12202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℂ)
192	191, 91	expp1d 14112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀↑𝑛) · 𝑀))
193	190, 192	breqtrd 5133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < ((𝑀↑𝑛) · 𝑀))
194		ltdivmul 12058	. . . . . . . . . . . . . . . . . . . . . 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 12556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℤ)
198		fllt 13768	. . . . . . . . . . . . . . . . . . . . 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 11322	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ≤ 𝑀)
202	108, 172, 111, 182, 201	letrd 11331	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ 𝑀)
203	108, 111, 101, 171, 202	lemul1ad 12122	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛)))
204	168, 203	eqbrtrd 5129	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛)))
205	90	nnnn0d 12503	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℕ₀)
206	205	nn0ge0d 12506	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑀)
207		max1 13145	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
208	100, 58, 207	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
209	208, 57	breqtrrdi 5149	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ 𝑇)
210		leexp1a 14140	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) ∧ (0 ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ 𝑇)) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛))
211	100, 116, 91, 170, 209, 210	syl32anc 1380	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛))
212	101, 152, 111, 206, 211	lemul2ad 12123	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · (𝑇↑𝑛)))
213	109, 165, 158, 204, 212	letrd 11331	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · (𝑇↑𝑛)))
214	98, 109, 157, 158, 164, 213	le2addd 11797	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
215		nn0cn 12452	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
216	215	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℂ)
217		1cnd 11169	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ∈ ℂ)
218	191, 216, 217	adddid 11198	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1)))
219	191	mulridd 11191	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 1) = 𝑀)
220	219	oveq2d 7403	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀))
221	218, 220	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀))
222	221	oveq1d 7402	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)))
223	191, 216	mulcld 11194	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℂ)
224	152	recnd 11202	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℂ)
225	223, 191, 224	adddird 11199	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
226	222, 225	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
227	214, 226	breqtrrd 5135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)))
228		max2 13147	. . . . . . . . . . . . . . . 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 5149	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ 𝑇)
231		nn0z 12554	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℤ)
232	231	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℤ)
233		uzid 12808	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ_≥‘𝑛))
234	232, 233	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ (ℤ_≥‘𝑛))
235		peano2uz 12860	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘𝑛) → (𝑛 + 1) ∈ (ℤ_≥‘𝑛))
236	234, 235	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ (ℤ_≥‘𝑛))
237	116, 230, 236	leexp2ad 14219	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)))
238	90, 113	nnmulcld 12239	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ)
239	238	nngt0d 12235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀 · (𝑛 + 1)))
240		lemul2 12035	. . . . . . . . . . . . . 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 11331	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
244	89, 110, 120, 151, 243	letrd 11331	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
245	244	expr 456	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
246	245	ralrimdva 3133	. . . . . . . 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 12629	. . . 4 ⊢ (𝑋 ∈ ℕ₀ → (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
251	250	impcom 407	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀) → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))
252		fveq2 6858	. . . . 5 ⊢ (𝑘 = 𝑌 → (𝐹‘𝑘) = (𝐹‘𝑌))
253	252	breq1d 5117	. . . 4 ⊢ (𝑘 = 𝑌 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) ↔ (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
254	253	rspccv 3585	. . 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 1540 ∈ wcel 2109 ∀wral 3044 Vcvv 3447 ifcif 4488 class class class wbr 5107 ↦ cmpt 5188 ‘cfv 6511 (class class class)co 7387 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 < clt 11208 ≤ cle 11209 − cmin 11405 -cneg 11406 / cdiv 11835 ℕcn 12186 2c2 12241 ℕ₀cn0 12442 ℤcz 12529 ℤ_≥cuz 12793 ℚcq 12907 ℝ⁺crp 12951 ...cfz 13468 ⌊cfl 13752 mod cmo 13831 ↑cexp 14026 ℙcprime 16641 pCnt cpc 16807 ↾_s cress 17200 +_gcplusg 17220 ._rcmulr 17221 AbsValcabv 20717 ℂ_fldccnfld 21264 logclog 26463

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147 ax-mulf 11148

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-tpos 8205 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-er 8671 df-map 8801 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-sup 9393 df-inf 9394 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-ico 13312 df-fz 13469 df-fl 13754 df-mod 13832 df-seq 13967 df-exp 14027 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-0g 17404 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-grp 18868 df-minusg 18869 df-subg 19055 df-cmn 19712 df-abl 19713 df-mgp 20050 df-rng 20062 df-ur 20091 df-ring 20144 df-cring 20145 df-oppr 20246 df-dvdsr 20266 df-unit 20267 df-invr 20297 df-dvr 20310 df-subrng 20455 df-subrg 20479 df-drng 20640 df-abv 20718 df-cnfld 21265

This theorem is referenced by: ostth2lem3 27546

W3C validator