Theorem aks4d1p1p7

Description: Bound of intermediary of inequality step. (Contributed by metakunt, 19-Aug-2024)

	Ref	Expression
Hypotheses	aks4d1p1p7.1	|- ( ph -> A e. RR )
	aks4d1p1p7.2	|- ( ph -> 4 <_ A )
Assertion	aks4d1p1p7	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb A ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ ( 2 - 1 ) ) / A ) ) ) <_ ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` A ) ^ 3 ) / A ) ) )

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1p7.1	|- ( ph -> A e. RR )
2		aks4d1p1p7.2	|- ( ph -> 4 <_ A )
3	1	recnd	|- ( ph -> A e. CC )
4		0red	|- ( ph -> 0 e. RR )
5		4re	|- 4 e. RR
6	5	a1i	|- ( ph -> 4 e. RR )
7		4pos	|- 0 < 4
8	7	a1i	|- ( ph -> 0 < 4 )
9	4 6 1 8 2	ltletrd	|- ( ph -> 0 < A )
10	4 9	ltned	|- ( ph -> 0 =/= A )
11	10	necomd	|- ( ph -> A =/= 0 )
12	3 11	logcld	|- ( ph -> ( log ` A ) e. CC )
13		2cnd	|- ( ph -> 2 e. CC )
14		2pos	|- 0 < 2
15	14	a1i	|- ( ph -> 0 < 2 )
16	4 15	ltned	|- ( ph -> 0 =/= 2 )
17	16	necomd	|- ( ph -> 2 =/= 0 )
18	13 17	logcld	|- ( ph -> ( log ` 2 ) e. CC )
19		1lt2	|- 1 < 2
20		2rp	|- 2 e. RR+
21		loggt0b	|- ( 2 e. RR+ -> ( 0 < ( log ` 2 ) <-> 1 < 2 ) )
22	20 21	ax-mp	|- ( 0 < ( log ` 2 ) <-> 1 < 2 )
23	19 22	mpbir	|- 0 < ( log ` 2 )
24	23	a1i	|- ( ph -> 0 < ( log ` 2 ) )
25	4 24	ltned	|- ( ph -> 0 =/= ( log ` 2 ) )
26	25	necomd	|- ( ph -> ( log ` 2 ) =/= 0 )
27		5nn0	|- 5 e. NN0
28	27	a1i	|- ( ph -> 5 e. NN0 )
29	12 18 26 28	expdivd	|- ( ph -> ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) = ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) )
30	29	oveq1d	|- ( ph -> ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) = ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) )
31	30	oveq1d	|- ( ph -> ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) = ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) )
32	31	oveq2d	|- ( ph -> ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) = ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) )
33	32	oveq1d	|- ( ph -> ( ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
34	33	oveq2d	|- ( ph -> ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) )
35	34	oveq1d	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) = ( ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) )
36		2re	|- 2 e. RR
37	36	a1i	|- ( ph -> 2 e. RR )
38		1red	|- ( ph -> 1 e. RR )
39	1 9	elrpd	|- ( ph -> A e. RR+ )
40	39	relogcld	|- ( ph -> ( log ` A ) e. RR )
41	40 28	reexpcld	|- ( ph -> ( ( log ` A ) ^ 5 ) e. RR )
42	20	a1i	|- ( ph -> 2 e. RR+ )
43	42	relogcld	|- ( ph -> ( log ` 2 ) e. RR )
44	43 28	reexpcld	|- ( ph -> ( ( log ` 2 ) ^ 5 ) e. RR )
45	28	nn0zd	|- ( ph -> 5 e. ZZ )
46	18 26 45	expne0d	|- ( ph -> ( ( log ` 2 ) ^ 5 ) =/= 0 )
47	41 44 46	redivcld	|- ( ph -> ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) e. RR )
48	47 38	readdcld	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) e. RR )
49	48 43	remulcld	|- ( ph -> ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) e. RR )
50	12 28	expcld	|- ( ph -> ( ( log ` A ) ^ 5 ) e. CC )
51	18 28	expcld	|- ( ph -> ( ( log ` 2 ) ^ 5 ) e. CC )
52	50 51 46	divcld	|- ( ph -> ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) e. CC )
53		1cnd	|- ( ph -> 1 e. CC )
54	52 53	addcld	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) e. CC )
55	19	a1i	|- ( ph -> 1 < 2 )
56	37 55	rplogcld	|- ( ph -> ( log ` 2 ) e. RR+ )
57	56 45	rpexpcld	|- ( ph -> ( ( log ` 2 ) ^ 5 ) e. RR+ )
58		1re	|- 1 e. RR
59		3nn0	|- 3 e. NN0
60	58 59	nn0addge2i	|- 1 <_ ( 3 + 1 )
61	60	a1i	|- ( ph -> 1 <_ ( 3 + 1 ) )
62		df-4	|- 4 = ( 3 + 1 )
63	61 62	breqtrrdi	|- ( ph -> 1 <_ 4 )
64	38 6 1 63 2	letrd	|- ( ph -> 1 <_ A )
65	1 64	logge0d	|- ( ph -> 0 <_ ( log ` A ) )
66	40 28 65	expge0d	|- ( ph -> 0 <_ ( ( log ` A ) ^ 5 ) )
67	41 57 66	divge0d	|- ( ph -> 0 <_ ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) )
68	47	ltp1d	|- ( ph -> ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) < ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) )
69	4 47 48 67 68	lelttrd	|- ( ph -> 0 < ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) )
70	4 69	ltned	|- ( ph -> 0 =/= ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) )
71	70	necomd	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) =/= 0 )
72	54 18 71 26	mulne0d	|- ( ph -> ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) =/= 0 )
73	38 49 72	redivcld	|- ( ph -> ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) e. RR )
74		5re	|- 5 e. RR
75	74	a1i	|- ( ph -> 5 e. RR )
76		4nn0	|- 4 e. NN0
77	76	a1i	|- ( ph -> 4 e. NN0 )
78	40 77	reexpcld	|- ( ph -> ( ( log ` A ) ^ 4 ) e. RR )
79	75 78	remulcld	|- ( ph -> ( 5 x. ( ( log ` A ) ^ 4 ) ) e. RR )
80	44 1	remulcld	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) e. RR )
81	51 3 46 11	mulne0d	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) =/= 0 )
82	79 80 81	redivcld	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) e. RR )
83	73 82	remulcld	|- ( ph -> ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) e. RR )
84	37 83	remulcld	|- ( ph -> ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) e. RR )
85	43	resqcld	|- ( ph -> ( ( log ` 2 ) ^ 2 ) e. RR )
86		2z	|- 2 e. ZZ
87	86	a1i	|- ( ph -> 2 e. ZZ )
88	18 26 87	expne0d	|- ( ph -> ( ( log ` 2 ) ^ 2 ) =/= 0 )
89	37 85 88	redivcld	|- ( ph -> ( 2 / ( ( log ` 2 ) ^ 2 ) ) e. RR )
90		1nn0	|- 1 e. NN0
91	90	a1i	|- ( ph -> 1 e. NN0 )
92	40 91	reexpcld	|- ( ph -> ( ( log ` A ) ^ 1 ) e. RR )
93	92 1 11	redivcld	|- ( ph -> ( ( ( log ` A ) ^ 1 ) / A ) e. RR )
94	89 93	remulcld	|- ( ph -> ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) e. RR )
95	84 94	readdcld	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) e. RR )
96	47 43	remulcld	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) e. RR )
97		1lt4	|- 1 < 4
98	97	a1i	|- ( ph -> 1 < 4 )
99	38 6 1 98 2	ltletrd	|- ( ph -> 1 < A )
100		loggt0b	|- ( A e. RR+ -> ( 0 < ( log ` A ) <-> 1 < A ) )
101	39 100	syl	|- ( ph -> ( 0 < ( log ` A ) <-> 1 < A ) )
102	99 101	mpbird	|- ( ph -> 0 < ( log ` A ) )
103	4 102	ltned	|- ( ph -> 0 =/= ( log ` A ) )
104	103	necomd	|- ( ph -> ( log ` A ) =/= 0 )
105	12 104 45	expne0d	|- ( ph -> ( ( log ` A ) ^ 5 ) =/= 0 )
106	50 51 105 46	divne0d	|- ( ph -> ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) =/= 0 )
107	52 18 106 26	mulne0d	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) =/= 0 )
108	38 96 107	redivcld	|- ( ph -> ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) e. RR )
109	108 82	remulcld	|- ( ph -> ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) e. RR )
110	37 109	remulcld	|- ( ph -> ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) e. RR )
111	110 94	readdcld	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) e. RR )
112	59	a1i	|- ( ph -> 3 e. NN0 )
113	40 112	reexpcld	|- ( ph -> ( ( log ` A ) ^ 3 ) e. RR )
114	6 113	remulcld	|- ( ph -> ( 4 x. ( ( log ` A ) ^ 3 ) ) e. RR )
115	43 77	reexpcld	|- ( ph -> ( ( log ` 2 ) ^ 4 ) e. RR )
116	115 1	remulcld	|- ( ph -> ( ( ( log ` 2 ) ^ 4 ) x. A ) e. RR )
117	18 77	expcld	|- ( ph -> ( ( log ` 2 ) ^ 4 ) e. CC )
118		4z	|- 4 e. ZZ
119	118	a1i	|- ( ph -> 4 e. ZZ )
120	18 26 119	expne0d	|- ( ph -> ( ( log ` 2 ) ^ 4 ) =/= 0 )
121	117 3 120 11	mulne0d	|- ( ph -> ( ( ( log ` 2 ) ^ 4 ) x. A ) =/= 0 )
122	114 116 121	redivcld	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) e. RR )
123		0le2	|- 0 <_ 2
124	123	a1i	|- ( ph -> 0 <_ 2 )
125	57 39	rpmulcld	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) e. RR+ )
126	28	nn0ge0d	|- ( ph -> 0 <_ 5 )
127	40 77 65	expge0d	|- ( ph -> 0 <_ ( ( log ` A ) ^ 4 ) )
128	75 78 126 127	mulge0d	|- ( ph -> 0 <_ ( 5 x. ( ( log ` A ) ^ 4 ) ) )
129	79 125 128	divge0d	|- ( ph -> 0 <_ ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) )
130	1 99	rplogcld	|- ( ph -> ( log ` A ) e. RR+ )
131	130 45	rpexpcld	|- ( ph -> ( ( log ` A ) ^ 5 ) e. RR+ )
132	131 57	rpdivcld	|- ( ph -> ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) e. RR+ )
133	132 56	rpmulcld	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) e. RR+ )
134	24 22	sylib	|- ( ph -> 1 < 2 )
135	37 134	rplogcld	|- ( ph -> ( log ` 2 ) e. RR+ )
136	135 45	rpexpcld	|- ( ph -> ( ( log ` 2 ) ^ 5 ) e. RR+ )
137	41 136 66	divge0d	|- ( ph -> 0 <_ ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) )
138	47 137	ge0p1rpd	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) e. RR+ )
139	138 135	rpmulcld	|- ( ph -> ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) e. RR+ )
140		0le1	|- 0 <_ 1
141	140	a1i	|- ( ph -> 0 <_ 1 )
142	135	rpred	|- ( ph -> ( log ` 2 ) e. RR )
143	135	rpge0d	|- ( ph -> 0 <_ ( log ` 2 ) )
144	47	lep1d	|- ( ph -> ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) <_ ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) )
145	47 48 142 143 144	lemul1ad	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) <_ ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) )
146	133 139 38 141 145	lediv2ad	|- ( ph -> ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) <_ ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) )
147	73 108 82 129 146	lemul1ad	|- ( ph -> ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) <_ ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
148	83 109 37 124 147	lemul2ad	|- ( ph -> ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) <_ ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) )
149	84 110 94 148	leadd1dd	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) <_ ( ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) )
150	50 18 51 46	div23d	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) = ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) )
151	150	eqcomd	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) = ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) )
152	151	oveq2d	|- ( ph -> ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) = ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) )
153	152	oveq1d	|- ( ph -> ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
154	153	oveq2d	|- ( ph -> ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) )
155	18	sqcld	|- ( ph -> ( ( log ` 2 ) ^ 2 ) e. CC )
156	12 91	expcld	|- ( ph -> ( ( log ` A ) ^ 1 ) e. CC )
157	13 155 156 3 88 11	divmuldivd	|- ( ph -> ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) )
158	154 157	oveq12d	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) = ( ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
159	50 18	mulcld	|- ( ph -> ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) e. CC )
160	50 18 105 26	mulne0d	|- ( ph -> ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) =/= 0 )
161	53 159 51 160 46	divdiv2d	|- ( ph -> ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) = ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) )
162	161	oveq1d	|- ( ph -> ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
163	162	oveq2d	|- ( ph -> ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( 2 x. ( ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) )
164	53 51	mulcld	|- ( ph -> ( 1 x. ( ( log ` 2 ) ^ 5 ) ) e. CC )
165	164 159 160	divcld	|- ( ph -> ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) e. CC )
166	82	recnd	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) e. CC )
167	13 165 166	mulassd	|- ( ph -> ( ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( 2 x. ( ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) )
168	167	eqcomd	|- ( ph -> ( 2 x. ( ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
169	163 168	eqtrd	|- ( ph -> ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
170	169	oveq1d	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
171	13 164 159 160	divassd	|- ( ph -> ( ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) = ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) )
172	171	eqcomd	|- ( ph -> ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) = ( ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) )
173	172	oveq1d	|- ( ph -> ( ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
174	173	oveq1d	|- ( ph -> ( ( ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
175	13 53 51	mulassd	|- ( ph -> ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) = ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) )
176	175	eqcomd	|- ( ph -> ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) = ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) )
177	176	oveq1d	|- ( ph -> ( ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) = ( ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) )
178	177	oveq1d	|- ( ph -> ( ( ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
179	178	oveq1d	|- ( ph -> ( ( ( ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
180	13	mulid1d	|- ( ph -> ( 2 x. 1 ) = 2 )
181	180	oveq1d	|- ( ph -> ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) = ( 2 x. ( ( log ` 2 ) ^ 5 ) ) )
182	181	oveq1d	|- ( ph -> ( ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) = ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) )
183	182	oveq1d	|- ( ph -> ( ( ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
184	183	oveq1d	|- ( ph -> ( ( ( ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
185	13 51	mulcld	|- ( ph -> ( 2 x. ( ( log ` 2 ) ^ 5 ) ) e. CC )
186	79	recnd	|- ( ph -> ( 5 x. ( ( log ` A ) ^ 4 ) ) e. CC )
187	51 3	mulcld	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) e. CC )
188	185 159 186 187 160 81	divmuldivd	|- ( ph -> ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
189	188	oveq1d	|- ( ph -> ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
190	50 18 187	mulassd	|- ( ph -> ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( ( log ` A ) ^ 5 ) x. ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
191	190	oveq2d	|- ( ph -> ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) )
192	191	oveq1d	|- ( ph -> ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
193	185 186	mulcomd	|- ( ph -> ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) = ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. ( 2 x. ( ( log ` 2 ) ^ 5 ) ) ) )
194	18 51 3	mulassd	|- ( ph -> ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) = ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) )
195	194	eqcomd	|- ( ph -> ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) )
196	195	oveq2d	|- ( ph -> ( ( ( log ` A ) ^ 5 ) x. ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( ( log ` A ) ^ 5 ) x. ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) )
197	193 196	oveq12d	|- ( ph -> ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. ( 2 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) )
198	197	oveq1d	|- ( ph -> ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. ( 2 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
199	18 51	mulcld	|- ( ph -> ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) e. CC )
200	199 3	mulcld	|- ( ph -> ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) e. CC )
201	18 51 26 46	mulne0d	|- ( ph -> ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) =/= 0 )
202	199 3 201 11	mulne0d	|- ( ph -> ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) =/= 0 )
203	186 50 185 200 105 202	divmuldivd	|- ( ph -> ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` A ) ^ 5 ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) = ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. ( 2 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) )
204	203	eqcomd	|- ( ph -> ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. ( 2 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) = ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` A ) ^ 5 ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) )
205	204	oveq1d	|- ( ph -> ( ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. ( 2 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` A ) ^ 5 ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
206	75	recnd	|- ( ph -> 5 e. CC )
207	78	recnd	|- ( ph -> ( ( log ` A ) ^ 4 ) e. CC )
208	206 207 50 105	divassd	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` A ) ^ 5 ) ) = ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) ) )
209	194	oveq2d	|- ( ph -> ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) = ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
210	208 209	oveq12d	|- ( ph -> ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` A ) ^ 5 ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) = ( ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) )
211	210	oveq1d	|- ( ph -> ( ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` A ) ^ 5 ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
212	77	nn0zd	|- ( ph -> 4 e. ZZ )
213	12 104 45 212	expsubd	|- ( ph -> ( ( log ` A ) ^ ( 4 - 5 ) ) = ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) )
214	213	eqcomd	|- ( ph -> ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) = ( ( log ` A ) ^ ( 4 - 5 ) ) )
215		4p1e5	|- ( 4 + 1 ) = 5
216	74	recni	|- 5 e. CC
217	5	recni	|- 4 e. CC
218		ax-1cn	|- 1 e. CC
219	216 217 218	subaddi	|- ( ( 5 - 4 ) = 1 <-> ( 4 + 1 ) = 5 )
220	215 219	mpbir	|- ( 5 - 4 ) = 1
221	220	a1i	|- ( ph -> ( 5 - 4 ) = 1 )
222	53	subid1d	|- ( ph -> ( 1 - 0 ) = 1 )
223	221 222	eqtr4d	|- ( ph -> ( 5 - 4 ) = ( 1 - 0 ) )
224	206 217	jctir	|- ( ph -> ( 5 e. CC /\ 4 e. CC ) )
225		0cnd	|- ( ph -> 0 e. CC )
226	53 225	jca	|- ( ph -> ( 1 e. CC /\ 0 e. CC ) )
227		subeqrev	|- ( ( ( 5 e. CC /\ 4 e. CC ) /\ ( 1 e. CC /\ 0 e. CC ) ) -> ( ( 5 - 4 ) = ( 1 - 0 ) <-> ( 4 - 5 ) = ( 0 - 1 ) ) )
228	224 226 227	syl2anc	|- ( ph -> ( ( 5 - 4 ) = ( 1 - 0 ) <-> ( 4 - 5 ) = ( 0 - 1 ) ) )
229	223 228	mpbid	|- ( ph -> ( 4 - 5 ) = ( 0 - 1 ) )
230		df-neg	|- -u 1 = ( 0 - 1 )
231	229 230	eqtr4di	|- ( ph -> ( 4 - 5 ) = -u 1 )
232	231	oveq2d	|- ( ph -> ( ( log ` A ) ^ ( 4 - 5 ) ) = ( ( log ` A ) ^ -u 1 ) )
233	214 232	eqtrd	|- ( ph -> ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) = ( ( log ` A ) ^ -u 1 ) )
234	233	oveq2d	|- ( ph -> ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) ) = ( 5 x. ( ( log ` A ) ^ -u 1 ) ) )
235	13 18 51 187 26 81	divmuldivd	|- ( ph -> ( ( 2 / ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
236	235	eqcomd	|- ( ph -> ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( 2 / ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) )
237	234 236	oveq12d	|- ( ph -> ( ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( ( 5 x. ( ( log ` A ) ^ -u 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) )
238	237	oveq1d	|- ( ph -> ( ( ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( 5 x. ( ( log ` A ) ^ -u 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
239		1zzd	|- ( ph -> 1 e. ZZ )
240	12 104 239	expnegd	|- ( ph -> ( ( log ` A ) ^ -u 1 ) = ( 1 / ( ( log ` A ) ^ 1 ) ) )
241	240	oveq2d	|- ( ph -> ( 5 x. ( ( log ` A ) ^ -u 1 ) ) = ( 5 x. ( 1 / ( ( log ` A ) ^ 1 ) ) ) )
242	51 51 3 46 11	divdiv1d	|- ( ph -> ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) = ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) )
243	242	eqcomd	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) )
244	243	oveq2d	|- ( ph -> ( ( 2 / ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( 2 / ( log ` 2 ) ) x. ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) ) )
245	241 244	oveq12d	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ -u 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( ( 5 x. ( 1 / ( ( log ` A ) ^ 1 ) ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) ) ) )
246	245	oveq1d	|- ( ph -> ( ( ( 5 x. ( ( log ` A ) ^ -u 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( 5 x. ( 1 / ( ( log ` A ) ^ 1 ) ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
247	12 104 239	expne0d	|- ( ph -> ( ( log ` A ) ^ 1 ) =/= 0 )
248	206 53 156 247	divassd	|- ( ph -> ( ( 5 x. 1 ) / ( ( log ` A ) ^ 1 ) ) = ( 5 x. ( 1 / ( ( log ` A ) ^ 1 ) ) ) )
249	248	eqcomd	|- ( ph -> ( 5 x. ( 1 / ( ( log ` A ) ^ 1 ) ) ) = ( ( 5 x. 1 ) / ( ( log ` A ) ^ 1 ) ) )
250	51 46	dividd	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) = 1 )
251	250	oveq1d	|- ( ph -> ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) = ( 1 / A ) )
252	251	oveq2d	|- ( ph -> ( ( 2 / ( log ` 2 ) ) x. ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) ) = ( ( 2 / ( log ` 2 ) ) x. ( 1 / A ) ) )
253	249 252	oveq12d	|- ( ph -> ( ( 5 x. ( 1 / ( ( log ` A ) ^ 1 ) ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) ) ) = ( ( ( 5 x. 1 ) / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( 1 / A ) ) ) )
254	253	oveq1d	|- ( ph -> ( ( ( 5 x. ( 1 / ( ( log ` A ) ^ 1 ) ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( ( 5 x. 1 ) / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( 1 / A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
255	206	mulid1d	|- ( ph -> ( 5 x. 1 ) = 5 )
256	255	oveq1d	|- ( ph -> ( ( 5 x. 1 ) / ( ( log ` A ) ^ 1 ) ) = ( 5 / ( ( log ` A ) ^ 1 ) ) )
257	13 18 53 3 26 11	divmuldivd	|- ( ph -> ( ( 2 / ( log ` 2 ) ) x. ( 1 / A ) ) = ( ( 2 x. 1 ) / ( ( log ` 2 ) x. A ) ) )
258	256 257	oveq12d	|- ( ph -> ( ( ( 5 x. 1 ) / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( 1 / A ) ) ) = ( ( 5 / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 x. 1 ) / ( ( log ` 2 ) x. A ) ) ) )
259	258	oveq1d	|- ( ph -> ( ( ( ( 5 x. 1 ) / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( 1 / A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( 5 / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 x. 1 ) / ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
260	180 13	eqeltrd	|- ( ph -> ( 2 x. 1 ) e. CC )
261	18 3	mulcld	|- ( ph -> ( ( log ` 2 ) x. A ) e. CC )
262	18 3 26 11	mulne0d	|- ( ph -> ( ( log ` 2 ) x. A ) =/= 0 )
263	206 156 260 261 247 262	divmuldivd	|- ( ph -> ( ( 5 / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 x. 1 ) / ( ( log ` 2 ) x. A ) ) ) = ( ( 5 x. ( 2 x. 1 ) ) / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) )
264	180	oveq2d	|- ( ph -> ( 5 x. ( 2 x. 1 ) ) = ( 5 x. 2 ) )
265	264	oveq1d	|- ( ph -> ( ( 5 x. ( 2 x. 1 ) ) / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) = ( ( 5 x. 2 ) / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) )
266	263 265	eqtrd	|- ( ph -> ( ( 5 / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 x. 1 ) / ( ( log ` 2 ) x. A ) ) ) = ( ( 5 x. 2 ) / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) )
267	266	oveq1d	|- ( ph -> ( ( ( 5 / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 x. 1 ) / ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( 5 x. 2 ) / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
268		5t2e10	|- ( 5 x. 2 ) = ; 1 0
269	268	a1i	|- ( ph -> ( 5 x. 2 ) = ; 1 0 )
270	269	oveq1d	|- ( ph -> ( ( 5 x. 2 ) / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) = ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) )
271	270	oveq1d	|- ( ph -> ( ( ( 5 x. 2 ) / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
272		10nn0	|- ; 1 0 e. NN0
273	272	nn0cni	|- ; 1 0 e. CC
274	273	a1i	|- ( ph -> ; 1 0 e. CC )
275	274	mulid1d	|- ( ph -> ( ; 1 0 x. 1 ) = ; 1 0 )
276	275	oveq1d	|- ( ph -> ( ( ; 1 0 x. 1 ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) = ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) )
277	13 156	mulcld	|- ( ph -> ( 2 x. ( ( log ` A ) ^ 1 ) ) e. CC )
278	277 155 88	divcld	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) e. CC )
279	278	mulid2d	|- ( ph -> ( 1 x. ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) )
280	276 279	oveq12d	|- ( ph -> ( ( ( ; 1 0 x. 1 ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( 1 x. ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) ) = ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) )
281	18 91	expcld	|- ( ph -> ( ( log ` 2 ) ^ 1 ) e. CC )
282	18 26 239	expne0d	|- ( ph -> ( ( log ` 2 ) ^ 1 ) =/= 0 )
283	277 281 282	divcld	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) e. CC )
284	283	mulid1d	|- ( ph -> ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) x. 1 ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) )
285	284	oveq2d	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) x. 1 ) ) = ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) ) )
286		10re	|- ; 1 0 e. RR
287	286	a1i	|- ( ph -> ; 1 0 e. RR )
288	287 40 104	redivcld	|- ( ph -> ( ; 1 0 / ( log ` A ) ) e. RR )
289	40 43 26	redivcld	|- ( ph -> ( ( log ` A ) / ( log ` 2 ) ) e. RR )
290	289 91	reexpcld	|- ( ph -> ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) e. RR )
291	37 290	remulcld	|- ( ph -> ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) e. RR )
292	288 291	readdcld	|- ( ph -> ( ( ; 1 0 / ( log ` A ) ) + ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) ) e. RR )
293	287 291	readdcld	|- ( ph -> ( ; 1 0 + ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) ) e. RR )
294	43 112	reexpcld	|- ( ph -> ( ( log ` 2 ) ^ 3 ) e. RR )
295		3z	|- 3 e. ZZ
296	295	a1i	|- ( ph -> 3 e. ZZ )
297	18 26 296	expne0d	|- ( ph -> ( ( log ` 2 ) ^ 3 ) =/= 0 )
298	113 294 297	redivcld	|- ( ph -> ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) e. RR )
299	6 298	remulcld	|- ( ph -> ( 4 x. ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) ) e. RR )
300		ere	|- _e e. RR
301	300	a1i	|- ( ph -> _e e. RR )
302	112	nn0red	|- ( ph -> 3 e. RR )
303		egt2lt3	|- ( 2 < _e /\ _e < 3 )
304	303	simpri	|- _e < 3
305	304	a1i	|- ( ph -> _e < 3 )
306		3lt4	|- 3 < 4
307	306	a1i	|- ( ph -> 3 < 4 )
308	302 6 1 307 2	ltletrd	|- ( ph -> 3 < A )
309	301 302 1 305 308	lttrd	|- ( ph -> _e < A )
310	301 1 309	ltled	|- ( ph -> _e <_ A )
311	301 1	lenltd	|- ( ph -> ( _e <_ A <-> -. A < _e ) )
312	310 311	mpbid	|- ( ph -> -. A < _e )
313		loglt1b	|- ( A e. RR+ -> ( ( log ` A ) < 1 <-> A < _e ) )
314	39 313	syl	|- ( ph -> ( ( log ` A ) < 1 <-> A < _e ) )
315	312 314	mtbird	|- ( ph -> -. ( log ` A ) < 1 )
316	38 40	lenltd	|- ( ph -> ( 1 <_ ( log ` A ) <-> -. ( log ` A ) < 1 ) )
317	315 316	mpbird	|- ( ph -> 1 <_ ( log ` A ) )
318		10nn	|- ; 1 0 e. NN
319	318	a1i	|- ( ph -> ; 1 0 e. NN )
320		nnledivrp	|- ( ( ; 1 0 e. NN /\ ( log ` A ) e. RR+ ) -> ( 1 <_ ( log ` A ) <-> ( ; 1 0 / ( log ` A ) ) <_ ; 1 0 ) )
321	319 130 320	syl2anc	|- ( ph -> ( 1 <_ ( log ` A ) <-> ( ; 1 0 / ( log ` A ) ) <_ ; 1 0 ) )
322	317 321	mpbid	|- ( ph -> ( ; 1 0 / ( log ` A ) ) <_ ; 1 0 )
323	288 287 291 322	leadd1dd	|- ( ph -> ( ( ; 1 0 / ( log ` A ) ) + ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) ) <_ ( ; 1 0 + ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) ) )
324	38 55	gtned	|- ( ph -> 2 =/= 1 )
325	37 15 1 9 324	relogbcld	|- ( ph -> ( 2 logb A ) e. RR )
326	325 91	reexpcld	|- ( ph -> ( ( 2 logb A ) ^ 1 ) e. RR )
327	42 55	jca	|- ( ph -> ( 2 e. RR+ /\ 1 < 2 ) )
328		logbgt0b	|- ( ( A e. RR+ /\ ( 2 e. RR+ /\ 1 < 2 ) ) -> ( 0 < ( 2 logb A ) <-> 1 < A ) )
329	39 327 328	syl2anc	|- ( ph -> ( 0 < ( 2 logb A ) <-> 1 < A ) )
330	99 329	mpbird	|- ( ph -> 0 < ( 2 logb A ) )
331	325 330	elrpd	|- ( ph -> ( 2 logb A ) e. RR+ )
332	331 239	rpexpcld	|- ( ph -> ( ( 2 logb A ) ^ 1 ) e. RR+ )
333	332	rpne0d	|- ( ph -> ( ( 2 logb A ) ^ 1 ) =/= 0 )
334	287 326 333	redivcld	|- ( ph -> ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) e. RR )
335	334 37	readdcld	|- ( ph -> ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + 2 ) e. RR )
336		sq2	|- ( 2 ^ 2 ) = 4
337	336	a1i	|- ( ph -> ( 2 ^ 2 ) = 4 )
338	337 6	eqeltrd	|- ( ph -> ( 2 ^ 2 ) e. RR )
339	6 338	remulcld	|- ( ph -> ( 4 x. ( 2 ^ 2 ) ) e. RR )
340	325	resqcld	|- ( ph -> ( ( 2 logb A ) ^ 2 ) e. RR )
341	6 340	remulcld	|- ( ph -> ( 4 x. ( ( 2 logb A ) ^ 2 ) ) e. RR )
342	325	recnd	|- ( ph -> ( 2 logb A ) e. CC )
343	342	exp1d	|- ( ph -> ( ( 2 logb A ) ^ 1 ) = ( 2 logb A ) )
344	343	oveq2d	|- ( ph -> ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) = ( ; 1 0 / ( 2 logb A ) ) )
345	344	oveq1d	|- ( ph -> ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + 2 ) = ( ( ; 1 0 / ( 2 logb A ) ) + 2 ) )
346	345 335	eqeltrrd	|- ( ph -> ( ( ; 1 0 / ( 2 logb A ) ) + 2 ) e. RR )
347	287	rehalfcld	|- ( ph -> ( ; 1 0 / 2 ) e. RR )
348	347 37	readdcld	|- ( ph -> ( ( ; 1 0 / 2 ) + 2 ) e. RR )
349	344 334	eqeltrrd	|- ( ph -> ( ; 1 0 / ( 2 logb A ) ) e. RR )
350	287 37 17	redivcld	|- ( ph -> ( ; 1 0 / 2 ) e. RR )
351	272	nn0ge0i	|- 0 <_ ; 1 0
352	351	a1i	|- ( ph -> 0 <_ ; 1 0 )
353	42 324 87	relogbexpd	|- ( ph -> ( 2 logb ( 2 ^ 2 ) ) = 2 )
354	353	eqcomd	|- ( ph -> 2 = ( 2 logb ( 2 ^ 2 ) ) )
355	337	oveq2d	|- ( ph -> ( 2 logb ( 2 ^ 2 ) ) = ( 2 logb 4 ) )
356	354 355	eqtrd	|- ( ph -> 2 = ( 2 logb 4 ) )
357	37	leidd	|- ( ph -> 2 <_ 2 )
358	87 357 6 8 1 9 2	logblebd	|- ( ph -> ( 2 logb 4 ) <_ ( 2 logb A ) )
359	356 358	eqbrtrd	|- ( ph -> 2 <_ ( 2 logb A ) )
360	42 331 287 352 359	lediv2ad	|- ( ph -> ( ; 1 0 / ( 2 logb A ) ) <_ ( ; 1 0 / 2 ) )
361	349 350 37 360	leadd1dd	|- ( ph -> ( ( ; 1 0 / ( 2 logb A ) ) + 2 ) <_ ( ( ; 1 0 / 2 ) + 2 ) )
362		1nn	|- 1 e. NN
363		6nn0	|- 6 e. NN0
364		2nn0	|- 2 e. NN0
365	27 364	nn0addcli	|- ( 5 + 2 ) e. NN0
366		5p2e7	|- ( 5 + 2 ) = 7
367		7re	|- 7 e. RR
368	367 364	nn0addge1i	|- 7 <_ ( 7 + 2 )
369		7p2e9	|- ( 7 + 2 ) = 9
370	368 369	breqtri	|- 7 <_ 9
371	366 370	eqbrtri	|- ( 5 + 2 ) <_ 9
372	362 363 365 371	declei	|- ( 5 + 2 ) <_ ; 1 6
373	372	a1i	|- ( ph -> ( 5 + 2 ) <_ ; 1 6 )
374	206 13 274 17	ldiv	|- ( ph -> ( ( 5 x. 2 ) = ; 1 0 <-> 5 = ( ; 1 0 / 2 ) ) )
375	269 374	mpbid	|- ( ph -> 5 = ( ; 1 0 / 2 ) )
376	375	oveq1d	|- ( ph -> ( 5 + 2 ) = ( ( ; 1 0 / 2 ) + 2 ) )
377		4t4e16	|- ( 4 x. 4 ) = ; 1 6
378	377	eqcomi	|- ; 1 6 = ( 4 x. 4 )
379	378	a1i	|- ( ph -> ; 1 6 = ( 4 x. 4 ) )
380	337	eqcomd	|- ( ph -> 4 = ( 2 ^ 2 ) )
381	380	oveq2d	|- ( ph -> ( 4 x. 4 ) = ( 4 x. ( 2 ^ 2 ) ) )
382	379 381	eqtrd	|- ( ph -> ; 1 6 = ( 4 x. ( 2 ^ 2 ) ) )
383	373 376 382	3brtr3d	|- ( ph -> ( ( ; 1 0 / 2 ) + 2 ) <_ ( 4 x. ( 2 ^ 2 ) ) )
384	346 348 339 361 383	letrd	|- ( ph -> ( ( ; 1 0 / ( 2 logb A ) ) + 2 ) <_ ( 4 x. ( 2 ^ 2 ) ) )
385	345 384	eqbrtrd	|- ( ph -> ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + 2 ) <_ ( 4 x. ( 2 ^ 2 ) ) )
386	4 6 8	ltled	|- ( ph -> 0 <_ 4 )
387	364	a1i	|- ( ph -> 2 e. NN0 )
388	37 325 387 124 359	leexp1ad	|- ( ph -> ( 2 ^ 2 ) <_ ( ( 2 logb A ) ^ 2 ) )
389	338 340 6 386 388	lemul2ad	|- ( ph -> ( 4 x. ( 2 ^ 2 ) ) <_ ( 4 x. ( ( 2 logb A ) ^ 2 ) ) )
390	335 339 341 385 389	letrd	|- ( ph -> ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + 2 ) <_ ( 4 x. ( ( 2 logb A ) ^ 2 ) ) )
391	37 326	remulcld	|- ( ph -> ( 2 x. ( ( 2 logb A ) ^ 1 ) ) e. RR )
392	391	recnd	|- ( ph -> ( 2 x. ( ( 2 logb A ) ^ 1 ) ) e. CC )
393	326	recnd	|- ( ph -> ( ( 2 logb A ) ^ 1 ) e. CC )
394	274 392 393 333	divdird	|- ( ph -> ( ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) / ( ( 2 logb A ) ^ 1 ) ) = ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + ( ( 2 x. ( ( 2 logb A ) ^ 1 ) ) / ( ( 2 logb A ) ^ 1 ) ) ) )
395	13 393 393 333	divassd	|- ( ph -> ( ( 2 x. ( ( 2 logb A ) ^ 1 ) ) / ( ( 2 logb A ) ^ 1 ) ) = ( 2 x. ( ( ( 2 logb A ) ^ 1 ) / ( ( 2 logb A ) ^ 1 ) ) ) )
396	395	oveq2d	|- ( ph -> ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + ( ( 2 x. ( ( 2 logb A ) ^ 1 ) ) / ( ( 2 logb A ) ^ 1 ) ) ) = ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + ( 2 x. ( ( ( 2 logb A ) ^ 1 ) / ( ( 2 logb A ) ^ 1 ) ) ) ) )
397	393 333	dividd	|- ( ph -> ( ( ( 2 logb A ) ^ 1 ) / ( ( 2 logb A ) ^ 1 ) ) = 1 )
398	397	oveq2d	|- ( ph -> ( 2 x. ( ( ( 2 logb A ) ^ 1 ) / ( ( 2 logb A ) ^ 1 ) ) ) = ( 2 x. 1 ) )
399	398 180	eqtrd	|- ( ph -> ( 2 x. ( ( ( 2 logb A ) ^ 1 ) / ( ( 2 logb A ) ^ 1 ) ) ) = 2 )
400	399	oveq2d	|- ( ph -> ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + ( 2 x. ( ( ( 2 logb A ) ^ 1 ) / ( ( 2 logb A ) ^ 1 ) ) ) ) = ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + 2 ) )
401	396 400	eqtrd	|- ( ph -> ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + ( ( 2 x. ( ( 2 logb A ) ^ 1 ) ) / ( ( 2 logb A ) ^ 1 ) ) ) = ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + 2 ) )
402	394 401	eqtrd	|- ( ph -> ( ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) / ( ( 2 logb A ) ^ 1 ) ) = ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + 2 ) )
403	402	eqcomd	|- ( ph -> ( ( ; 1 0 / ( ( 2 logb A ) ^ 1 ) ) + 2 ) = ( ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) / ( ( 2 logb A ) ^ 1 ) ) )
404		2p1e3	|- ( 2 + 1 ) = 3
405	404	a1i	|- ( ph -> ( 2 + 1 ) = 3 )
406	302	recnd	|- ( ph -> 3 e. CC )
407	406 53 13	subadd2d	|- ( ph -> ( ( 3 - 1 ) = 2 <-> ( 2 + 1 ) = 3 ) )
408	405 407	mpbird	|- ( ph -> ( 3 - 1 ) = 2 )
409	408	eqcomd	|- ( ph -> 2 = ( 3 - 1 ) )
410	409	oveq2d	|- ( ph -> ( ( 2 logb A ) ^ 2 ) = ( ( 2 logb A ) ^ ( 3 - 1 ) ) )
411	410	oveq2d	|- ( ph -> ( 4 x. ( ( 2 logb A ) ^ 2 ) ) = ( 4 x. ( ( 2 logb A ) ^ ( 3 - 1 ) ) ) )
412	4 330	gtned	|- ( ph -> ( 2 logb A ) =/= 0 )
413	342 412 239 296	expsubd	|- ( ph -> ( ( 2 logb A ) ^ ( 3 - 1 ) ) = ( ( ( 2 logb A ) ^ 3 ) / ( ( 2 logb A ) ^ 1 ) ) )
414	413	oveq2d	|- ( ph -> ( 4 x. ( ( 2 logb A ) ^ ( 3 - 1 ) ) ) = ( 4 x. ( ( ( 2 logb A ) ^ 3 ) / ( ( 2 logb A ) ^ 1 ) ) ) )
415	411 414	eqtrd	|- ( ph -> ( 4 x. ( ( 2 logb A ) ^ 2 ) ) = ( 4 x. ( ( ( 2 logb A ) ^ 3 ) / ( ( 2 logb A ) ^ 1 ) ) ) )
416	217	a1i	|- ( ph -> 4 e. CC )
417	325 112	reexpcld	|- ( ph -> ( ( 2 logb A ) ^ 3 ) e. RR )
418	417	recnd	|- ( ph -> ( ( 2 logb A ) ^ 3 ) e. CC )
419	416 418 393 333	divassd	|- ( ph -> ( ( 4 x. ( ( 2 logb A ) ^ 3 ) ) / ( ( 2 logb A ) ^ 1 ) ) = ( 4 x. ( ( ( 2 logb A ) ^ 3 ) / ( ( 2 logb A ) ^ 1 ) ) ) )
420	419	eqcomd	|- ( ph -> ( 4 x. ( ( ( 2 logb A ) ^ 3 ) / ( ( 2 logb A ) ^ 1 ) ) ) = ( ( 4 x. ( ( 2 logb A ) ^ 3 ) ) / ( ( 2 logb A ) ^ 1 ) ) )
421	415 420	eqtrd	|- ( ph -> ( 4 x. ( ( 2 logb A ) ^ 2 ) ) = ( ( 4 x. ( ( 2 logb A ) ^ 3 ) ) / ( ( 2 logb A ) ^ 1 ) ) )
422	390 403 421	3brtr3d	|- ( ph -> ( ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) / ( ( 2 logb A ) ^ 1 ) ) <_ ( ( 4 x. ( ( 2 logb A ) ^ 3 ) ) / ( ( 2 logb A ) ^ 1 ) ) )
423	287 391	readdcld	|- ( ph -> ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) e. RR )
424	6 417	remulcld	|- ( ph -> ( 4 x. ( ( 2 logb A ) ^ 3 ) ) e. RR )
425	423 424 332	lediv1d	|- ( ph -> ( ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) <_ ( 4 x. ( ( 2 logb A ) ^ 3 ) ) <-> ( ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) / ( ( 2 logb A ) ^ 1 ) ) <_ ( ( 4 x. ( ( 2 logb A ) ^ 3 ) ) / ( ( 2 logb A ) ^ 1 ) ) ) )
426	422 425	mpbird	|- ( ph -> ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) <_ ( 4 x. ( ( 2 logb A ) ^ 3 ) ) )
427	87	uzidd	|- ( ph -> 2 e. ( ZZ>= ` 2 ) )
428	427 39	jca	|- ( ph -> ( 2 e. ( ZZ>= ` 2 ) /\ A e. RR+ ) )
429		relogbval	|- ( ( 2 e. ( ZZ>= ` 2 ) /\ A e. RR+ ) -> ( 2 logb A ) = ( ( log ` A ) / ( log ` 2 ) ) )
430	428 429	syl	|- ( ph -> ( 2 logb A ) = ( ( log ` A ) / ( log ` 2 ) ) )
431	430	oveq1d	|- ( ph -> ( ( 2 logb A ) ^ 1 ) = ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) )
432	431	oveq2d	|- ( ph -> ( 2 x. ( ( 2 logb A ) ^ 1 ) ) = ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) )
433	432	oveq2d	|- ( ph -> ( ; 1 0 + ( 2 x. ( ( 2 logb A ) ^ 1 ) ) ) = ( ; 1 0 + ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) ) )
434	430	oveq1d	|- ( ph -> ( ( 2 logb A ) ^ 3 ) = ( ( ( log ` A ) / ( log ` 2 ) ) ^ 3 ) )
435	12 18 26 112	expdivd	|- ( ph -> ( ( ( log ` A ) / ( log ` 2 ) ) ^ 3 ) = ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) )
436	434 435	eqtrd	|- ( ph -> ( ( 2 logb A ) ^ 3 ) = ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) )
437	436	oveq2d	|- ( ph -> ( 4 x. ( ( 2 logb A ) ^ 3 ) ) = ( 4 x. ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) ) )
438	426 433 437	3brtr3d	|- ( ph -> ( ; 1 0 + ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) ) <_ ( 4 x. ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) ) )
439	292 293 299 323 438	letrd	|- ( ph -> ( ( ; 1 0 / ( log ` A ) ) + ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) ) <_ ( 4 x. ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) ) )
440	12	exp1d	|- ( ph -> ( ( log ` A ) ^ 1 ) = ( log ` A ) )
441	440	eqcomd	|- ( ph -> ( log ` A ) = ( ( log ` A ) ^ 1 ) )
442	441	oveq2d	|- ( ph -> ( ; 1 0 / ( log ` A ) ) = ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) )
443	13 156 281 282	divassd	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) = ( 2 x. ( ( ( log ` A ) ^ 1 ) / ( ( log ` 2 ) ^ 1 ) ) ) )
444	12 18 26 91	expdivd	|- ( ph -> ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) = ( ( ( log ` A ) ^ 1 ) / ( ( log ` 2 ) ^ 1 ) ) )
445	444	eqcomd	|- ( ph -> ( ( ( log ` A ) ^ 1 ) / ( ( log ` 2 ) ^ 1 ) ) = ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) )
446	445	oveq2d	|- ( ph -> ( 2 x. ( ( ( log ` A ) ^ 1 ) / ( ( log ` 2 ) ^ 1 ) ) ) = ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) )
447	443 446	eqtrd	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) = ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) )
448	447	eqcomd	|- ( ph -> ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) )
449	442 448	oveq12d	|- ( ph -> ( ( ; 1 0 / ( log ` A ) ) + ( 2 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 1 ) ) ) = ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) ) )
450	113	recnd	|- ( ph -> ( ( log ` A ) ^ 3 ) e. CC )
451	18 112	expcld	|- ( ph -> ( ( log ` 2 ) ^ 3 ) e. CC )
452	416 450 451 297	divassd	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) = ( 4 x. ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) ) )
453	452	eqcomd	|- ( ph -> ( 4 x. ( ( ( log ` A ) ^ 3 ) / ( ( log ` 2 ) ^ 3 ) ) ) = ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) )
454	439 449 453	3brtr3d	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) )
455	285 454	eqbrtrd	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) x. 1 ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) )
456	281 282	dividd	|- ( ph -> ( ( ( log ` 2 ) ^ 1 ) / ( ( log ` 2 ) ^ 1 ) ) = 1 )
457	456	eqcomd	|- ( ph -> 1 = ( ( ( log ` 2 ) ^ 1 ) / ( ( log ` 2 ) ^ 1 ) ) )
458	457	oveq2d	|- ( ph -> ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) x. 1 ) = ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) x. ( ( ( log ` 2 ) ^ 1 ) / ( ( log ` 2 ) ^ 1 ) ) ) )
459	277 281 281 281 282 282	divmuldivd	|- ( ph -> ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) x. ( ( ( log ` 2 ) ^ 1 ) / ( ( log ` 2 ) ^ 1 ) ) ) = ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) ) )
460	458 459	eqtrd	|- ( ph -> ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) x. 1 ) = ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) ) )
461	460	oveq2d	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 1 ) ) x. 1 ) ) = ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) ) ) )
462	416 450	mulcld	|- ( ph -> ( 4 x. ( ( log ` A ) ^ 3 ) ) e. CC )
463	462 451 297	divcld	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) e. CC )
464	463	mulid1d	|- ( ph -> ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) x. 1 ) = ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) )
465	464	eqcomd	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) = ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) x. 1 ) )
466	455 461 465	3brtr3d	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) ) ) <_ ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) x. 1 ) )
467	274 156 247	divcld	|- ( ph -> ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) e. CC )
468	467	mulid1d	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) x. 1 ) = ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) )
469	468	eqcomd	|- ( ph -> ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) = ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) x. 1 ) )
470	18 26	dividd	|- ( ph -> ( ( log ` 2 ) / ( log ` 2 ) ) = 1 )
471	470	eqcomd	|- ( ph -> 1 = ( ( log ` 2 ) / ( log ` 2 ) ) )
472	471	oveq2d	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) x. 1 ) = ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) / ( log ` 2 ) ) ) )
473	469 472	eqtrd	|- ( ph -> ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) = ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) / ( log ` 2 ) ) ) )
474	274 156 18 18 247 26	divmuldivd	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) / ( log ` 2 ) ) ) = ( ( ; 1 0 x. ( log ` 2 ) ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) )
475	473 474	eqtrd	|- ( ph -> ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) = ( ( ; 1 0 x. ( log ` 2 ) ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) )
476	18	exp1d	|- ( ph -> ( ( log ` 2 ) ^ 1 ) = ( log ` 2 ) )
477	476	oveq2d	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) ^ 1 ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( log ` 2 ) ) )
478		df-2	|- 2 = ( 1 + 1 )
479	478	a1i	|- ( ph -> 2 = ( 1 + 1 ) )
480	479	oveq2d	|- ( ph -> ( ( log ` 2 ) ^ 2 ) = ( ( log ` 2 ) ^ ( 1 + 1 ) ) )
481	18 91 91	expaddd	|- ( ph -> ( ( log ` 2 ) ^ ( 1 + 1 ) ) = ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) )
482	480 481	eqtrd	|- ( ph -> ( ( log ` 2 ) ^ 2 ) = ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) )
483	482	eqcomd	|- ( ph -> ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) = ( ( log ` 2 ) ^ 2 ) )
484	477 483	oveq12d	|- ( ph -> ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) ) = ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 2 ) ) )
485	475 484	oveq12d	|- ( ph -> ( ( ; 1 0 / ( ( log ` A ) ^ 1 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( log ` 2 ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 1 ) x. ( ( log ` 2 ) ^ 1 ) ) ) ) = ( ( ( ; 1 0 x. ( log ` 2 ) ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) )
486	476	eqcomd	|- ( ph -> ( log ` 2 ) = ( ( log ` 2 ) ^ 1 ) )
487	486	oveq2d	|- ( ph -> ( ( log ` 2 ) / ( log ` 2 ) ) = ( ( log ` 2 ) / ( ( log ` 2 ) ^ 1 ) ) )
488	471 487	eqtrd	|- ( ph -> 1 = ( ( log ` 2 ) / ( ( log ` 2 ) ^ 1 ) ) )
489	488	oveq2d	|- ( ph -> ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) x. 1 ) = ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) x. ( ( log ` 2 ) / ( ( log ` 2 ) ^ 1 ) ) ) )
490	476 18	eqeltrd	|- ( ph -> ( ( log ` 2 ) ^ 1 ) e. CC )
491	476 26	eqnetrd	|- ( ph -> ( ( log ` 2 ) ^ 1 ) =/= 0 )
492	462 451 18 490 297 491	divmuldivd	|- ( ph -> ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) x. ( ( log ` 2 ) / ( ( log ` 2 ) ^ 1 ) ) ) = ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( log ` 2 ) ) / ( ( ( log ` 2 ) ^ 3 ) x. ( ( log ` 2 ) ^ 1 ) ) ) )
493	489 492	eqtrd	|- ( ph -> ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 3 ) ) x. 1 ) = ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( log ` 2 ) ) / ( ( ( log ` 2 ) ^ 3 ) x. ( ( log ` 2 ) ^ 1 ) ) ) )
494	466 485 493	3brtr3d	|- ( ph -> ( ( ( ; 1 0 x. ( log ` 2 ) ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) <_ ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( log ` 2 ) ) / ( ( ( log ` 2 ) ^ 3 ) x. ( ( log ` 2 ) ^ 1 ) ) ) )
495	156 18	mulcld	|- ( ph -> ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) e. CC )
496	156 18 247 26	mulne0d	|- ( ph -> ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) =/= 0 )
497	274 18 495 496	div23d	|- ( ph -> ( ( ; 1 0 x. ( log ` 2 ) ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) = ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) x. ( log ` 2 ) ) )
498	277 18 155 88	div23d	|- ( ph -> ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 2 ) ) = ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) x. ( log ` 2 ) ) )
499	497 498	oveq12d	|- ( ph -> ( ( ( ; 1 0 x. ( log ` 2 ) ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) = ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) x. ( log ` 2 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) x. ( log ` 2 ) ) ) )
500	62	a1i	|- ( ph -> 4 = ( 3 + 1 ) )
501	500	oveq2d	|- ( ph -> ( ( log ` 2 ) ^ 4 ) = ( ( log ` 2 ) ^ ( 3 + 1 ) ) )
502	18 91 112	expaddd	|- ( ph -> ( ( log ` 2 ) ^ ( 3 + 1 ) ) = ( ( ( log ` 2 ) ^ 3 ) x. ( ( log ` 2 ) ^ 1 ) ) )
503	501 502	eqtrd	|- ( ph -> ( ( log ` 2 ) ^ 4 ) = ( ( ( log ` 2 ) ^ 3 ) x. ( ( log ` 2 ) ^ 1 ) ) )
504	503	eqcomd	|- ( ph -> ( ( ( log ` 2 ) ^ 3 ) x. ( ( log ` 2 ) ^ 1 ) ) = ( ( log ` 2 ) ^ 4 ) )
505	504	oveq2d	|- ( ph -> ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( log ` 2 ) ) / ( ( ( log ` 2 ) ^ 3 ) x. ( ( log ` 2 ) ^ 1 ) ) ) = ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 4 ) ) )
506	494 499 505	3brtr3d	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) x. ( log ` 2 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) x. ( log ` 2 ) ) ) <_ ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 4 ) ) )
507	92 43	remulcld	|- ( ph -> ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) e. RR )
508	287 507 496	redivcld	|- ( ph -> ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) e. RR )
509	508	recnd	|- ( ph -> ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) e. CC )
510	509 278 18	adddird	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) x. ( log ` 2 ) ) = ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) x. ( log ` 2 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) x. ( log ` 2 ) ) ) )
511	510	eqcomd	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) x. ( log ` 2 ) ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) x. ( log ` 2 ) ) ) = ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) x. ( log ` 2 ) ) )
512	18 26 212	expne0d	|- ( ph -> ( ( log ` 2 ) ^ 4 ) =/= 0 )
513	462 18 117 512	div23d	|- ( ph -> ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 4 ) ) = ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 4 ) ) x. ( log ` 2 ) ) )
514	506 511 513	3brtr3d	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) x. ( log ` 2 ) ) <_ ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 4 ) ) x. ( log ` 2 ) ) )
515	37 92	remulcld	|- ( ph -> ( 2 x. ( ( log ` A ) ^ 1 ) ) e. RR )
516	515 85 88	redivcld	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) e. RR )
517	508 516	readdcld	|- ( ph -> ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) e. RR )
518	114 115 120	redivcld	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 4 ) ) e. RR )
519	517 518 135	lemul1d	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 4 ) ) <-> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) x. ( log ` 2 ) ) <_ ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 4 ) ) x. ( log ` 2 ) ) ) )
520	514 519	mpbird	|- ( ph -> ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 4 ) ) )
521	280 520	eqbrtrd	|- ( ph -> ( ( ( ; 1 0 x. 1 ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( 1 x. ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 4 ) ) )
522	274 53 495 496	divassd	|- ( ph -> ( ( ; 1 0 x. 1 ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) = ( ; 1 0 x. ( 1 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) )
523	53 277 155 88	div12d	|- ( ph -> ( 1 x. ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( 1 / ( ( log ` 2 ) ^ 2 ) ) ) )
524	522 523	oveq12d	|- ( ph -> ( ( ( ; 1 0 x. 1 ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) + ( 1 x. ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( log ` 2 ) ^ 2 ) ) ) ) = ( ( ; 1 0 x. ( 1 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( 1 / ( ( log ` 2 ) ^ 2 ) ) ) ) )
525	462	mulid1d	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. 1 ) = ( 4 x. ( ( log ` A ) ^ 3 ) ) )
526	525	eqcomd	|- ( ph -> ( 4 x. ( ( log ` A ) ^ 3 ) ) = ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. 1 ) )
527	526	oveq1d	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( log ` 2 ) ^ 4 ) ) = ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. 1 ) / ( ( log ` 2 ) ^ 4 ) ) )
528	521 524 527	3brtr3d	|- ( ph -> ( ( ; 1 0 x. ( 1 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( 1 / ( ( log ` 2 ) ^ 2 ) ) ) ) <_ ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. 1 ) / ( ( log ` 2 ) ^ 4 ) ) )
529	3 11	dividd	|- ( ph -> ( A / A ) = 1 )
530	529	eqcomd	|- ( ph -> 1 = ( A / A ) )
531	530	oveq1d	|- ( ph -> ( 1 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) = ( ( A / A ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) )
532	3 3 495 11 496	divdiv1d	|- ( ph -> ( ( A / A ) / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) = ( A / ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) )
533	531 532	eqtrd	|- ( ph -> ( 1 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) = ( A / ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) )
534	533	oveq2d	|- ( ph -> ( ; 1 0 x. ( 1 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) = ( ; 1 0 x. ( A / ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) ) )
535		eqidd	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( 1 / ( ( log ` 2 ) ^ 2 ) ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( 1 / ( ( log ` 2 ) ^ 2 ) ) ) )
536	530	oveq1d	|- ( ph -> ( 1 / ( ( log ` 2 ) ^ 2 ) ) = ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) )
537	536	oveq2d	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( 1 / ( ( log ` 2 ) ^ 2 ) ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) ) )
538	535 537	eqtrd	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( 1 / ( ( log ` 2 ) ^ 2 ) ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) ) )
539	534 538	oveq12d	|- ( ph -> ( ( ; 1 0 x. ( 1 / ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( 1 / ( ( log ` 2 ) ^ 2 ) ) ) ) = ( ( ; 1 0 x. ( A / ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) ) ) )
540	462 53 117 512	divassd	|- ( ph -> ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. 1 ) / ( ( log ` 2 ) ^ 4 ) ) = ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( 1 / ( ( log ` 2 ) ^ 4 ) ) ) )
541	528 539 540	3brtr3d	|- ( ph -> ( ( ; 1 0 x. ( A / ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( 1 / ( ( log ` 2 ) ^ 4 ) ) ) )
542	3 495	mulcomd	|- ( ph -> ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) = ( ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) x. A ) )
543	156 18 3	mulassd	|- ( ph -> ( ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) x. A ) = ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) )
544	542 543	eqtrd	|- ( ph -> ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) = ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) )
545	544	oveq2d	|- ( ph -> ( A / ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) = ( A / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) )
546	545	oveq2d	|- ( ph -> ( ; 1 0 x. ( A / ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) ) = ( ; 1 0 x. ( A / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) ) )
547	3 3 155 11 88	divdiv1d	|- ( ph -> ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) = ( A / ( A x. ( ( log ` 2 ) ^ 2 ) ) ) )
548	3 155	mulcomd	|- ( ph -> ( A x. ( ( log ` 2 ) ^ 2 ) ) = ( ( ( log ` 2 ) ^ 2 ) x. A ) )
549	548	oveq2d	|- ( ph -> ( A / ( A x. ( ( log ` 2 ) ^ 2 ) ) ) = ( A / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) )
550	547 549	eqtrd	|- ( ph -> ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) = ( A / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) )
551	550	oveq2d	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( A / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
552	546 551	oveq12d	|- ( ph -> ( ( ; 1 0 x. ( A / ( A x. ( ( ( log ` A ) ^ 1 ) x. ( log ` 2 ) ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 2 ) ) ) ) = ( ( ; 1 0 x. ( A / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( A / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) ) )
553		eqidd	|- ( ph -> ( 1 / ( ( log ` 2 ) ^ 4 ) ) = ( 1 / ( ( log ` 2 ) ^ 4 ) ) )
554	530	oveq1d	|- ( ph -> ( 1 / ( ( log ` 2 ) ^ 4 ) ) = ( ( A / A ) / ( ( log ` 2 ) ^ 4 ) ) )
555	553 554	eqtrd	|- ( ph -> ( 1 / ( ( log ` 2 ) ^ 4 ) ) = ( ( A / A ) / ( ( log ` 2 ) ^ 4 ) ) )
556	555	oveq2d	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( 1 / ( ( log ` 2 ) ^ 4 ) ) ) = ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 4 ) ) ) )
557	541 552 556	3brtr3d	|- ( ph -> ( ( ; 1 0 x. ( A / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( A / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 4 ) ) ) )
558	156 261	mulcld	|- ( ph -> ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) e. CC )
559	156 261 247 262	mulne0d	|- ( ph -> ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) =/= 0 )
560	274 558 3 559	div32d	|- ( ph -> ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) x. A ) = ( ; 1 0 x. ( A / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) ) )
561	560	eqcomd	|- ( ph -> ( ; 1 0 x. ( A / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) ) = ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) x. A ) )
562	155 3	mulcld	|- ( ph -> ( ( ( log ` 2 ) ^ 2 ) x. A ) e. CC )
563	155 3 88 11	mulne0d	|- ( ph -> ( ( ( log ` 2 ) ^ 2 ) x. A ) =/= 0 )
564	277 562 3 563	div32d	|- ( ph -> ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) x. A ) = ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( A / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) )
565	564	eqcomd	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( A / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) = ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) x. A ) )
566	561 565	oveq12d	|- ( ph -> ( ( ; 1 0 x. ( A / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) x. ( A / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) ) = ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) x. A ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) x. A ) ) )
567	3 3 117 11 512	divdiv1d	|- ( ph -> ( ( A / A ) / ( ( log ` 2 ) ^ 4 ) ) = ( A / ( A x. ( ( log ` 2 ) ^ 4 ) ) ) )
568	3 117	mulcomd	|- ( ph -> ( A x. ( ( log ` 2 ) ^ 4 ) ) = ( ( ( log ` 2 ) ^ 4 ) x. A ) )
569	568	oveq2d	|- ( ph -> ( A / ( A x. ( ( log ` 2 ) ^ 4 ) ) ) = ( A / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
570	567 569	eqtrd	|- ( ph -> ( ( A / A ) / ( ( log ` 2 ) ^ 4 ) ) = ( A / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
571	570	oveq2d	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( ( A / A ) / ( ( log ` 2 ) ^ 4 ) ) ) = ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( A / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) ) )
572	557 566 571	3brtr3d	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) x. A ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) x. A ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( A / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) ) )
573	43 1	remulcld	|- ( ph -> ( ( log ` 2 ) x. A ) e. RR )
574	92 573	remulcld	|- ( ph -> ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) e. RR )
575	287 574 559	redivcld	|- ( ph -> ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) e. RR )
576	575	recnd	|- ( ph -> ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) e. CC )
577	157 94	eqeltrrd	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) e. RR )
578	577	recnd	|- ( ph -> ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) e. CC )
579	576 578 3	adddird	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) x. A ) = ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) x. A ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) x. A ) ) )
580	579	eqcomd	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) x. A ) + ( ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) x. A ) ) = ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) x. A ) )
581	12 112	expcld	|- ( ph -> ( ( log ` A ) ^ 3 ) e. CC )
582	416 581	mulcld	|- ( ph -> ( 4 x. ( ( log ` A ) ^ 3 ) ) e. CC )
583	117 3	mulcld	|- ( ph -> ( ( ( log ` 2 ) ^ 4 ) x. A ) e. CC )
584	117 3 512 11	mulne0d	|- ( ph -> ( ( ( log ` 2 ) ^ 4 ) x. A ) =/= 0 )
585	582 583 3 584	div32d	|- ( ph -> ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) x. A ) = ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( A / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) ) )
586	585	eqcomd	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) x. ( A / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) ) = ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) x. A ) )
587	572 580 586	3brtr3d	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) x. A ) <_ ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) x. A ) )
588	575 577	readdcld	|- ( ph -> ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) e. RR )
589	588 122 39	lemul1d	|- ( ph -> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) <-> ( ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) x. A ) <_ ( ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) x. A ) ) )
590	587 589	mpbird	|- ( ph -> ( ( ; 1 0 / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
591	271 590	eqbrtrd	|- ( ph -> ( ( ( 5 x. 2 ) / ( ( ( log ` A ) ^ 1 ) x. ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
592	267 591	eqbrtrd	|- ( ph -> ( ( ( 5 / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 x. 1 ) / ( ( log ` 2 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
593	259 592	eqbrtrd	|- ( ph -> ( ( ( ( 5 x. 1 ) / ( ( log ` A ) ^ 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( 1 / A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
594	254 593	eqbrtrd	|- ( ph -> ( ( ( 5 x. ( 1 / ( ( log ` A ) ^ 1 ) ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( ( log ` 2 ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) / A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
595	246 594	eqbrtrd	|- ( ph -> ( ( ( 5 x. ( ( log ` A ) ^ -u 1 ) ) x. ( ( 2 / ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
596	238 595	eqbrtrd	|- ( ph -> ( ( ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` A ) ^ 5 ) ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
597	211 596	eqbrtrd	|- ( ph -> ( ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` A ) ^ 5 ) ) x. ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
598	205 597	eqbrtrd	|- ( ph -> ( ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. ( 2 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( ( log ` 2 ) x. ( ( log ` 2 ) ^ 5 ) ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
599	198 598	eqbrtrd	|- ( ph -> ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( ( log ` 2 ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
600	192 599	eqbrtrd	|- ( ph -> ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) x. ( 5 x. ( ( log ` A ) ^ 4 ) ) ) / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) x. ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
601	189 600	eqbrtrd	|- ( ph -> ( ( ( ( 2 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
602	184 601	eqbrtrd	|- ( ph -> ( ( ( ( ( 2 x. 1 ) x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
603	179 602	eqbrtrd	|- ( ph -> ( ( ( ( 2 x. ( 1 x. ( ( log ` 2 ) ^ 5 ) ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
604	174 603	eqbrtrd	|- ( ph -> ( ( ( 2 x. ( ( 1 x. ( ( log ` 2 ) ^ 5 ) ) / ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
605	170 604	eqbrtrd	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) x. ( log ` 2 ) ) / ( ( log ` 2 ) ^ 5 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 x. ( ( log ` A ) ^ 1 ) ) / ( ( ( log ` 2 ) ^ 2 ) x. A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
606	158 605	eqbrtrd	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
607	95 111 122 149 606	letrd	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) ^ 5 ) / ( ( log ` 2 ) ^ 5 ) ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
608	35 607	eqbrtrd	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) <_ ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
609	427 39 429	syl2anc	|- ( ph -> ( 2 logb A ) = ( ( log ` A ) / ( log ` 2 ) ) )
610	609	eqcomd	|- ( ph -> ( ( log ` A ) / ( log ` 2 ) ) = ( 2 logb A ) )
611	610	oveq1d	|- ( ph -> ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) = ( ( 2 logb A ) ^ 5 ) )
612	611	oveq1d	|- ( ph -> ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) = ( ( ( 2 logb A ) ^ 5 ) + 1 ) )
613	612	oveq1d	|- ( ph -> ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) = ( ( ( ( 2 logb A ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) )
614	613	oveq2d	|- ( ph -> ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) = ( 1 / ( ( ( ( 2 logb A ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) )
615		5cn	|- 5 e. CC
616	615	a1i	|- ( ph -> 5 e. CC )
617	616 207	mulcld	|- ( ph -> ( 5 x. ( ( log ` A ) ^ 4 ) ) e. CC )
618	617	mulid1d	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. 1 ) = ( 5 x. ( ( log ` A ) ^ 4 ) ) )
619	618	eqcomd	|- ( ph -> ( 5 x. ( ( log ` A ) ^ 4 ) ) = ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. 1 ) )
620		eqidd	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) = ( ( ( log ` 2 ) ^ 5 ) x. A ) )
621		df-5	|- 5 = ( 4 + 1 )
622	621	a1i	|- ( ph -> 5 = ( 4 + 1 ) )
623	622	oveq2d	|- ( ph -> ( ( log ` 2 ) ^ 5 ) = ( ( log ` 2 ) ^ ( 4 + 1 ) ) )
624	18 91 77	expaddd	|- ( ph -> ( ( log ` 2 ) ^ ( 4 + 1 ) ) = ( ( ( log ` 2 ) ^ 4 ) x. ( ( log ` 2 ) ^ 1 ) ) )
625	623 624	eqtrd	|- ( ph -> ( ( log ` 2 ) ^ 5 ) = ( ( ( log ` 2 ) ^ 4 ) x. ( ( log ` 2 ) ^ 1 ) ) )
626	476	oveq2d	|- ( ph -> ( ( ( log ` 2 ) ^ 4 ) x. ( ( log ` 2 ) ^ 1 ) ) = ( ( ( log ` 2 ) ^ 4 ) x. ( log ` 2 ) ) )
627	625 626	eqtrd	|- ( ph -> ( ( log ` 2 ) ^ 5 ) = ( ( ( log ` 2 ) ^ 4 ) x. ( log ` 2 ) ) )
628	627	oveq1d	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) = ( ( ( ( log ` 2 ) ^ 4 ) x. ( log ` 2 ) ) x. A ) )
629	620 628	eqtrd	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) = ( ( ( ( log ` 2 ) ^ 4 ) x. ( log ` 2 ) ) x. A ) )
630	117 18 3	mulassd	|- ( ph -> ( ( ( ( log ` 2 ) ^ 4 ) x. ( log ` 2 ) ) x. A ) = ( ( ( log ` 2 ) ^ 4 ) x. ( ( log ` 2 ) x. A ) ) )
631	629 630	eqtrd	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) = ( ( ( log ` 2 ) ^ 4 ) x. ( ( log ` 2 ) x. A ) ) )
632	18 3	mulcomd	|- ( ph -> ( ( log ` 2 ) x. A ) = ( A x. ( log ` 2 ) ) )
633	632	oveq2d	|- ( ph -> ( ( ( log ` 2 ) ^ 4 ) x. ( ( log ` 2 ) x. A ) ) = ( ( ( log ` 2 ) ^ 4 ) x. ( A x. ( log ` 2 ) ) ) )
634	631 633	eqtrd	|- ( ph -> ( ( ( log ` 2 ) ^ 5 ) x. A ) = ( ( ( log ` 2 ) ^ 4 ) x. ( A x. ( log ` 2 ) ) ) )
635	619 634	oveq12d	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. 1 ) / ( ( ( log ` 2 ) ^ 4 ) x. ( A x. ( log ` 2 ) ) ) ) )
636	3 18	mulcld	|- ( ph -> ( A x. ( log ` 2 ) ) e. CC )
637	3 18 11 26	mulne0d	|- ( ph -> ( A x. ( log ` 2 ) ) =/= 0 )
638	186 117 53 636 120 637	divmuldivd	|- ( ph -> ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` 2 ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) = ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. 1 ) / ( ( ( log ` 2 ) ^ 4 ) x. ( A x. ( log ` 2 ) ) ) ) )
639	638	eqcomd	|- ( ph -> ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) x. 1 ) / ( ( ( log ` 2 ) ^ 4 ) x. ( A x. ( log ` 2 ) ) ) ) = ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` 2 ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
640	635 639	eqtrd	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` 2 ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
641	206 207 117 120	divassd	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` 2 ) ^ 4 ) ) = ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` 2 ) ^ 4 ) ) ) )
642	641	oveq1d	|- ( ph -> ( ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( log ` 2 ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) = ( ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` 2 ) ^ 4 ) ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
643	640 642	eqtrd	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` 2 ) ^ 4 ) ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
644	12 18 26 77	expdivd	|- ( ph -> ( ( ( log ` A ) / ( log ` 2 ) ) ^ 4 ) = ( ( ( log ` A ) ^ 4 ) / ( ( log ` 2 ) ^ 4 ) ) )
645	644	eqcomd	|- ( ph -> ( ( ( log ` A ) ^ 4 ) / ( ( log ` 2 ) ^ 4 ) ) = ( ( ( log ` A ) / ( log ` 2 ) ) ^ 4 ) )
646	645	oveq2d	|- ( ph -> ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` 2 ) ^ 4 ) ) ) = ( 5 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 4 ) ) )
647	646	oveq1d	|- ( ph -> ( ( 5 x. ( ( ( log ` A ) ^ 4 ) / ( ( log ` 2 ) ^ 4 ) ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) = ( ( 5 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
648	643 647	eqtrd	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( 5 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
649	610	oveq1d	|- ( ph -> ( ( ( log ` A ) / ( log ` 2 ) ) ^ 4 ) = ( ( 2 logb A ) ^ 4 ) )
650	649	oveq2d	|- ( ph -> ( 5 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 4 ) ) = ( 5 x. ( ( 2 logb A ) ^ 4 ) ) )
651	650	oveq1d	|- ( ph -> ( ( 5 x. ( ( ( log ` A ) / ( log ` 2 ) ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) = ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
652	648 651	eqtrd	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
653	342 77	expcld	|- ( ph -> ( ( 2 logb A ) ^ 4 ) e. CC )
654	616 653	mulcld	|- ( ph -> ( 5 x. ( ( 2 logb A ) ^ 4 ) ) e. CC )
655	39	rpne0d	|- ( ph -> A =/= 0 )
656	3 18 655 26	mulne0d	|- ( ph -> ( A x. ( log ` 2 ) ) =/= 0 )
657	636 656	reccld	|- ( ph -> ( 1 / ( A x. ( log ` 2 ) ) ) e. CC )
658	654 657	mulcld	|- ( ph -> ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) e. CC )
659	658	addid1d	|- ( ph -> ( ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) + 0 ) = ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) )
660	659	eqcomd	|- ( ph -> ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) = ( ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) + 0 ) )
661	652 660	eqtrd	|- ( ph -> ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) = ( ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) + 0 ) )
662	614 661	oveq12d	|- ( ph -> ( ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) = ( ( 1 / ( ( ( ( 2 logb A ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) + 0 ) ) )
663	662	oveq2d	|- ( ph -> ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) = ( 2 x. ( ( 1 / ( ( ( ( 2 logb A ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) + 0 ) ) ) )
664		1e2m1	|- 1 = ( 2 - 1 )
665	664	a1i	|- ( ph -> 1 = ( 2 - 1 ) )
666	665	oveq2d	|- ( ph -> ( ( log ` A ) ^ 1 ) = ( ( log ` A ) ^ ( 2 - 1 ) ) )
667	666	oveq1d	|- ( ph -> ( ( ( log ` A ) ^ 1 ) / A ) = ( ( ( log ` A ) ^ ( 2 - 1 ) ) / A ) )
668	667	oveq2d	|- ( ph -> ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) = ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ ( 2 - 1 ) ) / A ) ) )
669	663 668	oveq12d	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( ( log ` A ) / ( log ` 2 ) ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( 5 x. ( ( log ` A ) ^ 4 ) ) / ( ( ( log ` 2 ) ^ 5 ) x. A ) ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ 1 ) / A ) ) ) = ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb A ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ ( 2 - 1 ) ) / A ) ) ) )
670		4cn	|- 4 e. CC
671	670	a1i	|- ( ph -> 4 e. CC )
672	671 117 581 3 120 655	divmuldivd	|- ( ph -> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` A ) ^ 3 ) / A ) ) = ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) )
673	672	eqcomd	|- ( ph -> ( ( 4 x. ( ( log ` A ) ^ 3 ) ) / ( ( ( log ` 2 ) ^ 4 ) x. A ) ) = ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` A ) ^ 3 ) / A ) ) )
674	608 669 673	3brtr3d	|- ( ph -> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb A ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb A ) ^ 4 ) ) x. ( 1 / ( A x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` A ) ^ ( 2 - 1 ) ) / A ) ) ) <_ ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` A ) ^ 3 ) / A ) ) )