ostth2lem3

	Ref	Expression
Hypotheses	qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	qabsabv.a	$⊢ A = AbsVal (Q)$
	padic.j	$⊢ J = (q \in ℙ ⟼ (x \in ℚ ⟼ if (x = 0, 0, q^{- (q pCnt x)})))$
	ostth.k	$⊢ K = (x \in ℚ ⟼ if (x = 0, 0, 1))$
	ostth.1	$⊢ φ \to F \in A$
	ostth2.2	$⊢ φ \to N \in ℤ_{\geq 2}$
	ostth2.3	$⊢ φ \to 1 < F (N)$
	ostth2.4	$⊢ R = \frac{\log F (N)}{\log N}$
	ostth2.5	$⊢ φ \to M \in ℤ_{\geq 2}$
	ostth2.6	$⊢ S = \frac{\log F (M)}{\log M}$
	ostth2.7	$⊢ T = if (F (M) \leq 1, 1, F (M))$
	ostth2.8	$⊢ U = \frac{\log N}{\log M}$
Assertion	ostth2lem3	$⊢ (φ \land X \in ℕ) \to {(\frac{F (N)}{T^{U}})}^{X} \leq X M T (U + 1)$

Proof

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

Metamath Proof Explorer

Theorem ostth2lem3

Proof