aks4d1p1p5

Description: Show inequality for existence of a non-divisor. (Contributed by metakunt, 19-Aug-2024)

	Ref	Expression
Hypotheses	aks4d1p1p5.1	$⊢ φ \to N \in ℕ$
	aks4d1p1p5.2	$⊢ A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
	aks4d1p1p5.3	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
	aks4d1p1p5.4	$⊢ φ \to 4 \leq N$
	aks4d1p1p5.5	$⊢ C = \log_{2} ({\log_{2} N}^{5} + 1)$
	aks4d1p1p5.6	$⊢ D = {\log_{2} N}^{2}$
	aks4d1p1p5.7	$⊢ E = {\log_{2} N}^{4}$
Assertion	aks4d1p1p5	$⊢ φ \to A < 2^{B}$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1p5.1	$⊢ φ \to N \in ℕ$
2		aks4d1p1p5.2	$⊢ A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
3		aks4d1p1p5.3	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
4		aks4d1p1p5.4	$⊢ φ \to 4 \leq N$
5		aks4d1p1p5.5	$⊢ C = \log_{2} ({\log_{2} N}^{5} + 1)$
6		aks4d1p1p5.6	$⊢ D = {\log_{2} N}^{2}$
7		aks4d1p1p5.7	$⊢ E = {\log_{2} N}^{4}$
8		3re	$⊢ 3 \in ℝ$
9	8	a1i	$⊢ φ \to 3 \in ℝ$
10		4re	$⊢ 4 \in ℝ$
11	10	a1i	$⊢ φ \to 4 \in ℝ$
12	1	nnred	$⊢ φ \to N \in ℝ$
13	9	lep1d	$⊢ φ \to 3 \leq 3 + 1$
14		3p1e4	$⊢ 3 + 1 = 4$
15	13 14	breqtrdi	$⊢ φ \to 3 \leq 4$
16	9 11 12 15 4	letrd	$⊢ φ \to 3 \leq N$
17		2re	$⊢ 2 \in ℝ$
18	17	a1i	$⊢ (φ \land x \in [4, N]) \to 2 \in ℝ$
19		2pos	$⊢ 0 < 2$
20	19	a1i	$⊢ (φ \land x \in [4, N]) \to 0 < 2$
21		elicc2	$⊢ (4 \in ℝ \land N \in ℝ) \to (x \in [4, N] \leftrightarrow (x \in ℝ \land 4 \leq x \land x \leq N))$
22	11 12 21	syl2anc	$⊢ φ \to (x \in [4, N] \leftrightarrow (x \in ℝ \land 4 \leq x \land x \leq N))$
23	22	biimpd	$⊢ φ \to (x \in [4, N] \to (x \in ℝ \land 4 \leq x \land x \leq N))$
24	23	imp	$⊢ (φ \land x \in [4, N]) \to (x \in ℝ \land 4 \leq x \land x \leq N)$
25	24	simp1d	$⊢ (φ \land x \in [4, N]) \to x \in ℝ$
26		0red	$⊢ φ \to 0 \in ℝ$
27	26	adantr	$⊢ (φ \land x \in [4, N]) \to 0 \in ℝ$
28	10	a1i	$⊢ (φ \land x \in [4, N]) \to 4 \in ℝ$
29		4pos	$⊢ 0 < 4$
30	29	a1i	$⊢ (φ \land x \in [4, N]) \to 0 < 4$
31	24	simp2d	$⊢ (φ \land x \in [4, N]) \to 4 \leq x$
32	27 28 25 30 31	ltletrd	$⊢ (φ \land x \in [4, N]) \to 0 < x$
33		1red	$⊢ φ \to 1 \in ℝ$
34		1lt2	$⊢ 1 < 2$
35	34	a1i	$⊢ φ \to 1 < 2$
36	33 35	ltned	$⊢ φ \to 1 \neq 2$
37	36	necomd	$⊢ φ \to 2 \neq 1$
38	37	adantr	$⊢ (φ \land x \in [4, N]) \to 2 \neq 1$
39	18 20 25 32 38	relogbcld	$⊢ (φ \land x \in [4, N]) \to \log_{2} x \in ℝ$
40		5nn0	$⊢ 5 \in ℕ_{0}$
41	40	a1i	$⊢ (φ \land x \in [4, N]) \to 5 \in ℕ_{0}$
42	39 41	reexpcld	$⊢ (φ \land x \in [4, N]) \to {\log_{2} x}^{5} \in ℝ$
43		1red	$⊢ (φ \land x \in [4, N]) \to 1 \in ℝ$
44	42 43	readdcld	$⊢ (φ \land x \in [4, N]) \to {\log_{2} x}^{5} + 1 \in ℝ$
45	27 43	readdcld	$⊢ (φ \land x \in [4, N]) \to 0 + 1 \in ℝ$
46	27	ltp1d	$⊢ (φ \land x \in [4, N]) \to 0 < 0 + 1$
47	41	nn0zd	$⊢ (φ \land x \in [4, N]) \to 5 \in ℤ$
48		ax-resscn	$⊢ ℝ \subseteq ℂ$
49	48 18	sselid	$⊢ (φ \land x \in [4, N]) \to 2 \in ℂ$
50	27 20	gtned	$⊢ (φ \land x \in [4, N]) \to 2 \neq 0$
51		logb1	$⊢ (2 \in ℂ \land 2 \neq 0 \land 2 \neq 1) \to \log_{2} 1 = 0$
52	49 50 38 51	syl3anc	$⊢ (φ \land x \in [4, N]) \to \log_{2} 1 = 0$
53		1lt4	$⊢ 1 < 4$
54	53	a1i	$⊢ (φ \land x \in [4, N]) \to 1 < 4$
55	43 28 25 54 31	ltletrd	$⊢ (φ \land x \in [4, N]) \to 1 < x$
56		2z	$⊢ 2 \in ℤ$
57	56	a1i	$⊢ (φ \land x \in [4, N]) \to 2 \in ℤ$
58	57	uzidd	$⊢ (φ \land x \in [4, N]) \to 2 \in ℤ_{\geq 2}$
59		1rp	$⊢ 1 \in ℝ^{+}$
60	59	a1i	$⊢ (φ \land x \in [4, N]) \to 1 \in ℝ^{+}$
61	25 32	elrpd	$⊢ (φ \land x \in [4, N]) \to x \in ℝ^{+}$
62		logblt	$⊢ (2 \in ℤ_{\geq 2} \land 1 \in ℝ^{+} \land x \in ℝ^{+}) \to (1 < x \leftrightarrow \log_{2} 1 < \log_{2} x)$
63	58 60 61 62	syl3anc	$⊢ (φ \land x \in [4, N]) \to (1 < x \leftrightarrow \log_{2} 1 < \log_{2} x)$
64	55 63	mpbid	$⊢ (φ \land x \in [4, N]) \to \log_{2} 1 < \log_{2} x$
65	52 64	eqbrtrrd	$⊢ (φ \land x \in [4, N]) \to 0 < \log_{2} x$
66		expgt0	$⊢ (\log_{2} x \in ℝ \land 5 \in ℤ \land 0 < \log_{2} x) \to 0 < {\log_{2} x}^{5}$
67	39 47 65 66	syl3anc	$⊢ (φ \land x \in [4, N]) \to 0 < {\log_{2} x}^{5}$
68	27 42 43 67	ltadd1dd	$⊢ (φ \land x \in [4, N]) \to 0 + 1 < {\log_{2} x}^{5} + 1$
69	27 45 44 46 68	lttrd	$⊢ (φ \land x \in [4, N]) \to 0 < {\log_{2} x}^{5} + 1$
70	18 20 44 69 38	relogbcld	$⊢ (φ \land x \in [4, N]) \to \log_{2} ({\log_{2} x}^{5} + 1) \in ℝ$
71	18 70	remulcld	$⊢ (φ \land x \in [4, N]) \to 2 \log_{2} ({\log_{2} x}^{5} + 1) \in ℝ$
72		0red	$⊢ (φ \land x \in [4, N]) \to 0 \in ℝ$
73		simpr	$⊢ (φ \land x \in [4, N]) \to x \in [4, N]$
74	11 12	jca	$⊢ φ \to (4 \in ℝ \land N \in ℝ)$
75	74	adantr	$⊢ (φ \land x \in [4, N]) \to (4 \in ℝ \land N \in ℝ)$
76	75 21	syl	$⊢ (φ \land x \in [4, N]) \to (x \in [4, N] \leftrightarrow (x \in ℝ \land 4 \leq x \land x \leq N))$
77	73 76	mpbid	$⊢ (φ \land x \in [4, N]) \to (x \in ℝ \land 4 \leq x \land x \leq N)$
78	77	simp2d	$⊢ (φ \land x \in [4, N]) \to 4 \leq x$
79	72 28 25 30 78	ltletrd	$⊢ (φ \land x \in [4, N]) \to 0 < x$
80	18 20 25 79 38	relogbcld	$⊢ (φ \land x \in [4, N]) \to \log_{2} x \in ℝ$
81	80	resqcld	$⊢ (φ \land x \in [4, N]) \to {\log_{2} x}^{2} \in ℝ$
82	71 81	readdcld	$⊢ (φ \land x \in [4, N]) \to 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2} \in ℝ$
83	82	fmpttd	$⊢ φ \to (x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : [4, N] ⟶ ℝ$
84	48	a1i	$⊢ φ \to ℝ \subseteq ℂ$
85		3lt4	$⊢ 3 < 4$
86	85	a1i	$⊢ φ \to 3 < 4$
87	12 33	readdcld	$⊢ φ \to N + 1 \in ℝ$
88	12	ltp1d	$⊢ φ \to N < N + 1$
89	11 12 87 4 88	lelttrd	$⊢ φ \to 4 < N + 1$
90	86 89	jca	$⊢ φ \to (3 < 4 \land 4 < N + 1)$
91	9	rexrd	$⊢ φ \to 3 \in ℝ^{*}$
92	87	rexrd	$⊢ φ \to N + 1 \in ℝ^{*}$
93	11	rexrd	$⊢ φ \to 4 \in ℝ^{*}$
94		elioo5	$⊢ (3 \in ℝ^{} \land N + 1 \in ℝ^{} \land 4 \in ℝ^{*}) \to (4 \in (3, N + 1) \leftrightarrow (3 < 4 \land 4 < N + 1))$
95	91 92 93 94	syl3anc	$⊢ φ \to (4 \in (3, N + 1) \leftrightarrow (3 < 4 \land 4 < N + 1))$
96	90 95	mpbird	$⊢ φ \to 4 \in (3, N + 1)$
97	9 11 12 86 4	ltletrd	$⊢ φ \to 3 < N$
98	97 88	jca	$⊢ φ \to (3 < N \land N < N + 1)$
99	12	rexrd	$⊢ φ \to N \in ℝ^{*}$
100		elioo5	$⊢ (3 \in ℝ^{} \land N + 1 \in ℝ^{} \land N \in ℝ^{*}) \to (N \in (3, N + 1) \leftrightarrow (3 < N \land N < N + 1))$
101	91 92 99 100	syl3anc	$⊢ φ \to (N \in (3, N + 1) \leftrightarrow (3 < N \land N < N + 1))$
102	98 101	mpbird	$⊢ φ \to N \in (3, N + 1)$
103		iccssioo2	$⊢ (4 \in (3, N + 1) \land N \in (3, N + 1)) \to [4, N] \subseteq (3, N + 1)$
104	96 102 103	syl2anc	$⊢ φ \to [4, N] \subseteq (3, N + 1)$
105	104	resmptd	$⊢ φ \to {(x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) ↾}_{[4, N]} = (x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})$
106		2cnd	$⊢ (φ \land x \in (3, N + 1)) \to 2 \in ℂ$
107	17	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 2 \in ℝ$
108	19	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 0 < 2$
109		elioore	$⊢ x \in (3, N + 1) \to x \in ℝ$
110	109	adantl	$⊢ (φ \land x \in (3, N + 1)) \to x \in ℝ$
111		0red	$⊢ (φ \land x \in (3, N + 1)) \to 0 \in ℝ$
112	8	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 3 \in ℝ$
113		3pos	$⊢ 0 < 3$
114	113	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 0 < 3$
115		eliooord	$⊢ x \in (3, N + 1) \to (3 < x \land x < N + 1)$
116		simpl	$⊢ (3 < x \land x < N + 1) \to 3 < x$
117	115 116	syl	$⊢ x \in (3, N + 1) \to 3 < x$
118	117	adantl	$⊢ (φ \land x \in (3, N + 1)) \to 3 < x$
119	111 112 110 114 118	lttrd	$⊢ (φ \land x \in (3, N + 1)) \to 0 < x$
120	37	adantr	$⊢ (φ \land x \in (3, N + 1)) \to 2 \neq 1$
121	107 108 110 119 120	relogbcld	$⊢ (φ \land x \in (3, N + 1)) \to \log_{2} x \in ℝ$
122	40	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 5 \in ℕ_{0}$
123	121 122	reexpcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log_{2} x}^{5} \in ℝ$
124		1red	$⊢ (φ \land x \in (3, N + 1)) \to 1 \in ℝ$
125	123 124	readdcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log_{2} x}^{5} + 1 \in ℝ$
126	111 124	readdcld	$⊢ (φ \land x \in (3, N + 1)) \to 0 + 1 \in ℝ$
127	111	ltp1d	$⊢ (φ \land x \in (3, N + 1)) \to 0 < 0 + 1$
128	122	nn0zd	$⊢ (φ \land x \in (3, N + 1)) \to 5 \in ℤ$
129	34	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 1 < 2$
130		2lt3	$⊢ 2 < 3$
131	130	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 2 < 3$
132	124 107 112 129 131	lttrd	$⊢ (φ \land x \in (3, N + 1)) \to 1 < 3$
133	124 112 110 132 118	lttrd	$⊢ (φ \land x \in (3, N + 1)) \to 1 < x$
134	110 119	elrpd	$⊢ (φ \land x \in (3, N + 1)) \to x \in ℝ^{+}$
135		2rp	$⊢ 2 \in ℝ^{+}$
136	135	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 2 \in ℝ^{+}$
137	134 136 129	jca32	$⊢ (φ \land x \in (3, N + 1)) \to (x \in ℝ^{+} \land (2 \in ℝ^{+} \land 1 < 2))$
138		logbgt0b	$⊢ (x \in ℝ^{+} \land (2 \in ℝ^{+} \land 1 < 2)) \to (0 < \log_{2} x \leftrightarrow 1 < x)$
139	137 138	syl	$⊢ (φ \land x \in (3, N + 1)) \to (0 < \log_{2} x \leftrightarrow 1 < x)$
140	133 139	mpbird	$⊢ (φ \land x \in (3, N + 1)) \to 0 < \log_{2} x$
141	121 128 140 66	syl3anc	$⊢ (φ \land x \in (3, N + 1)) \to 0 < {\log_{2} x}^{5}$
142	111 123 124 141	ltadd1dd	$⊢ (φ \land x \in (3, N + 1)) \to 0 + 1 < {\log_{2} x}^{5} + 1$
143	111 126 125 127 142	lttrd	$⊢ (φ \land x \in (3, N + 1)) \to 0 < {\log_{2} x}^{5} + 1$
144	124 129	ltned	$⊢ (φ \land x \in (3, N + 1)) \to 1 \neq 2$
145	144	necomd	$⊢ (φ \land x \in (3, N + 1)) \to 2 \neq 1$
146	107 108 125 143 145	relogbcld	$⊢ (φ \land x \in (3, N + 1)) \to \log_{2} ({\log_{2} x}^{5} + 1) \in ℝ$
147	146	recnd	$⊢ (φ \land x \in (3, N + 1)) \to \log_{2} ({\log_{2} x}^{5} + 1) \in ℂ$
148	106 147	mulcld	$⊢ (φ \land x \in (3, N + 1)) \to 2 \log_{2} ({\log_{2} x}^{5} + 1) \in ℂ$
149	48 121	sselid	$⊢ (φ \land x \in (3, N + 1)) \to \log_{2} x \in ℂ$
150	149	sqcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log_{2} x}^{2} \in ℂ$
151	148 150	addcld	$⊢ (φ \land x \in (3, N + 1)) \to 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2} \in ℂ$
152	151	fmpttd	$⊢ φ \to (x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : (3, N + 1) ⟶ ℂ$
153		ioossre	$⊢ (3, N + 1) \subseteq ℝ$
154	153	a1i	$⊢ φ \to (3, N + 1) \subseteq ℝ$
155	84 152 154	3jca	$⊢ φ \to (ℝ \subseteq ℂ \land (x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : (3, N + 1) ⟶ ℂ \land (3, N + 1) \subseteq ℝ)$
156	136	relogcld	$⊢ (φ \land x \in (3, N + 1)) \to \log 2 \in ℝ$
157	125 156	remulcld	$⊢ (φ \land x \in (3, N + 1)) \to ({\log_{2} x}^{5} + 1) \log 2 \in ℝ$
158	48 123	sselid	$⊢ (φ \land x \in (3, N + 1)) \to {\log_{2} x}^{5} \in ℂ$
159		1cnd	$⊢ (φ \land x \in (3, N + 1)) \to 1 \in ℂ$
160	158 159	addcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log_{2} x}^{5} + 1 \in ℂ$
161	111 108	gtned	$⊢ (φ \land x \in (3, N + 1)) \to 2 \neq 0$
162	106 161	logcld	$⊢ (φ \land x \in (3, N + 1)) \to \log 2 \in ℂ$
163	111 143	gtned	$⊢ (φ \land x \in (3, N + 1)) \to {\log_{2} x}^{5} + 1 \neq 0$
164		loggt0b	$⊢ 2 \in ℝ^{+} \to (0 < \log 2 \leftrightarrow 1 < 2)$
165	135 164	ax-mp	$⊢ 0 < \log 2 \leftrightarrow 1 < 2$
166	35 165	sylibr	$⊢ φ \to 0 < \log 2$
167	26 166	ltned	$⊢ φ \to 0 \neq \log 2$
168	167	necomd	$⊢ φ \to \log 2 \neq 0$
169	168	adantr	$⊢ (φ \land x \in (3, N + 1)) \to \log 2 \neq 0$
170	160 162 163 169	mulne0d	$⊢ (φ \land x \in (3, N + 1)) \to ({\log_{2} x}^{5} + 1) \log 2 \neq 0$
171	124 157 170	redivcld	$⊢ (φ \land x \in (3, N + 1)) \to \frac{1}{({\log_{2} x}^{5} + 1) \log 2} \in ℝ$
172		5re	$⊢ 5 \in ℝ$
173	172	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 5 \in ℝ$
174		4nn0	$⊢ 4 \in ℕ_{0}$
175	174	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 4 \in ℕ_{0}$
176	121 175	reexpcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log_{2} x}^{4} \in ℝ$
177	173 176	remulcld	$⊢ (φ \land x \in (3, N + 1)) \to 5 {\log_{2} x}^{4} \in ℝ$
178	110 156	remulcld	$⊢ (φ \land x \in (3, N + 1)) \to x \log 2 \in ℝ$
179	48 110	sselid	$⊢ (φ \land x \in (3, N + 1)) \to x \in ℂ$
180	111 119	gtned	$⊢ (φ \land x \in (3, N + 1)) \to x \neq 0$
181	179 162 180 169	mulne0d	$⊢ (φ \land x \in (3, N + 1)) \to x \log 2 \neq 0$
182	124 178 181	redivcld	$⊢ (φ \land x \in (3, N + 1)) \to \frac{1}{x \log 2} \in ℝ$
183	177 182	remulcld	$⊢ (φ \land x \in (3, N + 1)) \to 5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) \in ℝ$
184	183 111	readdcld	$⊢ (φ \land x \in (3, N + 1)) \to 5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0 \in ℝ$
185	171 184	remulcld	$⊢ (φ \land x \in (3, N + 1)) \to (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) \in ℝ$
186	107 185	remulcld	$⊢ (φ \land x \in (3, N + 1)) \to 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) \in ℝ$
187	156	resqcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log 2}^{2} \in ℝ$
188	56	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 2 \in ℤ$
189	162 169 188	expne0d	$⊢ (φ \land x \in (3, N + 1)) \to {\log 2}^{2} \neq 0$
190	107 187 189	redivcld	$⊢ (φ \land x \in (3, N + 1)) \to \frac{2}{{\log 2}^{2}} \in ℝ$
191	134	relogcld	$⊢ (φ \land x \in (3, N + 1)) \to \log x \in ℝ$
192		2m1e1	$⊢ 2 - 1 = 1$
193		1nn0	$⊢ 1 \in ℕ_{0}$
194	192 193	eqeltri	$⊢ 2 - 1 \in ℕ_{0}$
195	194	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 2 - 1 \in ℕ_{0}$
196	191 195	reexpcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log x}^{2 - 1} \in ℝ$
197	196 110 180	redivcld	$⊢ (φ \land x \in (3, N + 1)) \to \frac{{\log x}^{2 - 1}}{x} \in ℝ$
198	190 197	remulcld	$⊢ (φ \land x \in (3, N + 1)) \to (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}) \in ℝ$
199	186 198	readdcld	$⊢ (φ \land x \in (3, N + 1)) \to 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}) \in ℝ$
200	199	ralrimiva	$⊢ φ \to \forall x \in (3, N + 1) 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}) \in ℝ$
201		nfcv	$⊢ \underline{Ⅎ} x (3, N + 1)$
202	201	fnmptf	$⊢ \forall x \in (3, N + 1) 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}) \in ℝ \to (x \in (3, N + 1) ⟼ 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x})) Fn (3, N + 1)$
203	200 202	syl	$⊢ φ \to (x \in (3, N + 1) ⟼ 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x})) Fn (3, N + 1)$
204	9	leidd	$⊢ φ \to 3 \leq 3$
205	12	lep1d	$⊢ φ \to N \leq N + 1$
206	9 12 87 16 205	letrd	$⊢ φ \to 3 \leq N + 1$
207	9 87 204 206	aks4d1p1p6	$⊢ φ \to \frac{d (x \in (3, N + 1)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})}{d_{ℝ} x} = (x \in (3, N + 1) ⟼ 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}))$
208	207	fneq1d	$⊢ φ \to (\frac{d (x \in (3, N + 1)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})}{d_{ℝ} x} Fn (3, N + 1) \leftrightarrow (x \in (3, N + 1) ⟼ 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x})) Fn (3, N + 1))$
209	203 208	mpbird	$⊢ φ \to \frac{d (x \in (3, N + 1)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})}{d_{ℝ} x} Fn (3, N + 1)$
210	209	fndmd	$⊢ φ \to dom \frac{d (x \in (3, N + 1)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})}{d_{ℝ} x} = (3, N + 1)$
211		dvcn	$⊢ ((ℝ \subseteq ℂ \land (x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : (3, N + 1) ⟶ ℂ \land (3, N + 1) \subseteq ℝ) \land dom \frac{d (x \in (3, N + 1)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})}{d_{ℝ} x} = (3, N + 1)) \to (x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : (3, N + 1) \underset{cn}{⟶} ℂ$
212	155 210 211	syl2anc	$⊢ φ \to (x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : (3, N + 1) \underset{cn}{⟶} ℂ$
213		rescncf	$⊢ [4, N] \subseteq (3, N + 1) \to ((x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : (3, N + 1) \underset{cn}{⟶} ℂ \to ({(x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) ↾}_{[4, N]}) : [4, N] \underset{cn}{⟶} ℂ)$
214	104 213	syl	$⊢ φ \to ((x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : (3, N + 1) \underset{cn}{⟶} ℂ \to ({(x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) ↾}_{[4, N]}) : [4, N] \underset{cn}{⟶} ℂ)$
215	212 214	mpd	$⊢ φ \to ({(x \in (3, N + 1) ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) ↾}_{[4, N]}) : [4, N] \underset{cn}{⟶} ℂ$
216	105 215	eqeltrrd	$⊢ φ \to (x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : [4, N] \underset{cn}{⟶} ℂ$
217		cncffvrn	$⊢ (ℝ \subseteq ℂ \land (x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : [4, N] \underset{cn}{⟶} ℂ) \to ((x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : [4, N] \underset{cn}{⟶} ℝ \leftrightarrow (x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : [4, N] ⟶ ℝ)$
218	84 216 217	syl2anc	$⊢ φ \to ((x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : [4, N] \underset{cn}{⟶} ℝ \leftrightarrow (x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : [4, N] ⟶ ℝ)$
219	83 218	mpbird	$⊢ φ \to (x \in [4, N] ⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2}) : [4, N] \underset{cn}{⟶} ℝ$
220	174	a1i	$⊢ (φ \land x \in [4, N]) \to 4 \in ℕ_{0}$
221	39 220	reexpcld	$⊢ (φ \land x \in [4, N]) \to {\log_{2} x}^{4} \in ℝ$
222	221	fmpttd	$⊢ φ \to (x \in [4, N] ⟼ {\log_{2} x}^{4}) : [4, N] ⟶ ℝ$
223	104	resmptd	$⊢ φ \to {(x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) ↾}_{[4, N]} = (x \in [4, N] ⟼ {\log_{2} x}^{4})$
224	48 176	sselid	$⊢ (φ \land x \in (3, N + 1)) \to {\log_{2} x}^{4} \in ℂ$
225	224	fmpttd	$⊢ φ \to (x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) : (3, N + 1) ⟶ ℂ$
226	84 225 154	3jca	$⊢ φ \to (ℝ \subseteq ℂ \land (x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) : (3, N + 1) ⟶ ℂ \land (3, N + 1) \subseteq ℝ)$
227	10	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 4 \in ℝ$
228	156 175	reexpcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log 2}^{4} \in ℝ$
229		4z	$⊢ 4 \in ℤ$
230	229	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 4 \in ℤ$
231	162 169 230	expne0d	$⊢ (φ \land x \in (3, N + 1)) \to {\log 2}^{4} \neq 0$
232	227 228 231	redivcld	$⊢ (φ \land x \in (3, N + 1)) \to \frac{4}{{\log 2}^{4}} \in ℝ$
233		4m1e3	$⊢ 4 - 1 = 3$
234		3nn0	$⊢ 3 \in ℕ_{0}$
235	233 234	eqeltri	$⊢ 4 - 1 \in ℕ_{0}$
236	235	a1i	$⊢ (φ \land x \in (3, N + 1)) \to 4 - 1 \in ℕ_{0}$
237	191 236	reexpcld	$⊢ (φ \land x \in (3, N + 1)) \to {\log x}^{4 - 1} \in ℝ$
238	237 110 180	redivcld	$⊢ (φ \land x \in (3, N + 1)) \to \frac{{\log x}^{4 - 1}}{x} \in ℝ$
239	232 238	remulcld	$⊢ (φ \land x \in (3, N + 1)) \to (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x}) \in ℝ$
240	239	ralrimiva	$⊢ φ \to \forall x \in (3, N + 1) (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x}) \in ℝ$
241	201	fnmptf	$⊢ \forall x \in (3, N + 1) (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x}) \in ℝ \to (x \in (3, N + 1) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x})) Fn (3, N + 1)$
242	240 241	syl	$⊢ φ \to (x \in (3, N + 1) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x})) Fn (3, N + 1)$
243	113	a1i	$⊢ φ \to 0 < 3$
244		eqid	$⊢ (x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) = (x \in (3, N + 1) ⟼ {\log_{2} x}^{4})$
245		eqid	$⊢ (x \in (3, N + 1) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x})) = (x \in (3, N + 1) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x}))$
246		eqid	$⊢ \frac{4}{{\log 2}^{4}} = \frac{4}{{\log 2}^{4}}$
247		4nn	$⊢ 4 \in ℕ$
248	247	a1i	$⊢ φ \to 4 \in ℕ$
249	9 87 243 206 244 245 246 248	dvrelogpow2b	$⊢ φ \to \frac{d (x \in (3, N + 1)⟼ {\log_{2} x}^{4})}{d_{ℝ} x} = (x \in (3, N + 1) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x}))$
250	249	fneq1d	$⊢ φ \to (\frac{d (x \in (3, N + 1)⟼ {\log_{2} x}^{4})}{d_{ℝ} x} Fn (3, N + 1) \leftrightarrow (x \in (3, N + 1) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x})) Fn (3, N + 1))$
251	242 250	mpbird	$⊢ φ \to \frac{d (x \in (3, N + 1)⟼ {\log_{2} x}^{4})}{d_{ℝ} x} Fn (3, N + 1)$
252	251	fndmd	$⊢ φ \to dom \frac{d (x \in (3, N + 1)⟼ {\log_{2} x}^{4})}{d_{ℝ} x} = (3, N + 1)$
253		dvcn	$⊢ ((ℝ \subseteq ℂ \land (x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) : (3, N + 1) ⟶ ℂ \land (3, N + 1) \subseteq ℝ) \land dom \frac{d (x \in (3, N + 1)⟼ {\log_{2} x}^{4})}{d_{ℝ} x} = (3, N + 1)) \to (x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) : (3, N + 1) \underset{cn}{⟶} ℂ$
254	226 252 253	syl2anc	$⊢ φ \to (x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) : (3, N + 1) \underset{cn}{⟶} ℂ$
255		rescncf	$⊢ [4, N] \subseteq (3, N + 1) \to ((x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) : (3, N + 1) \underset{cn}{⟶} ℂ \to ({(x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) ↾}_{[4, N]}) : [4, N] \underset{cn}{⟶} ℂ)$
256	104 255	syl	$⊢ φ \to ((x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) : (3, N + 1) \underset{cn}{⟶} ℂ \to ({(x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) ↾}_{[4, N]}) : [4, N] \underset{cn}{⟶} ℂ)$
257	254 256	mpd	$⊢ φ \to ({(x \in (3, N + 1) ⟼ {\log_{2} x}^{4}) ↾}_{[4, N]}) : [4, N] \underset{cn}{⟶} ℂ$
258	223 257	eqeltrrd	$⊢ φ \to (x \in [4, N] ⟼ {\log_{2} x}^{4}) : [4, N] \underset{cn}{⟶} ℂ$
259		cncffvrn	$⊢ (ℝ \subseteq ℂ \land (x \in [4, N] ⟼ {\log_{2} x}^{4}) : [4, N] \underset{cn}{⟶} ℂ) \to ((x \in [4, N] ⟼ {\log_{2} x}^{4}) : [4, N] \underset{cn}{⟶} ℝ \leftrightarrow (x \in [4, N] ⟼ {\log_{2} x}^{4}) : [4, N] ⟶ ℝ)$
260	84 258 259	syl2anc	$⊢ φ \to ((x \in [4, N] ⟼ {\log_{2} x}^{4}) : [4, N] \underset{cn}{⟶} ℝ \leftrightarrow (x \in [4, N] ⟼ {\log_{2} x}^{4}) : [4, N] ⟶ ℝ)$
261	222 260	mpbird	$⊢ φ \to (x \in [4, N] ⟼ {\log_{2} x}^{4}) : [4, N] \underset{cn}{⟶} ℝ$
262	11 12 15 4	aks4d1p1p6	$⊢ φ \to \frac{d (x \in (4, N)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})}{d_{ℝ} x} = (x \in (4, N) ⟼ 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}))$
263	29	a1i	$⊢ φ \to 0 < 4$
264		eqid	$⊢ (x \in (4, N) ⟼ {\log_{2} x}^{4}) = (x \in (4, N) ⟼ {\log_{2} x}^{4})$
265		eqid	$⊢ (x \in (4, N) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x})) = (x \in (4, N) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x}))$
266	11 12 263 4 264 265 246 248	dvrelogpow2b	$⊢ φ \to \frac{d (x \in (4, N)⟼ {\log_{2} x}^{4})}{d_{ℝ} x} = (x \in (4, N) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x}))$
267	233	a1i	$⊢ (φ \land x \in (4, N)) \to 4 - 1 = 3$
268	267	oveq2d	$⊢ (φ \land x \in (4, N)) \to {\log x}^{4 - 1} = {\log x}^{3}$
269	268	oveq1d	$⊢ (φ \land x \in (4, N)) \to \frac{{\log x}^{4 - 1}}{x} = \frac{{\log x}^{3}}{x}$
270	269	oveq2d	$⊢ (φ \land x \in (4, N)) \to (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x}) = (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{3}}{x})$
271	270	mpteq2dva	$⊢ φ \to (x \in (4, N) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{4 - 1}}{x})) = (x \in (4, N) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{3}}{x}))$
272	266 271	eqtrd	$⊢ φ \to \frac{d (x \in (4, N)⟼ {\log_{2} x}^{4})}{d_{ℝ} x} = (x \in (4, N) ⟼ (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{3}}{x}))$
273		elioore	$⊢ x \in (4, N) \to x \in ℝ$
274	273	adantl	$⊢ (φ \land x \in (4, N)) \to x \in ℝ$
275	10	a1i	$⊢ (φ \land x \in (4, N)) \to 4 \in ℝ$
276		eliooord	$⊢ x \in (4, N) \to (4 < x \land x < N)$
277	276	simpld	$⊢ x \in (4, N) \to 4 < x$
278	277	adantl	$⊢ (φ \land x \in (4, N)) \to 4 < x$
279	275 274 278	ltled	$⊢ (φ \land x \in (4, N)) \to 4 \leq x$
280	274 279	aks4d1p1p7	$⊢ (φ \land x \in (4, N)) \to 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}) \leq (\frac{4}{{\log 2}^{4}}) (\frac{{\log x}^{3}}{x})$
281		oveq2	$⊢ x = 4 \to \log_{2} x = \log_{2} 4$
282	281	oveq1d	$⊢ x = 4 \to {\log_{2} x}^{5} = {\log_{2} 4}^{5}$
283	282	oveq1d	$⊢ x = 4 \to {\log_{2} x}^{5} + 1 = {\log_{2} 4}^{5} + 1$
284	283	oveq2d	$⊢ x = 4 \to \log_{2} ({\log_{2} x}^{5} + 1) = \log_{2} ({\log_{2} 4}^{5} + 1)$
285	284	oveq2d	$⊢ x = 4 \to 2 \log_{2} ({\log_{2} x}^{5} + 1) = 2 \log_{2} ({\log_{2} 4}^{5} + 1)$
286	281	oveq1d	$⊢ x = 4 \to {\log_{2} x}^{2} = {\log_{2} 4}^{2}$
287	285 286	oveq12d	$⊢ x = 4 \to 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2} = 2 \log_{2} ({\log_{2} 4}^{5} + 1) + {\log_{2} 4}^{2}$
288	281	oveq1d	$⊢ x = 4 \to {\log_{2} x}^{4} = {\log_{2} 4}^{4}$
289		oveq2	$⊢ x = N \to \log_{2} x = \log_{2} N$
290	289	oveq1d	$⊢ x = N \to {\log_{2} x}^{5} = {\log_{2} N}^{5}$
291	290	oveq1d	$⊢ x = N \to {\log_{2} x}^{5} + 1 = {\log_{2} N}^{5} + 1$
292	291	oveq2d	$⊢ x = N \to \log_{2} ({\log_{2} x}^{5} + 1) = \log_{2} ({\log_{2} N}^{5} + 1)$
293	292	oveq2d	$⊢ x = N \to 2 \log_{2} ({\log_{2} x}^{5} + 1) = 2 \log_{2} ({\log_{2} N}^{5} + 1)$
294	5	a1i	$⊢ x = N \to C = \log_{2} ({\log_{2} N}^{5} + 1)$
295	294	oveq2d	$⊢ x = N \to 2 C = 2 \log_{2} ({\log_{2} N}^{5} + 1)$
296	295	eqcomd	$⊢ x = N \to 2 \log_{2} ({\log_{2} N}^{5} + 1) = 2 C$
297	293 296	eqtrd	$⊢ x = N \to 2 \log_{2} ({\log_{2} x}^{5} + 1) = 2 C$
298	289	oveq1d	$⊢ x = N \to {\log_{2} x}^{2} = {\log_{2} N}^{2}$
299	6	a1i	$⊢ x = N \to D = {\log_{2} N}^{2}$
300	299	eqcomd	$⊢ x = N \to {\log_{2} N}^{2} = D$
301	298 300	eqtrd	$⊢ x = N \to {\log_{2} x}^{2} = D$
302	297 301	oveq12d	$⊢ x = N \to 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2} = 2 C + D$
303	289	oveq1d	$⊢ x = N \to {\log_{2} x}^{4} = {\log_{2} N}^{4}$
304	7	a1i	$⊢ x = N \to E = {\log_{2} N}^{4}$
305	304	eqcomd	$⊢ x = N \to {\log_{2} N}^{4} = E$
306	303 305	eqtrd	$⊢ x = N \to {\log_{2} x}^{4} = E$
307		sq2	$⊢ 2^{2} = 4$
308	307	oveq2i	$⊢ \log_{2} 2^{2} = \log_{2} 4$
309	308	a1i	$⊢ φ \to \log_{2} 2^{2} = \log_{2} 4$
310	309	eqcomd	$⊢ φ \to \log_{2} 4 = \log_{2} 2^{2}$
311	135	a1i	$⊢ φ \to 2 \in ℝ^{+}$
312	56	a1i	$⊢ φ \to 2 \in ℤ$
313		relogbexp	$⊢ (2 \in ℝ^{+} \land 2 \neq 1 \land 2 \in ℤ) \to \log_{2} 2^{2} = 2$
314	311 37 312 313	syl3anc	$⊢ φ \to \log_{2} 2^{2} = 2$
315	310 314	eqtrd	$⊢ φ \to \log_{2} 4 = 2$
316	315	oveq1d	$⊢ φ \to {\log_{2} 4}^{5} = 2^{5}$
317	316	oveq1d	$⊢ φ \to {\log_{2} 4}^{5} + 1 = 2^{5} + 1$
318	317	oveq2d	$⊢ φ \to \log_{2} ({\log_{2} 4}^{5} + 1) = \log_{2} (2^{5} + 1)$
319	17	a1i	$⊢ φ \to 2 \in ℝ$
320	319	leidd	$⊢ φ \to 2 \leq 2$
321	315 319	eqeltrd	$⊢ φ \to \log_{2} 4 \in ℝ$
322	40	a1i	$⊢ φ \to 5 \in ℕ_{0}$
323	321 322	reexpcld	$⊢ φ \to {\log_{2} 4}^{5} \in ℝ$
324	316 323	eqeltrrd	$⊢ φ \to 2^{5} \in ℝ$
325	324 33	readdcld	$⊢ φ \to 2^{5} + 1 \in ℝ$
326	322	nn0zd	$⊢ φ \to 5 \in ℤ$
327	19	a1i	$⊢ φ \to 0 < 2$
328	327 315	breqtrrd	$⊢ φ \to 0 < \log_{2} 4$
329	321 326 328	3jca	$⊢ φ \to (\log_{2} 4 \in ℝ \land 5 \in ℤ \land 0 < \log_{2} 4)$
330		expgt0	$⊢ (\log_{2} 4 \in ℝ \land 5 \in ℤ \land 0 < \log_{2} 4) \to 0 < {\log_{2} 4}^{5}$
331	329 330	syl	$⊢ φ \to 0 < {\log_{2} 4}^{5}$
332	331 316	breqtrd	$⊢ φ \to 0 < 2^{5}$
333	324	ltp1d	$⊢ φ \to 2^{5} < 2^{5} + 1$
334	26 324 325 332 333	lttrd	$⊢ φ \to 0 < 2^{5} + 1$
335		6nn0	$⊢ 6 \in ℕ_{0}$
336	335	a1i	$⊢ φ \to 6 \in ℕ_{0}$
337	319 336	reexpcld	$⊢ φ \to 2^{6} \in ℝ$
338	336	nn0zd	$⊢ φ \to 6 \in ℤ$
339		expgt0	$⊢ (2 \in ℝ \land 6 \in ℤ \land 0 < 2) \to 0 < 2^{6}$
340	319 338 327 339	syl3anc	$⊢ φ \to 0 < 2^{6}$
341	324 324	readdcld	$⊢ φ \to 2^{5} + 2^{5} \in ℝ$
342	33 319 35	ltled	$⊢ φ \to 1 \leq 2$
343	319 322 342	expge1d	$⊢ φ \to 1 \leq 2^{5}$
344	33 324 324 343	leadd2dd	$⊢ φ \to 2^{5} + 1 \leq 2^{5} + 2^{5}$
345	341	leidd	$⊢ φ \to 2^{5} + 2^{5} \leq 2^{5} + 2^{5}$
346		df-6	$⊢ 6 = 5 + 1$
347	346	a1i	$⊢ φ \to 6 = 5 + 1$
348	347	oveq2d	$⊢ φ \to 2^{6} = 2^{5 + 1}$
349		2cn	$⊢ 2 \in ℂ$
350	349	a1i	$⊢ φ \to 2 \in ℂ$
351	193	a1i	$⊢ φ \to 1 \in ℕ_{0}$
352	350 351 322	expaddd	$⊢ φ \to 2^{5 + 1} = 2^{5} 2^{1}$
353	348 352	eqtrd	$⊢ φ \to 2^{6} = 2^{5} 2^{1}$
354	350	exp1d	$⊢ φ \to 2^{1} = 2$
355	354	oveq2d	$⊢ φ \to 2^{5} 2^{1} = 2^{5} \cdot 2$
356	353 355	eqtrd	$⊢ φ \to 2^{6} = 2^{5} \cdot 2$
357	48 324	sselid	$⊢ φ \to 2^{5} \in ℂ$
358	357	times2d	$⊢ φ \to 2^{5} \cdot 2 = 2^{5} + 2^{5}$
359	356 358	eqtrd	$⊢ φ \to 2^{6} = 2^{5} + 2^{5}$
360	359	eqcomd	$⊢ φ \to 2^{5} + 2^{5} = 2^{6}$
361	345 360	breqtrd	$⊢ φ \to 2^{5} + 2^{5} \leq 2^{6}$
362	325 341 337 344 361	letrd	$⊢ φ \to 2^{5} + 1 \leq 2^{6}$
363	312 320 325 334 337 340 362	logblebd	$⊢ φ \to \log_{2} (2^{5} + 1) \leq \log_{2} 2^{6}$
364	311 37 338	relogbexpd	$⊢ φ \to \log_{2} 2^{6} = 6$
365	363 364	breqtrd	$⊢ φ \to \log_{2} (2^{5} + 1) \leq 6$
366	318 365	eqbrtrd	$⊢ φ \to \log_{2} ({\log_{2} 4}^{5} + 1) \leq 6$
367		6t2e12	$⊢ 6 \cdot 2 = 12$
368		6cn	$⊢ 6 \in ℂ$
369	368	a1i	$⊢ φ \to 6 \in ℂ$
370		2nn	$⊢ 2 \in ℕ$
371	193 370	decnncl	$⊢ 12 \in ℕ$
372	371	a1i	$⊢ φ \to 12 \in ℕ$
373	372	nnred	$⊢ φ \to 12 \in ℝ$
374	373	recnd	$⊢ φ \to 12 \in ℂ$
375	26 327	gtned	$⊢ φ \to 2 \neq 0$
376	369 350 374 375	ldiv	$⊢ φ \to (6 \cdot 2 = 12 \leftrightarrow 6 = \frac{12}{2})$
377	367 376	mpbii	$⊢ φ \to 6 = \frac{12}{2}$
378	366 377	breqtrd	$⊢ φ \to \log_{2} ({\log_{2} 4}^{5} + 1) \leq \frac{12}{2}$
379	323 33	readdcld	$⊢ φ \to {\log_{2} 4}^{5} + 1 \in ℝ$
380	26 33	readdcld	$⊢ φ \to 0 + 1 \in ℝ$
381	26	ltp1d	$⊢ φ \to 0 < 0 + 1$
382	26 323 33 331	ltadd1dd	$⊢ φ \to 0 + 1 < {\log_{2} 4}^{5} + 1$
383	26 380 379 381 382	lttrd	$⊢ φ \to 0 < {\log_{2} 4}^{5} + 1$
384	319 327 379 383 37	relogbcld	$⊢ φ \to \log_{2} ({\log_{2} 4}^{5} + 1) \in ℝ$
385	384 373 311	lemuldiv2d	$⊢ φ \to (2 \log_{2} ({\log_{2} 4}^{5} + 1) \leq 12 \leftrightarrow \log_{2} ({\log_{2} 4}^{5} + 1) \leq \frac{12}{2})$
386	378 385	mpbird	$⊢ φ \to 2 \log_{2} ({\log_{2} 4}^{5} + 1) \leq 12$
387	315	oveq1d	$⊢ φ \to {\log_{2} 4}^{2} = 2^{2}$
388	387 307	eqtrdi	$⊢ φ \to {\log_{2} 4}^{2} = 4$
389	388	oveq2d	$⊢ φ \to 16 - {\log_{2} 4}^{2} = 16 - 4$
390		2nn0	$⊢ 2 \in ℕ_{0}$
391		eqid	$⊢ 12 = 12$
392		4cn	$⊢ 4 \in ℂ$
393		4p2e6	$⊢ 4 + 2 = 6$
394	392 349 393	addcomli	$⊢ 2 + 4 = 6$
395	193 390 174 391 394	decaddi	$⊢ 12 + 4 = 16$
396	392	a1i	$⊢ φ \to 4 \in ℂ$
397		6nn	$⊢ 6 \in ℕ$
398	193 397	decnncl	$⊢ 16 \in ℕ$
399	398	a1i	$⊢ φ \to 16 \in ℕ$
400	399	nnred	$⊢ φ \to 16 \in ℝ$
401	48 400	sselid	$⊢ φ \to 16 \in ℂ$
402	374 396 401	addlsub	$⊢ φ \to (12 + 4 = 16 \leftrightarrow 12 = 16 - 4)$
403	395 402	mpbii	$⊢ φ \to 12 = 16 - 4$
404	389 403	eqtr4d	$⊢ φ \to 16 - {\log_{2} 4}^{2} = 12$
405	404	eqcomd	$⊢ φ \to 12 = 16 - {\log_{2} 4}^{2}$
406	386 405	breqtrd	$⊢ φ \to 2 \log_{2} ({\log_{2} 4}^{5} + 1) \leq 16 - {\log_{2} 4}^{2}$
407	319 384	remulcld	$⊢ φ \to 2 \log_{2} ({\log_{2} 4}^{5} + 1) \in ℝ$
408	321	resqcld	$⊢ φ \to {\log_{2} 4}^{2} \in ℝ$
409		leaddsub	$⊢ (2 \log_{2} ({\log_{2} 4}^{5} + 1) \in ℝ \land {\log_{2} 4}^{2} \in ℝ \land 16 \in ℝ) \to (2 \log_{2} ({\log_{2} 4}^{5} + 1) + {\log_{2} 4}^{2} \leq 16 \leftrightarrow 2 \log_{2} ({\log_{2} 4}^{5} + 1) \leq 16 - {\log_{2} 4}^{2})$
410	407 408 400 409	syl3anc	$⊢ φ \to (2 \log_{2} ({\log_{2} 4}^{5} + 1) + {\log_{2} 4}^{2} \leq 16 \leftrightarrow 2 \log_{2} ({\log_{2} 4}^{5} + 1) \leq 16 - {\log_{2} 4}^{2})$
411	406 410	mpbird	$⊢ φ \to 2 \log_{2} ({\log_{2} 4}^{5} + 1) + {\log_{2} 4}^{2} \leq 16$
412	315	oveq1d	$⊢ φ \to {\log_{2} 4}^{4} = 2^{4}$
413		2exp4	$⊢ 2^{4} = 16$
414	412 413	eqtrdi	$⊢ φ \to {\log_{2} 4}^{4} = 16$
415	414	eqcomd	$⊢ φ \to 16 = {\log_{2} 4}^{4}$
416	411 415	breqtrd	$⊢ φ \to 2 \log_{2} ({\log_{2} 4}^{5} + 1) + {\log_{2} 4}^{2} \leq {\log_{2} 4}^{4}$
417	11 12 219 261 262 272 280 287 288 302 306 416 4	dvle2	$⊢ φ \to 2 C + D \leq E$
418	1 2 3 16 5 6 7 417	aks4d1p1p4	$⊢ φ \to A < 2^{B}$

Metamath Proof Explorer

Theorem aks4d1p1p5

Proof