Theorem ostth2lem2

Description: Lemma for ostth2 . (Contributed by Mario Carneiro, 10-Sep-2014)

	Ref	Expression
Hypotheses	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	ostth2lem2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) ) → ( 𝐹 ‘ 𝑌 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3		padic.j	⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
4		ostth.k	⊢ 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) )
5		ostth.1	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
6		ostth2.2	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
7		ostth2.3	⊢ ( 𝜑 → 1 < ( 𝐹 ‘ 𝑁 ) )
8		ostth2.4	⊢ 𝑅 = ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) )
9		ostth2.5	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
10		ostth2.6	⊢ 𝑆 = ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) )
11		ostth2.7	⊢ 𝑇 = if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) )
12		oveq2	⊢ ( 𝑥 = 0 → ( 𝑀 ↑ 𝑥 ) = ( 𝑀 ↑ 0 ) )
13	12	oveq1d	⊢ ( 𝑥 = 0 → ( ( 𝑀 ↑ 𝑥 ) − 1 ) = ( ( 𝑀 ↑ 0 ) − 1 ) )
14	13	oveq2d	⊢ ( 𝑥 = 0 → ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) = ( 0 ... ( ( 𝑀 ↑ 0 ) − 1 ) ) )
15		oveq2	⊢ ( 𝑥 = 0 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 0 ) )
16		oveq2	⊢ ( 𝑥 = 0 → ( 𝑇 ↑ 𝑥 ) = ( 𝑇 ↑ 0 ) )
17	15 16	oveq12d	⊢ ( 𝑥 = 0 → ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) = ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) )
18	17	breq2d	⊢ ( 𝑥 = 0 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) ) )
19	14 18	raleqbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 0 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) ) )
20	19	imbi2d	⊢ ( 𝑥 = 0 → ( ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 0 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) ) ) )
21		oveq2	⊢ ( 𝑥 = 𝑛 → ( 𝑀 ↑ 𝑥 ) = ( 𝑀 ↑ 𝑛 ) )
22	21	oveq1d	⊢ ( 𝑥 = 𝑛 → ( ( 𝑀 ↑ 𝑥 ) − 1 ) = ( ( 𝑀 ↑ 𝑛 ) − 1 ) )
23	22	oveq2d	⊢ ( 𝑥 = 𝑛 → ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) = ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) )
24		oveq2	⊢ ( 𝑥 = 𝑛 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 𝑛 ) )
25		oveq2	⊢ ( 𝑥 = 𝑛 → ( 𝑇 ↑ 𝑥 ) = ( 𝑇 ↑ 𝑛 ) )
26	24 25	oveq12d	⊢ ( 𝑥 = 𝑛 → ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) = ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) )
27	26	breq2d	⊢ ( 𝑥 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) )
28	23 27	raleqbidv	⊢ ( 𝑥 = 𝑛 → ( ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) )
29	28	imbi2d	⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) )
30		oveq2	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑀 ↑ 𝑥 ) = ( 𝑀 ↑ ( 𝑛 + 1 ) ) )
31	30	oveq1d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑀 ↑ 𝑥 ) − 1 ) = ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) )
32	31	oveq2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) = ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) )
33		oveq2	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑀 · 𝑥 ) = ( 𝑀 · ( 𝑛 + 1 ) ) )
34		oveq2	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑇 ↑ 𝑥 ) = ( 𝑇 ↑ ( 𝑛 + 1 ) ) )
35	33 34	oveq12d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) = ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) )
36	35	breq2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) )
37	32 36	raleqbidv	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) )
38	37	imbi2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) ) )
39		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑀 ↑ 𝑥 ) = ( 𝑀 ↑ 𝑋 ) )
40	39	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑀 ↑ 𝑥 ) − 1 ) = ( ( 𝑀 ↑ 𝑋 ) − 1 ) )
41	40	oveq2d	⊢ ( 𝑥 = 𝑋 → ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) = ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) )
42		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 𝑋 ) )
43		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑇 ↑ 𝑥 ) = ( 𝑇 ↑ 𝑋 ) )
44	42 43	oveq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) = ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) )
45	44	breq2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) ) )
46	41 45	raleqbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) ) )
47	46	imbi2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑥 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑥 ) · ( 𝑇 ↑ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) ) ) )
48		eluz2nn	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ )
49	9 48	syl	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
50	49	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
51	50	exp0d	⊢ ( 𝜑 → ( 𝑀 ↑ 0 ) = 1 )
52	51	oveq1d	⊢ ( 𝜑 → ( ( 𝑀 ↑ 0 ) − 1 ) = ( 1 − 1 ) )
53		1m1e0	⊢ ( 1 − 1 ) = 0
54	52 53	eqtrdi	⊢ ( 𝜑 → ( ( 𝑀 ↑ 0 ) − 1 ) = 0 )
55	54	oveq2d	⊢ ( 𝜑 → ( 0 ... ( ( 𝑀 ↑ 0 ) − 1 ) ) = ( 0 ... 0 ) )
56	55	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 0 ) − 1 ) ) ↔ 𝑘 ∈ ( 0 ... 0 ) ) )
57		0le0	⊢ 0 ≤ 0
58	57	a1i	⊢ ( 𝜑 → 0 ≤ 0 )
59	1	qrng0	⊢ 0 = ( 0g ‘ 𝑄 )
60	2 59	abv0	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 0 ) = 0 )
61	5 60	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 0 )
62	50	mul01d	⊢ ( 𝜑 → ( 𝑀 · 0 ) = 0 )
63	62	oveq1d	⊢ ( 𝜑 → ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) = ( 0 · ( 𝑇 ↑ 0 ) ) )
64		1re	⊢ 1 ∈ ℝ
65		nnq	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℚ )
66	49 65	syl	⊢ ( 𝜑 → 𝑀 ∈ ℚ )
67	1	qrngbas	⊢ ℚ = ( Base ‘ 𝑄 )
68	2 67	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
69	5 66 68	syl2anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
70		ifcl	⊢ ( ( 1 ∈ ℝ ∧ ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) ∈ ℝ )
71	64 69 70	sylancr	⊢ ( 𝜑 → if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) ∈ ℝ )
72	11 71	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
73	72	recnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
74		0nn0	⊢ 0 ∈ ℕ0
75		expcl	⊢ ( ( 𝑇 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝑇 ↑ 0 ) ∈ ℂ )
76	73 74 75	sylancl	⊢ ( 𝜑 → ( 𝑇 ↑ 0 ) ∈ ℂ )
77	76	mul02d	⊢ ( 𝜑 → ( 0 · ( 𝑇 ↑ 0 ) ) = 0 )
78	63 77	eqtrd	⊢ ( 𝜑 → ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) = 0 )
79	58 61 78	3brtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) )
80		elfz1eq	⊢ ( 𝑘 ∈ ( 0 ... 0 ) → 𝑘 = 0 )
81	80	fveq2d	⊢ ( 𝑘 ∈ ( 0 ... 0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 0 ) )
82	81	breq1d	⊢ ( 𝑘 ∈ ( 0 ... 0 ) → ( ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) ↔ ( 𝐹 ‘ 0 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) ) )
83	79 82	syl5ibrcom	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 0 ) → ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) ) )
84	56 83	sylbid	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 0 ) − 1 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) ) )
85	84	ralrimiv	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 0 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 0 ) · ( 𝑇 ↑ 0 ) ) )
86		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
87	86	breq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ↔ ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) )
88	87	cbvralvw	⊢ ( ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ↔ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) )
89	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝐹 ∈ 𝐴 )
90		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) → 𝑘 ∈ ℤ )
91	90	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑘 ∈ ℤ )
92		zq	⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℚ )
93	91 92	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑘 ∈ ℚ )
94	2 67	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑘 ∈ ℚ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
95	89 93 94	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
96	49	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑀 ∈ ℕ )
97		simplr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑛 ∈ ℕ0 )
98	96 97	nnexpcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 ↑ 𝑛 ) ∈ ℕ )
99	91 98	zmodcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ℕ0 )
100	99	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ℤ )
101		zq	⊢ ( ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ℤ → ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ℚ )
102	100 101	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ℚ )
103	2 67	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ℚ ) → ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℝ )
104	89 102 103	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℝ )
105	96 65	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑀 ∈ ℚ )
106	89 105 68	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
107	106 97	reexpcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ∈ ℝ )
108	91	zred	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑘 ∈ ℝ )
109	108 98	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ∈ ℝ )
110	109	flcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℤ )
111		zq	⊢ ( ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℤ → ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℚ )
112	110 111	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℚ )
113	2 67	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℚ ) → ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℝ )
114	89 112 113	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℝ )
115	107 114	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ∈ ℝ )
116	104 115	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) ∈ ℝ )
117	96	nnred	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑀 ∈ ℝ )
118		nn0p1nn	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ )
119	118	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
120	119	nnred	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℝ )
121	117 120	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · ( 𝑛 + 1 ) ) ∈ ℝ )
122	72	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑇 ∈ ℝ )
123		peano2nn0	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
124	123	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
125	122 124	reexpcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑇 ↑ ( 𝑛 + 1 ) ) ∈ ℝ )
126	121 125	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ∈ ℝ )
127		nnq	⊢ ( ( 𝑀 ↑ 𝑛 ) ∈ ℕ → ( 𝑀 ↑ 𝑛 ) ∈ ℚ )
128	98 127	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 ↑ 𝑛 ) ∈ ℚ )
129		qmulcl	⊢ ( ( ( 𝑀 ↑ 𝑛 ) ∈ ℚ ∧ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℚ ) → ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℚ )
130	128 112 129	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℚ )
131		qex	⊢ ℚ ∈ V
132		cnfldadd	⊢ + = ( +g ‘ ℂfld )
133	1 132	ressplusg	⊢ ( ℚ ∈ V → + = ( +g ‘ 𝑄 ) )
134	131 133	ax-mp	⊢ + = ( +g ‘ 𝑄 )
135	2 67 134	abvtri	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ℚ ∧ ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℚ ) → ( 𝐹 ‘ ( ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) + ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) ≤ ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) )
136	89 102 130 135	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) + ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) ≤ ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) )
137	98	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 ↑ 𝑛 ) ∈ ℝ+ )
138		modval	⊢ ( ( 𝑘 ∈ ℝ ∧ ( 𝑀 ↑ 𝑛 ) ∈ ℝ+ ) → ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) = ( 𝑘 − ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) )
139	108 137 138	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) = ( 𝑘 − ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) )
140	139	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) + ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) = ( ( 𝑘 − ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) + ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) )
141	108	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑘 ∈ ℂ )
142		qcn	⊢ ( ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℚ → ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℂ )
143	130 142	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℂ )
144	141 143	npcand	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑘 − ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) + ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) = 𝑘 )
145	140 144	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) + ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) = 𝑘 )
146	145	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) + ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) = ( 𝐹 ‘ 𝑘 ) )
147		cnfldmul	⊢ · = ( .r ‘ ℂfld )
148	1 147	ressmulr	⊢ ( ℚ ∈ V → · = ( .r ‘ 𝑄 ) )
149	131 148	ax-mp	⊢ · = ( .r ‘ 𝑄 )
150	2 67 149	abvmul	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑀 ↑ 𝑛 ) ∈ ℚ ∧ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℚ ) → ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) = ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) )
151	89 128 112 150	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) = ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) )
152	1 2	qabvexp	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) )
153	89 105 97 152	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) )
154	153	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) = ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) )
155	151 154	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) = ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) )
156	155	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) = ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) )
157	136 146 156	3brtr3d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) )
158	122 97	reexpcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑇 ↑ 𝑛 ) ∈ ℝ )
159	121 158	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ 𝑛 ) ) ∈ ℝ )
160		nn0re	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
161	160	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑛 ∈ ℝ )
162	117 161	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · 𝑛 ) ∈ ℝ )
163	162 158	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ∈ ℝ )
164	117 158	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · ( 𝑇 ↑ 𝑛 ) ) ∈ ℝ )
165		fveq2	⊢ ( 𝑗 = ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) )
166	165	breq1d	⊢ ( 𝑗 = ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ↔ ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) )
167		simprr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) )
168		zmodfz	⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ↑ 𝑛 ) ∈ ℕ ) → ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) )
169	91 98 168	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) )
170	166 167 169	rspcdva	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) )
171	117 107	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) ∈ ℝ )
172	107	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ∈ ℂ )
173	114	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ∈ ℂ )
174	172 173	mulcomd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) = ( ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) · ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) )
175	2 67	abvge0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → 0 ≤ ( 𝐹 ‘ 𝑀 ) )
176	89 105 175	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑀 ) )
177	106 97 176	expge0d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) )
178	110	zred	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℝ )
179		elfzle1	⊢ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) → 0 ≤ 𝑘 )
180	179	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 0 ≤ 𝑘 )
181	98	nnred	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 ↑ 𝑛 ) ∈ ℝ )
182	98	nngt0d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 0 < ( 𝑀 ↑ 𝑛 ) )
183		divge0	⊢ ( ( ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) ∧ ( ( 𝑀 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 𝑀 ↑ 𝑛 ) ) ) → 0 ≤ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) )
184	108 180 181 182 183	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 0 ≤ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) )
185		flge0nn0	⊢ ( ( ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) → ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℕ0 )
186	109 184 185	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℕ0 )
187	1 2	qabvle	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ∈ ℕ0 ) → ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ≤ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) )
188	89 186 187	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ≤ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) )
189		simprl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) )
190		0z	⊢ 0 ∈ ℤ
191	96 124	nnexpcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 ↑ ( 𝑛 + 1 ) ) ∈ ℕ )
192	191	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 ↑ ( 𝑛 + 1 ) ) ∈ ℤ )
193		elfzm11	⊢ ( ( 0 ∈ ℤ ∧ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) ) )
194	190 192 193	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) ) )
195	189 194	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ∧ 𝑘 < ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) )
196	195	simp3d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑘 < ( 𝑀 ↑ ( 𝑛 + 1 ) ) )
197	96	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑀 ∈ ℂ )
198	197 97	expp1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 ↑ ( 𝑛 + 1 ) ) = ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) )
199	196 198	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑘 < ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) )
200		ltdivmul	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( ( 𝑀 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 𝑀 ↑ 𝑛 ) ) ) → ( ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) < 𝑀 ↔ 𝑘 < ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) ) )
201	108 117 181 182 200	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) < 𝑀 ↔ 𝑘 < ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) ) )
202	199 201	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) < 𝑀 )
203	96	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑀 ∈ ℤ )
204		fllt	⊢ ( ( ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ∈ ℝ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) < 𝑀 ↔ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) < 𝑀 ) )
205	109 203 204	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) < 𝑀 ↔ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) < 𝑀 ) )
206	202 205	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) < 𝑀 )
207	178 117 206	ltled	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ≤ 𝑀 )
208	114 178 117 188 207	letrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ≤ 𝑀 )
209	114 117 107 177 208	lemul1ad	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) · ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) ≤ ( 𝑀 · ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) )
210	174 209	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ≤ ( 𝑀 · ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) )
211	96	nnnn0d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑀 ∈ ℕ0 )
212	211	nn0ge0d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 0 ≤ 𝑀 )
213		max1	⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐹 ‘ 𝑀 ) ≤ if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) )
214	106 64 213	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ 𝑀 ) ≤ if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) )
215	214 11	breqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ 𝑀 ) ≤ 𝑇 )
216		leexp1a	⊢ ( ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ0 ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝑀 ) ∧ ( 𝐹 ‘ 𝑀 ) ≤ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ≤ ( 𝑇 ↑ 𝑛 ) )
217	106 122 97 176 215 216	syl32anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ≤ ( 𝑇 ↑ 𝑛 ) )
218	107 158 117 212 217	lemul2ad	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) ≤ ( 𝑀 · ( 𝑇 ↑ 𝑛 ) ) )
219	115 171 164 210 218	letrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ≤ ( 𝑀 · ( 𝑇 ↑ 𝑛 ) ) )
220	104 115 163 164 170 219	le2addd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) ≤ ( ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) + ( 𝑀 · ( 𝑇 ↑ 𝑛 ) ) ) )
221		nn0cn	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
222	221	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑛 ∈ ℂ )
223		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 1 ∈ ℂ )
224	197 222 223	adddid	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · ( 𝑛 + 1 ) ) = ( ( 𝑀 · 𝑛 ) + ( 𝑀 · 1 ) ) )
225	197	mulridd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · 1 ) = 𝑀 )
226	225	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 · 𝑛 ) + ( 𝑀 · 1 ) ) = ( ( 𝑀 · 𝑛 ) + 𝑀 ) )
227	224 226	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · ( 𝑛 + 1 ) ) = ( ( 𝑀 · 𝑛 ) + 𝑀 ) )
228	227	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ 𝑛 ) ) = ( ( ( 𝑀 · 𝑛 ) + 𝑀 ) · ( 𝑇 ↑ 𝑛 ) ) )
229	197 222	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · 𝑛 ) ∈ ℂ )
230	158	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑇 ↑ 𝑛 ) ∈ ℂ )
231	229 197 230	adddird	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( ( 𝑀 · 𝑛 ) + 𝑀 ) · ( 𝑇 ↑ 𝑛 ) ) = ( ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) + ( 𝑀 · ( 𝑇 ↑ 𝑛 ) ) ) )
232	228 231	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ 𝑛 ) ) = ( ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) + ( 𝑀 · ( 𝑇 ↑ 𝑛 ) ) ) )
233	220 232	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ 𝑛 ) ) )
234		max2	⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ 1 ∈ ℝ ) → 1 ≤ if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) )
235	106 64 234	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 1 ≤ if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) )
236	235 11	breqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 1 ≤ 𝑇 )
237		nn0z	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
238	237	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑛 ∈ ℤ )
239		uzid	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
240	238 239	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
241		peano2uz	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
242	240 241	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
243	122 236 242	leexp2ad	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑇 ↑ 𝑛 ) ≤ ( 𝑇 ↑ ( 𝑛 + 1 ) ) )
244	96 119	nnmulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝑀 · ( 𝑛 + 1 ) ) ∈ ℕ )
245	244	nngt0d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → 0 < ( 𝑀 · ( 𝑛 + 1 ) ) )
246		lemul2	⊢ ( ( ( 𝑇 ↑ 𝑛 ) ∈ ℝ ∧ ( 𝑇 ↑ ( 𝑛 + 1 ) ) ∈ ℝ ∧ ( ( 𝑀 · ( 𝑛 + 1 ) ) ∈ ℝ ∧ 0 < ( 𝑀 · ( 𝑛 + 1 ) ) ) ) → ( ( 𝑇 ↑ 𝑛 ) ≤ ( 𝑇 ↑ ( 𝑛 + 1 ) ) ↔ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ 𝑛 ) ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) )
247	158 125 121 245 246	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑇 ↑ 𝑛 ) ≤ ( 𝑇 ↑ ( 𝑛 + 1 ) ) ↔ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ 𝑛 ) ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) )
248	243 247	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ 𝑛 ) ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) )
249	116 159 126 233 248	letrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑘 mod ( 𝑀 ↑ 𝑛 ) ) ) + ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ ( ⌊ ‘ ( 𝑘 / ( 𝑀 ↑ 𝑛 ) ) ) ) ) ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) )
250	95 116 126 157 249	letrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ∧ ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) )
251	250	expr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ) → ( ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) )
252	251	ralrimdva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑗 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) )
253	88 252	biimtrid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) )
254	253	expcom	⊢ ( 𝑛 ∈ ℕ0 → ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) ) )
255	254	a2d	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑛 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑛 ) · ( 𝑇 ↑ 𝑛 ) ) ) → ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ ( 𝑛 + 1 ) ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · ( 𝑛 + 1 ) ) · ( 𝑇 ↑ ( 𝑛 + 1 ) ) ) ) ) )
256	20 29 38 47 85 255	nn0ind	⊢ ( 𝑋 ∈ ℕ0 → ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) ) )
257	256	impcom	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) )
258		fveq2	⊢ ( 𝑘 = 𝑌 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑌 ) )
259	258	breq1d	⊢ ( 𝑘 = 𝑌 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) ↔ ( 𝐹 ‘ 𝑌 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) ) )
260	259	rspccv	⊢ ( ∀ 𝑘 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) → ( 𝑌 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) → ( 𝐹 ‘ 𝑌 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) ) )
261	257 260	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ0 ) → ( 𝑌 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) → ( 𝐹 ‘ 𝑌 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) ) )
262	261	3impia	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ( 0 ... ( ( 𝑀 ↑ 𝑋 ) − 1 ) ) ) → ( 𝐹 ‘ 𝑌 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) )