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 27613

Description: Lemma for ostth2 27616. (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 7376	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑀↑𝑥) = (𝑀↑0))
2	1	oveq1d 7383	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝑀↑𝑥) − 1) = ((𝑀↑0) − 1))
3	2	oveq2d 7384	. . . . . . 7 ⊢ (𝑥 = 0 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑0) − 1)))
4		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0))
5		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑇↑𝑥) = (𝑇↑0))
6	4, 5	oveq12d 7386	. . . . . . . 8 ⊢ (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 0) · (𝑇↑0)))
7	6	breq2d 5112	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
8	3, 7	raleqbidv 3318	. . . . . 6 ⊢ (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
9	8	imbi2d 340	. . . . 5 ⊢ (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))))
10		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑀↑𝑥) = (𝑀↑𝑛))
11	10	oveq1d 7383	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑛) − 1))
12	11	oveq2d 7384	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑛) − 1)))
13		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛))
14		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (𝑇↑𝑥) = (𝑇↑𝑛))
15	13, 14	oveq12d 7386	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑛) · (𝑇↑𝑛)))
16	15	breq2d 5112	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
17	12, 16	raleqbidv 3318	. . . . . 6 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
18	17	imbi2d 340	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))))
19		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑀↑𝑥) = (𝑀↑(𝑛 + 1)))
20	19	oveq1d 7383	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → ((𝑀↑𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1))
21	20	oveq2d 7384	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1)))
22		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1)))
23		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (𝑇↑𝑥) = (𝑇↑(𝑛 + 1)))
24	22, 23	oveq12d 7386	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
25	24	breq2d 5112	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
26	21, 25	raleqbidv 3318	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
27	26	imbi2d 340	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
28		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀↑𝑥) = (𝑀↑𝑋))
29	28	oveq1d 7383	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑀↑𝑥) − 1) = ((𝑀↑𝑋) − 1))
30	29	oveq2d 7384	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (0...((𝑀↑𝑥) − 1)) = (0...((𝑀↑𝑋) − 1)))
31		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋))
32		oveq2 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑇↑𝑥) = (𝑇↑𝑋))
33	31, 32	oveq12d 7386	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇↑𝑥)) = ((𝑀 · 𝑋) · (𝑇↑𝑋)))
34	33	breq2d 5112	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ (𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
35	30, 34	raleqbidv 3318	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
36	35	imbi2d 340	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑥) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑥) · (𝑇↑𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))))
37		ostth2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘2))
38		eluz2nn 12813	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘2) → 𝑀 ∈ ℕ)
39	37, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
40	39	nncnd 12173	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℂ)
41	40	exp0d 14075	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑0) = 1)
42	41	oveq1d 7383	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀↑0) − 1) = (1 − 1))
43		1m1e0 12229	. . . . . . . . . 10 ⊢ (1 − 1) = 0
44	42, 43	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀↑0) − 1) = 0)
45	44	oveq2d 7384	. . . . . . . 8 ⊢ (𝜑 → (0...((𝑀↑0) − 1)) = (0...0))
46	45	eleq2d 2823	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈ (0...0)))
47		0le0 12258	. . . . . . . . . 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 27600	. . . . . . . . . . 11 ⊢ 0 = (0_g‘𝑄)
53	50, 52	abv0 20768	. . . . . . . . . 10 ⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0)
54	49, 53	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘0) = 0)
55	40	mul01d 11344	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · 0) = 0)
56	55	oveq1d 7383	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0)))
57		ostth2.7	. . . . . . . . . . . . . 14 ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))
58		1re 11144	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
59		nnq 12887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
60	39, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℚ)
61	51	qrngbas 27598	. . . . . . . . . . . . . . . . 17 ⊢ ℚ = (Base‘𝑄)
62	50, 61	abvcl 20761	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℝ)
63	49, 60, 62	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ)
64		ifcl 4527	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (𝐹‘𝑀) ∈ ℝ) → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ)
65	58, 63, 64	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ)
66	57, 65	eqeltrid 2841	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ ℝ)
67	66	recnd 11172	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
68		0nn0 12428	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ₀
69		expcl 14014	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 0 ∈ ℕ₀) → (𝑇↑0) ∈ ℂ)
70	67, 68, 69	sylancl 587	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇↑0) ∈ ℂ)
71	70	mul02d 11343	. . . . . . . . . 10 ⊢ (𝜑 → (0 · (𝑇↑0)) = 0)
72	56, 71	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0)
73	48, 54, 72	3brtr4d 5132	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))
74		elfz1eq 13463	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...0) → 𝑘 = 0)
75	74	fveq2d 6846	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...0) → (𝐹‘𝑘) = (𝐹‘0))
76	75	breq1d 5110	. . . . . . . 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 3129	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))
80		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗))
81	80	breq1d 5110	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
82	81	cbvralvw 3216	. . . . . . . 8 ⊢ (∀𝑘 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
83	49	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝐹 ∈ 𝐴)
84		elfzelz 13452	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ)
85	84	ad2antrl 729	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℤ)
86		zq 12879	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℚ)
87	85, 86	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℚ)
88	50, 61	abvcl 20761	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑘 ∈ ℚ) → (𝐹‘𝑘) ∈ ℝ)
89	83, 87, 88	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ∈ ℝ)
90	39	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℕ)
91		simplr 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℕ₀)
92	90, 91	nnexpcld 14180	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℕ)
93	85, 92	zmodcld 13824	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℕ₀)
94	93	nn0zd 12525	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℤ)
95		zq 12879	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod (𝑀↑𝑛)) ∈ ℤ → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ)
96	94, 95	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ ℚ)
97	50, 61	abvcl 20761	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ∈ ℝ)
98	83, 96, 97	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ∈ ℝ)
99	90, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℚ)
100	83, 99, 62	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ∈ ℝ)
101	100, 91	reexpcld 14098	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℝ)
102	85	zred 12608	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℝ)
103	102, 92	nndivred 12211	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) ∈ ℝ)
104	103	flcld 13730	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ)
105		zq 12879	. . . . . . . . . . . . . . 15 ⊢ ((⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℤ → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ)
106	104, 105	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ)
107	50, 61	abvcl 20761	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ)
108	83, 106, 107	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℝ)
109	101, 108	remulcld 11174	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ∈ ℝ)
110	98, 109	readdcld 11173	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ∈ ℝ)
111	90	nnred 12172	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℝ)
112		nn0p1nn 12452	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
113	112	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ)
114	113	nnred 12172	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℝ)
115	111, 114	remulcld 11174	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ)
116	66	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑇 ∈ ℝ)
117		peano2nn0 12453	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ₀)
118	117	ad2antlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ ℕ₀)
119	116, 118	reexpcld 14098	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ)
120	115, 119	remulcld 11174	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ)
121		nnq 12887	. . . . . . . . . . . . . . 15 ⊢ ((𝑀↑𝑛) ∈ ℕ → (𝑀↑𝑛) ∈ ℚ)
122	92, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℚ)
123		qmulcl 12892	. . . . . . . . . . . . . 14 ⊢ (((𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ)
124	122, 106, 123	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ)
125		qex 12886	. . . . . . . . . . . . . . 15 ⊢ ℚ ∈ V
126		cnfldadd 21327	. . . . . . . . . . . . . . . 16 ⊢ + = (+_g‘ℂ_fld)
127	51, 126	ressplusg 17223	. . . . . . . . . . . . . . 15 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
128	125, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ + = (+_g‘𝑄)
129	50, 61, 128	abvtri 20767	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑘 mod (𝑀↑𝑛)) ∈ ℚ ∧ ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))))
130	83, 96, 124, 129	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))))
131	92	nnrpd 12959	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ⁺)
132		modval 13803	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℝ ∧ (𝑀↑𝑛) ∈ ℝ⁺) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
133	102, 131, 132	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) = (𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
134	133	oveq1d 7383	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))))
135	102	recnd 11172	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ ℂ)
136		qcn 12888	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℚ → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
137	124, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
138	135, 137	npcand 11508	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 − ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘)
139	134, 138	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = 𝑘)
140	139	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑘 mod (𝑀↑𝑛)) + ((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = (𝐹‘𝑘))
141		cnfldmul 21329	. . . . . . . . . . . . . . . . . 18 ⊢ · = (._r‘ℂ_fld)
142	51, 141	ressmulr 17239	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
143	125, 142	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ · = (._r‘𝑄)
144	50, 61, 143	abvmul 20766	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑀↑𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℚ) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
145	83, 122, 106, 144	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
146	51, 50	qabvexp 27605	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ₀) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))
147	83, 99, 91, 146	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))
148	147	oveq1d 7383	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑀↑𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
149	145, 148	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛))))) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))))
150	149	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (𝐹‘((𝑀↑𝑛) · (⌊‘(𝑘 / (𝑀↑𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))))
151	130, 140, 150	3brtr3d 5131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))))
152	116, 91	reexpcld 14098	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℝ)
153	115, 152	remulcld 11174	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ∈ ℝ)
154		nn0re 12422	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
155	154	ad2antlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℝ)
156	111, 155	remulcld 11174	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℝ)
157	156, 152	remulcld 11174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) · (𝑇↑𝑛)) ∈ ℝ)
158	111, 152	remulcld 11174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑇↑𝑛)) ∈ ℝ)
159		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → (𝐹‘𝑗) = (𝐹‘(𝑘 mod (𝑀↑𝑛))))
160	159	breq1d 5110	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑘 mod (𝑀↑𝑛)) → ((𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛))))
161		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
162		zmodfz 13825	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ (𝑀↑𝑛) ∈ ℕ) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1)))
163	85, 92, 162	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 mod (𝑀↑𝑛)) ∈ (0...((𝑀↑𝑛) − 1)))
164	160, 161, 163	rspcdva 3579	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(𝑘 mod (𝑀↑𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))
165	111, 101	remulcld 11174	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ∈ ℝ)
166	101	recnd 11172	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ∈ ℂ)
167	108	recnd 11172	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ∈ ℂ)
168	166, 167	mulcomd 11165	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)))
169	50, 61	abvge0 20762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → 0 ≤ (𝐹‘𝑀))
170	83, 99, 169	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝐹‘𝑀))
171	100, 91, 170	expge0d 14099	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ ((𝐹‘𝑀)↑𝑛))
172	104	zred 12608	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℝ)
173		elfzle1 13455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘)
174	173	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑘)
175	92	nnred 12172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑𝑛) ∈ ℝ)
176	92	nngt0d 12206	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀↑𝑛))
177		divge0 12023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ℝ ∧ 0 ≤ 𝑘) ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → 0 ≤ (𝑘 / (𝑀↑𝑛)))
178	102, 174, 175, 176, 177	syl22anc 839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ (𝑘 / (𝑀↑𝑛)))
179		flge0nn0 13752	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀↑𝑛))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀)
180	103, 178, 179	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀)
181	51, 50	qabvle 27604	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ 𝐴 ∧ (⌊‘(𝑘 / (𝑀↑𝑛))) ∈ ℕ₀) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ (⌊‘(𝑘 / (𝑀↑𝑛))))
182	83, 180, 181	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ (⌊‘(𝑘 / (𝑀↑𝑛))))
183		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)))
184		0z 12511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℤ
185	90, 118	nnexpcld 14180	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ)
186	185	nnzd 12526	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ)
187		elfzm11 13523	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 ∈ ℤ ∧ (𝑀↑(𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < (𝑀↑(𝑛 + 1)))))
188	184, 186, 187	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . 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 1145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < (𝑀↑(𝑛 + 1)))
191	90	nncnd 12173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℂ)
192	191, 91	expp1d 14082	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀↑𝑛) · 𝑀))
193	190, 192	breqtrd 5126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑘 < ((𝑀↑𝑛) · 𝑀))
194		ltdivmul 12029	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑀↑𝑛) ∈ ℝ ∧ 0 < (𝑀↑𝑛))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ 𝑘 < ((𝑀↑𝑛) · 𝑀)))
195	102, 111, 175, 176, 194	syl112anc 1377	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ 𝑘 < ((𝑀↑𝑛) · 𝑀)))
196	193, 195	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑘 / (𝑀↑𝑛)) < 𝑀)
197	90	nnzd 12526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℤ)
198		fllt 13738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 / (𝑀↑𝑛)) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀))
199	103, 197, 198	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑘 / (𝑀↑𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀))
200	196, 199	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) < 𝑀)
201	172, 111, 200	ltled 11293	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (⌊‘(𝑘 / (𝑀↑𝑛))) ≤ 𝑀)
202	108, 172, 111, 182, 201	letrd 11302	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) ≤ 𝑀)
203	108, 111, 101, 171, 202	lemul1ad 12093	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))) · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛)))
204	168, 203	eqbrtrd 5122	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · ((𝐹‘𝑀)↑𝑛)))
205	90	nnnn0d 12474	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑀 ∈ ℕ₀)
206	205	nn0ge0d 12477	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 ≤ 𝑀)
207		max1 13112	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
208	100, 58, 207	sylancl 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
209	208, 57	breqtrrdi 5142	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑀) ≤ 𝑇)
210		leexp1a 14110	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) ∧ (0 ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ 𝑇)) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛))
211	100, 116, 91, 170, 209, 210	syl32anc 1381	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘𝑀)↑𝑛) ≤ (𝑇↑𝑛))
212	101, 152, 111, 206, 211	lemul2ad 12094	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · ((𝐹‘𝑀)↑𝑛)) ≤ (𝑀 · (𝑇↑𝑛)))
213	109, 165, 158, 204, 212	letrd 11302	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛))))) ≤ (𝑀 · (𝑇↑𝑛)))
214	98, 109, 157, 158, 164, 213	le2addd 11768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
215		nn0cn 12423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
216	215	ad2antlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℂ)
217		1cnd 11139	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ∈ ℂ)
218	191, 216, 217	adddid 11168	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1)))
219	191	mulridd 11161	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 1) = 𝑀)
220	219	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀))
221	218, 220	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀))
222	221	oveq1d 7383	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)))
223	191, 216	mulcld 11164	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · 𝑛) ∈ ℂ)
224	152	recnd 11172	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ∈ ℂ)
225	223, 191, 224	adddird 11169	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
226	222, 225	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) = (((𝑀 · 𝑛) · (𝑇↑𝑛)) + (𝑀 · (𝑇↑𝑛))))
227	214, 226	breqtrrd 5128	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)))
228		max2 13114	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
229	100, 58, 228	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)))
230	229, 57	breqtrrdi 5142	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 1 ≤ 𝑇)
231		nn0z 12524	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℤ)
232	231	ad2antlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ ℤ)
233		uzid 12778	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ_≥‘𝑛))
234	232, 233	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 𝑛 ∈ (ℤ_≥‘𝑛))
235		peano2uz 12826	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘𝑛) → (𝑛 + 1) ∈ (ℤ_≥‘𝑛))
236	234, 235	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑛 + 1) ∈ (ℤ_≥‘𝑛))
237	116, 230, 236	leexp2ad 14189	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)))
238	90, 113	nnmulcld 12210	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ)
239	238	nngt0d 12206	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → 0 < (𝑀 · (𝑛 + 1)))
240		lemul2 12006	. . . . . . . . . . . . . 14 ⊢ (((𝑇↑𝑛) ∈ ℝ ∧ (𝑇↑(𝑛 + 1)) ∈ ℝ ∧ ((𝑀 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑀 · (𝑛 + 1)))) → ((𝑇↑𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇↑𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
241	152, 119, 115, 239, 240	syl112anc 1377	. . . . . . . . . . . . 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 11302	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → ((𝐹‘(𝑘 mod (𝑀↑𝑛))) + (((𝐹‘𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀↑𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
244	89, 110, 120, 151, 243	letrd 11302	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)))) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
245	244	expr 456	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀↑𝑛) − 1))(𝐹‘𝑗) ≤ ((𝑀 · 𝑛) · (𝑇↑𝑛)) → (𝐹‘𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
246	245	ralrimdva 3138	. . . . . . . 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 12599	. . . 4 ⊢ (𝑋 ∈ ℕ₀ → (𝜑 → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
251	250	impcom 407	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀) → ∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))
252		fveq2 6842	. . . . 5 ⊢ (𝑘 = 𝑌 → (𝐹‘𝑘) = (𝐹‘𝑌))
253	252	breq1d 5110	. . . 4 ⊢ (𝑘 = 𝑌 → ((𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) ↔ (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
254	253	rspccv 3575	. . 3 ⊢ (∀𝑘 ∈ (0...((𝑀↑𝑋) − 1))(𝐹‘𝑘) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)) → (𝑌 ∈ (0...((𝑀↑𝑋) − 1)) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
255	251, 254	syl 17	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀) → (𝑌 ∈ (0...((𝑀↑𝑋) − 1)) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋))))
256	255	3impia 1118	1 ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ₀ ∧ 𝑌 ∈ (0...((𝑀↑𝑋) − 1))) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 Vcvv 3442 ifcif 4481 class class class wbr 5100 ↦ cmpt 5181 ‘cfv 6500 (class class class)co 7368 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11178 ≤ cle 11179 − cmin 11376 -cneg 11377 / cdiv 11806 ℕcn 12157 2c2 12212 ℕ₀cn0 12413 ℤcz 12500 ℤ_≥cuz 12763 ℚcq 12873 ℝ⁺crp 12917 ...cfz 13435 ⌊cfl 13722 mod cmo 13801 ↑cexp 13996 ℙcprime 16610 pCnt cpc 16776 ↾_s cress 17169 +_gcplusg 17189 ._rcmulr 17190 AbsValcabv 20753 ℂ_fldccnfld 21321 logclog 26531

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117 ax-mulf 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-tpos 8178 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-map 8777 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-inf 9358 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-z 12501 df-dec 12620 df-uz 12764 df-q 12874 df-rp 12918 df-ico 13279 df-fz 13436 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-0g 17373 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-grp 18878 df-minusg 18879 df-subg 19065 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100 df-ur 20129 df-ring 20182 df-cring 20183 df-oppr 20285 df-dvdsr 20305 df-unit 20306 df-invr 20336 df-dvr 20349 df-subrng 20491 df-subrg 20515 df-drng 20676 df-abv 20754 df-cnfld 21322

This theorem is referenced by: ostth2lem3 27614

W3C validator