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	mulridd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ ) → ( 𝑋 · 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 ) ) ) )