Metamath Proof Explorer

Theorem ostth2lem3

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 , ( 𝐹 ‘ 𝑀 ) )
ostth2.8 ⊢ 𝑈 = ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) )
Assertion ostth2lem3 ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑁 ) / ( 𝑇 ↑𝑐 𝑈 ) ) ↑ 𝑋 ) ≤ ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 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 ostth2.8 ⊢ 𝑈 = ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) )
13 eluz2b2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
14 6 13 sylib ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
15 14 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
16 nnq ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℚ )
17 15 16 syl ⊢ ( 𝜑 → 𝑁 ∈ ℚ )
18 1 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
19 2 18 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
20 5 17 19 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
22 21 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
23 1re ⊢ 1 ∈ ℝ
24 eluz2b2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑀 ∈ ℕ ∧ 1 < 𝑀 ) )
25 9 24 sylib ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 1 < 𝑀 ) )
26 25 simpld ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
27 nnq ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℚ )
28 26 27 syl ⊢ ( 𝜑 → 𝑀 ∈ ℚ )
29 2 18 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
30 5 28 29 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
31 ifcl ⊢ ( ( 1 ∈ ℝ ∧ ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) ∈ ℝ )
32 23 30 31 sylancr ⊢ ( 𝜑 → if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) ∈ ℝ )
33 11 32 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑇 ∈ ℝ )
35 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
36 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
37 0lt1 ⊢ 0 < 1
38 37 a1i ⊢ ( 𝜑 → 0 < 1 )
39 max2 ⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ 1 ∈ ℝ ) → 1 ≤ if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) )
40 30 36 39 syl2anc ⊢ ( 𝜑 → 1 ≤ if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) )
41 40 11 breqtrrdi ⊢ ( 𝜑 → 1 ≤ 𝑇 )
42 35 36 33 38 41 ltletrd ⊢ ( 𝜑 → 0 < 𝑇 )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 < 𝑇 )
44 34 43 elrpd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑇 ∈ ℝ+ )
45 44 rpge0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 ≤ 𝑇 )
46 15 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
47 14 simprd ⊢ ( 𝜑 → 1 < 𝑁 )
48 46 47 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ+ )
49 26 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
50 25 simprd ⊢ ( 𝜑 → 1 < 𝑀 )
51 49 50 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑀 ) ∈ ℝ+ )
52 48 51 rpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) ) ∈ ℝ+ )
53 12 52 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
54 53 rpred ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑈 ∈ ℝ )
56 34 45 55 recxpcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑𝑐 𝑈 ) ∈ ℝ )
57 56 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑𝑐 𝑈 ) ∈ ℂ )
58 44 55 rpcxpcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑𝑐 𝑈 ) ∈ ℝ+ )
59 58 rpne0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑𝑐 𝑈 ) ≠ 0 )
60 nnnn0 ⊢ ( 𝑋 ∈ ℕ → 𝑋 ∈ ℕ0 )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑋 ∈ ℕ0 )
62 22 57 59 61 expdivd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑁 ) / ( 𝑇 ↑𝑐 𝑈 ) ) ↑ 𝑋 ) = ( ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) / ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) ) )
63 reexpcl ⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ ℝ ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) ∈ ℝ )
64 20 60 63 syl2an ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) ∈ ℝ )
65 26 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑀 ∈ ℕ )
66 65 nnred ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑀 ∈ ℝ )
67 nnre ⊢ ( 𝑋 ∈ ℕ → 𝑋 ∈ ℝ )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑋 ∈ ℝ )
69 68 55 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · 𝑈 ) ∈ ℝ )
70 61 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 ≤ 𝑋 )
71 53 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑈 )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 ≤ 𝑈 )
73 68 55 70 72 mulge0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 ≤ ( 𝑋 · 𝑈 ) )
74 flge0nn0 ⊢ ( ( ( 𝑋 · 𝑈 ) ∈ ℝ ∧ 0 ≤ ( 𝑋 · 𝑈 ) ) → ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ∈ ℕ0 )
75 69 73 74 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ∈ ℕ0 )
76 peano2nn0 ⊢ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℕ0 )
77 75 76 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℕ0 )
78 77 nn0red ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℝ )
79 66 78 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℝ )
80 34 77 reexpcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℝ )
81 79 80 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ∈ ℝ )
82 peano2re ⊢ ( 𝑈 ∈ ℝ → ( 𝑈 + 1 ) ∈ ℝ )
83 55 82 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑈 + 1 ) ∈ ℝ )
84 68 83 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · ( 𝑈 + 1 ) ) ∈ ℝ )
85 66 84 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ∈ ℝ )
86 56 61 reexpcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) ∈ ℝ )
87 86 34 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ∈ ℝ )
88 85 87 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) ∈ ℝ )
89 1 2 qabvexp ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ ∧ 𝑋 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) )
90 5 17 60 89 syl2an3an ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) )
91 68 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑋 ∈ ℂ )
92 48 rpred ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
93 92 recnd ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℂ )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( log ‘ 𝑁 ) ∈ ℂ )
95 51 rpred ⊢ ( 𝜑 → ( log ‘ 𝑀 ) ∈ ℝ )
96 95 recnd ⊢ ( 𝜑 → ( log ‘ 𝑀 ) ∈ ℂ )
97 96 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( log ‘ 𝑀 ) ∈ ℂ )
98 51 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( log ‘ 𝑀 ) ∈ ℝ+ )
99 98 rpne0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( log ‘ 𝑀 ) ≠ 0 )
100 91 94 97 99 divassd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · ( log ‘ 𝑁 ) ) / ( log ‘ 𝑀 ) ) = ( 𝑋 · ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) ) ) )
101 12 oveq2i ⊢ ( 𝑋 · 𝑈 ) = ( 𝑋 · ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) ) )
102 100 101 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · ( log ‘ 𝑁 ) ) / ( log ‘ 𝑀 ) ) = ( 𝑋 · 𝑈 ) )
103 102 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝑋 · ( log ‘ 𝑁 ) ) / ( log ‘ 𝑀 ) ) · ( log ‘ 𝑀 ) ) = ( ( 𝑋 · 𝑈 ) · ( log ‘ 𝑀 ) ) )
104 91 94 mulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · ( log ‘ 𝑁 ) ) ∈ ℂ )
105 104 97 99 divcan1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝑋 · ( log ‘ 𝑁 ) ) / ( log ‘ 𝑀 ) ) · ( log ‘ 𝑀 ) ) = ( 𝑋 · ( log ‘ 𝑁 ) ) )
106 103 105 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · 𝑈 ) · ( log ‘ 𝑀 ) ) = ( 𝑋 · ( log ‘ 𝑁 ) ) )
107 flltp1 ⊢ ( ( 𝑋 · 𝑈 ) ∈ ℝ → ( 𝑋 · 𝑈 ) < ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) )
108 69 107 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · 𝑈 ) < ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) )
109 69 78 98 108 ltmul1dd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · 𝑈 ) · ( log ‘ 𝑀 ) ) < ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) )
110 106 109 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · ( log ‘ 𝑁 ) ) < ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) )
111 92 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( log ‘ 𝑁 ) ∈ ℝ )
112 68 111 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · ( log ‘ 𝑁 ) ) ∈ ℝ )
113 95 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( log ‘ 𝑀 ) ∈ ℝ )
114 78 113 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ∈ ℝ )
115 eflt ⊢ ( ( ( 𝑋 · ( log ‘ 𝑁 ) ) ∈ ℝ ∧ ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ∈ ℝ ) → ( ( 𝑋 · ( log ‘ 𝑁 ) ) < ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ↔ ( exp ‘ ( 𝑋 · ( log ‘ 𝑁 ) ) ) < ( exp ‘ ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ) ) )
116 112 114 115 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · ( log ‘ 𝑁 ) ) < ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ↔ ( exp ‘ ( 𝑋 · ( log ‘ 𝑁 ) ) ) < ( exp ‘ ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ) ) )
117 110 116 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( exp ‘ ( 𝑋 · ( log ‘ 𝑁 ) ) ) < ( exp ‘ ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ) )
118 15 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
119 nnz ⊢ ( 𝑋 ∈ ℕ → 𝑋 ∈ ℤ )
120 reexplog ⊢ ( ( 𝑁 ∈ ℝ+ ∧ 𝑋 ∈ ℤ ) → ( 𝑁 ↑ 𝑋 ) = ( exp ‘ ( 𝑋 · ( log ‘ 𝑁 ) ) ) )
121 118 119 120 syl2an ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) = ( exp ‘ ( 𝑋 · ( log ‘ 𝑁 ) ) ) )
122 65 nnrpd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑀 ∈ ℝ+ )
123 77 nn0zd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℤ )
124 reexplog ⊢ ( ( 𝑀 ∈ ℝ+ ∧ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℤ ) → ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) = ( exp ‘ ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ) )
125 122 123 124 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) = ( exp ‘ ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) · ( log ‘ 𝑀 ) ) ) )
126 117 121 125 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) < ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) )
127 nnexpcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑋 ) ∈ ℕ )
128 15 60 127 syl2an ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) ∈ ℕ )
129 65 77 nnexpcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℕ )
130 nnltlem1 ⊢ ( ( ( 𝑁 ↑ 𝑋 ) ∈ ℕ ∧ ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℕ ) → ( ( 𝑁 ↑ 𝑋 ) < ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ↔ ( 𝑁 ↑ 𝑋 ) ≤ ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) )
131 128 129 130 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑁 ↑ 𝑋 ) < ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ↔ ( 𝑁 ↑ 𝑋 ) ≤ ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) )
132 126 131 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) ≤ ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) )
133 128 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) ∈ ℕ0 )
134 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
135 133 134 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) ∈ ( ℤ≥ ‘ 0 ) )
136 129 nnzd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℤ )
137 peano2zm ⊢ ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℤ → ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ∈ ℤ )
138 136 137 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ∈ ℤ )
139 elfz5 ⊢ ( ( ( 𝑁 ↑ 𝑋 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ∈ ℤ ) → ( ( 𝑁 ↑ 𝑋 ) ∈ ( 0 ... ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) ↔ ( 𝑁 ↑ 𝑋 ) ≤ ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) )
140 135 138 139 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑁 ↑ 𝑋 ) ∈ ( 0 ... ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) ↔ ( 𝑁 ↑ 𝑋 ) ≤ ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) )
141 132 140 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) ∈ ( 0 ... ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) )
142 1 2 3 4 5 6 7 8 9 10 11 ostth2lem2 ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℕ0 ∧ ( 𝑁 ↑ 𝑋 ) ∈ ( 0 ... ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) ) → ( 𝐹 ‘ ( 𝑁 ↑ 𝑋 ) ) ≤ ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) )
143 142 3expia ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝑋 ) ∈ ( 0 ... ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) → ( 𝐹 ‘ ( 𝑁 ↑ 𝑋 ) ) ≤ ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ) )
144 77 143 syldan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑁 ↑ 𝑋 ) ∈ ( 0 ... ( ( 𝑀 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) − 1 ) ) → ( 𝐹 ‘ ( 𝑁 ↑ 𝑋 ) ) ≤ ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ) )
145 141 144 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑁 ↑ 𝑋 ) ) ≤ ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) )
146 90 145 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) ≤ ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) )
147 85 80 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ∈ ℝ )
148 peano2re ⊢ ( ( 𝑋 · 𝑈 ) ∈ ℝ → ( ( 𝑋 · 𝑈 ) + 1 ) ∈ ℝ )
149 69 148 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · 𝑈 ) + 1 ) ∈ ℝ )
150 75 nn0red ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ∈ ℝ )
151 1red ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 1 ∈ ℝ )
152 flle ⊢ ( ( 𝑋 · 𝑈 ) ∈ ℝ → ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ≤ ( 𝑋 · 𝑈 ) )
153 69 152 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ≤ ( 𝑋 · 𝑈 ) )
154 150 69 151 153 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ≤ ( ( 𝑋 · 𝑈 ) + 1 ) )
155 nnge1 ⊢ ( 𝑋 ∈ ℕ → 1 ≤ 𝑋 )
156 155 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 1 ≤ 𝑋 )
157 151 68 69 156 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · 𝑈 ) + 1 ) ≤ ( ( 𝑋 · 𝑈 ) + 𝑋 ) )
158 55 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑈 ∈ ℂ )
159 151 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 1 ∈ ℂ )
160 91 158 159 adddid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · ( 𝑈 + 1 ) ) = ( ( 𝑋 · 𝑈 ) + ( 𝑋 · 1 ) ) )
161 91 mulid1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · 1 ) = 𝑋 )
162 161 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · 𝑈 ) + ( 𝑋 · 1 ) ) = ( ( 𝑋 · 𝑈 ) + 𝑋 ) )
163 160 162 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · ( 𝑈 + 1 ) ) = ( ( 𝑋 · 𝑈 ) + 𝑋 ) )
164 157 163 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑋 · 𝑈 ) + 1 ) ≤ ( 𝑋 · ( 𝑈 + 1 ) ) )
165 78 149 84 154 164 letrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ≤ ( 𝑋 · ( 𝑈 + 1 ) ) )
166 65 nngt0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 < 𝑀 )
167 lemul2 ⊢ ( ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℝ ∧ ( 𝑋 · ( 𝑈 + 1 ) ) ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ≤ ( 𝑋 · ( 𝑈 + 1 ) ) ↔ ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ≤ ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ) )
168 78 84 66 166 167 syl112anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ≤ ( 𝑋 · ( 𝑈 + 1 ) ) ↔ ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ≤ ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ) )
169 165 168 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ≤ ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) )
170 expgt0 ⊢ ( ( 𝑇 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ∈ ℤ ∧ 0 < 𝑇 ) → 0 < ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) )
171 34 123 43 170 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 < ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) )
172 lemul1 ⊢ ( ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℝ ∧ ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ∈ ℝ ∧ ( ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℝ ∧ 0 < ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ) → ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ≤ ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ↔ ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ≤ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ) )
173 79 85 80 171 172 syl112anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ≤ ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ↔ ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ≤ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ) )
174 169 173 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ≤ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) )
175 34 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑇 ∈ ℂ )
176 175 75 expp1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) = ( ( 𝑇 ↑ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) · 𝑇 ) )
177 41 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 1 ≤ 𝑇 )
178 remulcl ⊢ ( ( 𝑈 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝑈 · 𝑋 ) ∈ ℝ )
179 54 67 178 syl2an ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑈 · 𝑋 ) ∈ ℝ )
180 91 158 mulcomd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · 𝑈 ) = ( 𝑈 · 𝑋 ) )
181 153 180 breqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ≤ ( 𝑈 · 𝑋 ) )
182 34 177 150 179 181 cxplead ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑𝑐 ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) ≤ ( 𝑇 ↑𝑐 ( 𝑈 · 𝑋 ) ) )
183 cxpexp ⊢ ( ( 𝑇 ∈ ℂ ∧ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ∈ ℕ0 ) → ( 𝑇 ↑𝑐 ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) = ( 𝑇 ↑ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) )
184 175 75 183 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑𝑐 ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) = ( 𝑇 ↑ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) )
185 44 55 91 cxpmuld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑𝑐 ( 𝑈 · 𝑋 ) ) = ( ( 𝑇 ↑𝑐 𝑈 ) ↑𝑐 𝑋 ) )
186 cxpexp ⊢ ( ( ( 𝑇 ↑𝑐 𝑈 ) ∈ ℂ ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑇 ↑𝑐 𝑈 ) ↑𝑐 𝑋 ) = ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) )
187 57 61 186 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑇 ↑𝑐 𝑈 ) ↑𝑐 𝑋 ) = ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) )
188 185 187 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑𝑐 ( 𝑈 · 𝑋 ) ) = ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) )
189 182 184 188 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) ≤ ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) )
190 34 75 reexpcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) ∈ ℝ )
191 190 86 44 lemul1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑇 ↑ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) ≤ ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) ↔ ( ( 𝑇 ↑ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) · 𝑇 ) ≤ ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) )
192 189 191 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑇 ↑ ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) ) · 𝑇 ) ≤ ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) )
193 176 192 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ≤ ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) )
194 nngt0 ⊢ ( 𝑋 ∈ ℕ → 0 < 𝑋 )
195 194 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 < 𝑋 )
196 0red ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 ∈ ℝ )
197 53 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑈 ∈ ℝ+ )
198 197 rpgt0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 < 𝑈 )
199 55 ltp1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑈 < ( 𝑈 + 1 ) )
200 196 55 83 198 199 lttrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 < ( 𝑈 + 1 ) )
201 68 83 195 200 mulgt0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 < ( 𝑋 · ( 𝑈 + 1 ) ) )
202 66 84 166 201 mulgt0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 0 < ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) )
203 lemul2 ⊢ ( ( ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ∈ ℝ ∧ ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ∈ ℝ ∧ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ∈ ℝ ∧ 0 < ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ) ) → ( ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ≤ ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ↔ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ≤ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) ) )
204 80 87 85 202 203 syl112anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ≤ ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ↔ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ≤ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) ) )
205 193 204 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ≤ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) )
206 81 147 88 174 205 letrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) · ( 𝑇 ↑ ( ( ⌊ ‘ ( 𝑋 · 𝑈 ) ) + 1 ) ) ) ≤ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) )
207 64 81 88 146 206 letrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) ≤ ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) )
208 85 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) ∈ ℂ )
209 86 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) ∈ ℂ )
210 208 209 175 mul12d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) = ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · 𝑇 ) ) )
211 66 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑀 ∈ ℂ )
212 84 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · ( 𝑈 + 1 ) ) ∈ ℂ )
213 211 212 175 mul32d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · 𝑇 ) = ( ( 𝑀 · 𝑇 ) · ( 𝑋 · ( 𝑈 + 1 ) ) ) )
214 211 175 mulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 · 𝑇 ) ∈ ℂ )
215 83 recnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑈 + 1 ) ∈ ℂ )
216 214 91 215 mul12d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · 𝑇 ) · ( 𝑋 · ( 𝑈 + 1 ) ) ) = ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) )
217 213 216 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · 𝑇 ) = ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) )
218 217 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · 𝑇 ) ) = ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) ) )
219 210 218 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · ( 𝑋 · ( 𝑈 + 1 ) ) ) · ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · 𝑇 ) ) = ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) ) )
220 207 219 breqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) ≤ ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) ) )
221 66 34 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑀 · 𝑇 ) ∈ ℝ )
222 221 83 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ∈ ℝ )
223 68 222 remulcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) ∈ ℝ )
224 119 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → 𝑋 ∈ ℤ )
225 58 224 rpexpcld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) ∈ ℝ+ )
226 64 223 225 ledivmuld ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) / ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) ) ≤ ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) ↔ ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) ≤ ( ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) · ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) ) ) )
227 220 226 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑁 ) ↑ 𝑋 ) / ( ( 𝑇 ↑𝑐 𝑈 ) ↑ 𝑋 ) ) ≤ ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) )
228 62 227 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑁 ) / ( 𝑇 ↑𝑐 𝑈 ) ) ↑ 𝑋 ) ≤ ( 𝑋 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) )