Metamath Proof Explorer

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 ) ) ) → ( 𝐹 ‘ 𝑌 ) ≤ ( ( 𝑀 · 𝑋 ) · ( 𝑇 ↑ 𝑋 ) ) )