Theorem hgt750lem2

Description: Decimal multiplication galore! (Contributed by Thierry Arnoux, 26-Dec-2021)

	Ref	Expression
Assertion	hgt750lem2	|- ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 7 . _ 3 _ 4 8 )

Proof

Step	Hyp	Ref	Expression
1		1nn0	|- 1 e. NN0
2		0re	|- 0 e. RR
3		7re	|- 7 e. RR
4		9re	|- 9 e. RR
5		5re	|- 5 e. RR
6	5 5	pm3.2i	|- ( 5 e. RR /\ 5 e. RR )
7		dp2cl	|- ( ( 5 e. RR /\ 5 e. RR ) -> _ 5 5 e. RR )
8	6 7	ax-mp	|- _ 5 5 e. RR
9	4 8	pm3.2i	|- ( 9 e. RR /\ _ 5 5 e. RR )
10		dp2cl	|- ( ( 9 e. RR /\ _ 5 5 e. RR ) -> _ 9 _ 5 5 e. RR )
11	9 10	ax-mp	|- _ 9 _ 5 5 e. RR
12	4 11	pm3.2i	|- ( 9 e. RR /\ _ 9 _ 5 5 e. RR )
13		dp2cl	|- ( ( 9 e. RR /\ _ 9 _ 5 5 e. RR ) -> _ 9 _ 9 _ 5 5 e. RR )
14	12 13	ax-mp	|- _ 9 _ 9 _ 5 5 e. RR
15	3 14	pm3.2i	|- ( 7 e. RR /\ _ 9 _ 9 _ 5 5 e. RR )
16		dp2cl	|- ( ( 7 e. RR /\ _ 9 _ 9 _ 5 5 e. RR ) -> _ 7 _ 9 _ 9 _ 5 5 e. RR )
17	15 16	ax-mp	|- _ 7 _ 9 _ 9 _ 5 5 e. RR
18	2 17	pm3.2i	|- ( 0 e. RR /\ _ 7 _ 9 _ 9 _ 5 5 e. RR )
19		dp2cl	|- ( ( 0 e. RR /\ _ 7 _ 9 _ 9 _ 5 5 e. RR ) -> _ 0 _ 7 _ 9 _ 9 _ 5 5 e. RR )
20	18 19	ax-mp	|- _ 0 _ 7 _ 9 _ 9 _ 5 5 e. RR
21		dpcl	|- ( ( 1 e. NN0 /\ _ 0 _ 7 _ 9 _ 9 _ 5 5 e. RR ) -> ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR )
22	1 20 21	mp2an	|- ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR
23	22	resqcli	|- ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) e. RR
24		4nn0	|- 4 e. NN0
25		4nn	|- 4 e. NN
26		nnrp	|- ( 4 e. NN -> 4 e. RR+ )
27	25 26	ax-mp	|- 4 e. RR+
28	1 27	rpdp2cl	|- _ 1 4 e. RR+
29	24 28	rpdp2cl	|- _ 4 _ 1 4 e. RR+
30	1 29	rpdpcl	|- ( 1 . _ 4 _ 1 4 ) e. RR+
31		rpre	|- ( ( 1 . _ 4 _ 1 4 ) e. RR+ -> ( 1 . _ 4 _ 1 4 ) e. RR )
32	30 31	ax-mp	|- ( 1 . _ 4 _ 1 4 ) e. RR
33	23 32	remulcli	|- ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR
34		6re	|- 6 e. RR
35		1re	|- 1 e. RR
36	5 35	pm3.2i	|- ( 5 e. RR /\ 1 e. RR )
37		dp2cl	|- ( ( 5 e. RR /\ 1 e. RR ) -> _ 5 1 e. RR )
38	36 37	ax-mp	|- _ 5 1 e. RR
39	34 38	pm3.2i	|- ( 6 e. RR /\ _ 5 1 e. RR )
40		dp2cl	|- ( ( 6 e. RR /\ _ 5 1 e. RR ) -> _ 6 _ 5 1 e. RR )
41	39 40	ax-mp	|- _ 6 _ 5 1 e. RR
42		dpcl	|- ( ( 1 e. NN0 /\ _ 6 _ 5 1 e. RR ) -> ( 1 . _ 6 _ 5 1 ) e. RR )
43	1 41 42	mp2an	|- ( 1 . _ 6 _ 5 1 ) e. RR
44	33 43	pm3.2i	|- ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR /\ ( 1 . _ 6 _ 5 1 ) e. RR )
45	22	sqge0i	|- 0 <_ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 )
46		rpgt0	|- ( ( 1 . _ 4 _ 1 4 ) e. RR+ -> 0 < ( 1 . _ 4 _ 1 4 ) )
47	30 46	ax-mp	|- 0 < ( 1 . _ 4 _ 1 4 )
48	2 32 47	ltleii	|- 0 <_ ( 1 . _ 4 _ 1 4 )
49	23 32	mulge0i	|- ( ( 0 <_ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) /\ 0 <_ ( 1 . _ 4 _ 1 4 ) ) -> 0 <_ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) )
50	45 48 49	mp2an	|- 0 <_ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) )
51		0nn0	|- 0 e. NN0
52		7nn0	|- 7 e. NN0
53		9nn0	|- 9 e. NN0
54		5nn0	|- 5 e. NN0
55		5nn	|- 5 e. NN
56		nnrp	|- ( 5 e. NN -> 5 e. RR+ )
57	55 56	ax-mp	|- 5 e. RR+
58	54 57	rpdp2cl	|- _ 5 5 e. RR+
59	53 58	rpdp2cl	|- _ 9 _ 5 5 e. RR+
60	53 59	rpdp2cl	|- _ 9 _ 9 _ 5 5 e. RR+
61	52 60	rpdp2cl	|- _ 7 _ 9 _ 9 _ 5 5 e. RR+
62	51 61	rpdp2cl	|- _ 0 _ 7 _ 9 _ 9 _ 5 5 e. RR+
63		8nn	|- 8 e. NN
64	63	rpdp2cl2	|- _ 8 0 e. RR+
65	51 64	rpdp2cl	|- _ 0 _ 8 0 e. RR+
66		9lt10	|- 9 < ; 1 0
67		5lt10	|- 5 < ; 1 0
68	54 57 67 67	dp2lt10	|- _ 5 5 < ; 1 0
69	53 58 66 68	dp2lt10	|- _ 9 _ 5 5 < ; 1 0
70	53 59 66 69	dp2lt10	|- _ 9 _ 9 _ 5 5 < ; 1 0
71		7p1e8	|- ( 7 + 1 ) = 8
72	52 60 70 71	dp2ltsuc	|- _ 7 _ 9 _ 9 _ 5 5 < 8
73		8nn0	|- 8 e. NN0
74	73	dp20u	|- _ 8 0 = 8
75	72 74	breqtrri	|- _ 7 _ 9 _ 9 _ 5 5 < _ 8 0
76	51 61 64 75	dp2lt	|- _ 0 _ 7 _ 9 _ 9 _ 5 5 < _ 0 _ 8 0
77	1 62 65 76	dplt	|- ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) < ( 1 . _ 0 _ 8 0 )
78	1 62	rpdpcl	|- ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR+
79		rpge0	|- ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR+ -> 0 <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) )
80	78 79	ax-mp	|- 0 <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 )
81	1 65	rpdpcl	|- ( 1 . _ 0 _ 8 0 ) e. RR+
82		rpge0	|- ( ( 1 . _ 0 _ 8 0 ) e. RR+ -> 0 <_ ( 1 . _ 0 _ 8 0 ) )
83	81 82	ax-mp	|- 0 <_ ( 1 . _ 0 _ 8 0 )
84		8re	|- 8 e. RR
85	84 2	pm3.2i	|- ( 8 e. RR /\ 0 e. RR )
86		dp2cl	|- ( ( 8 e. RR /\ 0 e. RR ) -> _ 8 0 e. RR )
87	85 86	ax-mp	|- _ 8 0 e. RR
88	2 87	pm3.2i	|- ( 0 e. RR /\ _ 8 0 e. RR )
89		dp2cl	|- ( ( 0 e. RR /\ _ 8 0 e. RR ) -> _ 0 _ 8 0 e. RR )
90	88 89	ax-mp	|- _ 0 _ 8 0 e. RR
91		dpcl	|- ( ( 1 e. NN0 /\ _ 0 _ 8 0 e. RR ) -> ( 1 . _ 0 _ 8 0 ) e. RR )
92	1 90 91	mp2an	|- ( 1 . _ 0 _ 8 0 ) e. RR
93	22 92	lt2sqi	|- ( ( 0 <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ 0 <_ ( 1 . _ 0 _ 8 0 ) ) -> ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) < ( 1 . _ 0 _ 8 0 ) <-> ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) < ( ( 1 . _ 0 _ 8 0 ) ^ 2 ) ) )
94	80 83 93	mp2an	|- ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) < ( 1 . _ 0 _ 8 0 ) <-> ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) < ( ( 1 . _ 0 _ 8 0 ) ^ 2 ) )
95	77 94	mpbi	|- ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) < ( ( 1 . _ 0 _ 8 0 ) ^ 2 )
96	92	recni	|- ( 1 . _ 0 _ 8 0 ) e. CC
97	96	sqvali	|- ( ( 1 . _ 0 _ 8 0 ) ^ 2 ) = ( ( 1 . _ 0 _ 8 0 ) x. ( 1 . _ 0 _ 8 0 ) )
98		6nn0	|- 6 e. NN0
99	1 98	deccl	|- ; 1 6 e. NN0
100	98 24	deccl	|- ; 6 4 e. NN0
101		4lt10	|- 4 < ; 1 0
102		10pos	|- 0 < ; 1 0
103	99 51	deccl	|- ; ; 1 6 0 e. NN0
104		eqid	|- ; ; ; 1 6 0 0 = ; ; ; 1 6 0 0
105		eqid	|- ; 6 4 = ; 6 4
106		eqid	|- ; ; 1 6 0 = ; ; 1 6 0
107	98	dec0h	|- 6 = ; 0 6
108	99	nn0cni	|- ; 1 6 e. CC
109	108	addridi	|- ( ; 1 6 + 0 ) = ; 1 6
110		6cn	|- 6 e. CC
111	110	addlidi	|- ( 0 + 6 ) = 6
112	99 51 51 98 106 107 109 111	decadd	|- ( ; ; 1 6 0 + 6 ) = ; ; 1 6 6
113		4cn	|- 4 e. CC
114	113	addlidi	|- ( 0 + 4 ) = 4
115	103 51 98 24 104 105 112 114	decadd	|- ( ; ; ; 1 6 0 0 + ; 6 4 ) = ; ; ; 1 6 6 4
116		1t1e1	|- ( 1 x. 1 ) = 1
117	1	dp0u	|- ( 1 . 0 ) = 1
118	117 117	oveq12i	|- ( ( 1 . 0 ) x. ( 1 . 0 ) ) = ( 1 x. 1 )
119	51	dp20u	|- _ 0 0 = 0
120	119	oveq2i	|- ( 1 . _ 0 0 ) = ( 1 . 0 )
121	120 117	eqtri	|- ( 1 . _ 0 0 ) = 1
122	116 118 121	3eqtr4i	|- ( ( 1 . 0 ) x. ( 1 . 0 ) ) = ( 1 . _ 0 0 )
123		8t8e64	|- ( 8 x. 8 ) = ; 6 4
124	73	dp0u	|- ( 8 . 0 ) = 8
125	124 124	oveq12i	|- ( ( 8 . 0 ) x. ( 8 . 0 ) ) = ( 8 x. 8 )
126	119	oveq2i	|- ( ; 6 4 . _ 0 0 ) = ( ; 6 4 . 0 )
127	100	dp0u	|- ( ; 6 4 . 0 ) = ; 6 4
128	126 127	eqtri	|- ( ; 6 4 . _ 0 0 ) = ; 6 4
129	123 125 128	3eqtr4i	|- ( ( 8 . 0 ) x. ( 8 . 0 ) ) = ( ; 6 4 . _ 0 0 )
130		10nn0	|- ; 1 0 e. NN0
131	130 51	deccl	|- ; ; 1 0 0 e. NN0
132		eqid	|- ; ; ; 1 0 0 1 = ; ; ; 1 0 0 1
133		eqid	|- ; ; 1 6 6 = ; ; 1 6 6
134		eqid	|- ; ; 1 0 0 = ; ; 1 0 0
135		eqid	|- ; 1 6 = ; 1 6
136		dec10p	|- ( ; 1 0 + 1 ) = ; 1 1
137	130 51 1 98 134 135 136 111	decadd	|- ( ; ; 1 0 0 + ; 1 6 ) = ; ; 1 1 6
138		ax-1cn	|- 1 e. CC
139	138 110	addcomi	|- ( 1 + 6 ) = ( 6 + 1 )
140		6p1e7	|- ( 6 + 1 ) = 7
141	139 140	eqtri	|- ( 1 + 6 ) = 7
142	131 1 99 98 132 133 137 141	decadd	|- ( ; ; ; 1 0 0 1 + ; ; 1 6 6 ) = ; ; ; 1 1 6 7
143		eqid	|- ; 1 7 = ; 1 7
144	141	oveq1i	|- ( ( 1 + 6 ) + 1 ) = ( 7 + 1 )
145	144 71	eqtri	|- ( ( 1 + 6 ) + 1 ) = 8
146		7p4e11	|- ( 7 + 4 ) = ; 1 1
147	1 52 98 24 143 105 145 1 146	decaddc	|- ( ; 1 7 + ; 6 4 ) = ; 8 1
148	119	oveq2i	|- ( ; 1 6 . _ 0 0 ) = ( ; 1 6 . 0 )
149	99	dp0u	|- ( ; 1 6 . 0 ) = ; 1 6
150	148 149	eqtri	|- ( ; 1 6 . _ 0 0 ) = ; 1 6
151	121 150	oveq12i	|- ( ( 1 . _ 0 0 ) + ( ; 1 6 . _ 0 0 ) ) = ( 1 + ; 1 6 )
152	1	dec0h	|- 1 = ; 0 1
153	138	addlidi	|- ( 0 + 1 ) = 1
154	51 1 1 98 152 135 153 141	decadd	|- ( 1 + ; 1 6 ) = ; 1 7
155	151 154	eqtri	|- ( ( 1 . _ 0 0 ) + ( ; 1 6 . _ 0 0 ) ) = ; 1 7
156	155 128	oveq12i	|- ( ( ( 1 . _ 0 0 ) + ( ; 1 6 . _ 0 0 ) ) + ( ; 6 4 . _ 0 0 ) ) = ( ; 1 7 + ; 6 4 )
157	117 124	oveq12i	|- ( ( 1 . 0 ) + ( 8 . 0 ) ) = ( 1 + 8 )
158		8cn	|- 8 e. CC
159	138 158	addcomi	|- ( 1 + 8 ) = ( 8 + 1 )
160		8p1e9	|- ( 8 + 1 ) = 9
161	157 159 160	3eqtri	|- ( ( 1 . 0 ) + ( 8 . 0 ) ) = 9
162	161 161	oveq12i	|- ( ( ( 1 . 0 ) + ( 8 . 0 ) ) x. ( ( 1 . 0 ) + ( 8 . 0 ) ) ) = ( 9 x. 9 )
163		9t9e81	|- ( 9 x. 9 ) = ; 8 1
164	162 163	eqtri	|- ( ( ( 1 . 0 ) + ( 8 . 0 ) ) x. ( ( 1 . 0 ) + ( 8 . 0 ) ) ) = ; 8 1
165	147 156 164	3eqtr4ri	|- ( ( ( 1 . 0 ) + ( 8 . 0 ) ) x. ( ( 1 . 0 ) + ( 8 . 0 ) ) ) = ( ( ( 1 . _ 0 0 ) + ( ; 1 6 . _ 0 0 ) ) + ( ; 6 4 . _ 0 0 ) )
166	1 51 73 51 1 73 51 51 51 51 1 99 51 51 100 51 51 1 98 98 24 1 1 98 52 101 102 102 115 122 129 142 165	dpmul4	|- ( ( 1 . _ 0 _ 8 0 ) x. ( 1 . _ 0 _ 8 0 ) ) < ( 1 . _ 1 _ 6 7 )
167	97 166	eqbrtri	|- ( ( 1 . _ 0 _ 8 0 ) ^ 2 ) < ( 1 . _ 1 _ 6 7 )
168	92	resqcli	|- ( ( 1 . _ 0 _ 8 0 ) ^ 2 ) e. RR
169	34 3	pm3.2i	|- ( 6 e. RR /\ 7 e. RR )
170		dp2cl	|- ( ( 6 e. RR /\ 7 e. RR ) -> _ 6 7 e. RR )
171	169 170	ax-mp	|- _ 6 7 e. RR
172	35 171	pm3.2i	|- ( 1 e. RR /\ _ 6 7 e. RR )
173		dp2cl	|- ( ( 1 e. RR /\ _ 6 7 e. RR ) -> _ 1 _ 6 7 e. RR )
174	172 173	ax-mp	|- _ 1 _ 6 7 e. RR
175		dpcl	|- ( ( 1 e. NN0 /\ _ 1 _ 6 7 e. RR ) -> ( 1 . _ 1 _ 6 7 ) e. RR )
176	1 174 175	mp2an	|- ( 1 . _ 1 _ 6 7 ) e. RR
177	23 168 176	lttri	|- ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) < ( ( 1 . _ 0 _ 8 0 ) ^ 2 ) /\ ( ( 1 . _ 0 _ 8 0 ) ^ 2 ) < ( 1 . _ 1 _ 6 7 ) ) -> ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) < ( 1 . _ 1 _ 6 7 ) )
178	95 167 177	mp2an	|- ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) < ( 1 . _ 1 _ 6 7 )
179	23 176 32 47	ltmul1ii	|- ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) < ( 1 . _ 1 _ 6 7 ) <-> ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( ( 1 . _ 1 _ 6 7 ) x. ( 1 . _ 4 _ 1 4 ) ) )
180	178 179	mpbi	|- ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( ( 1 . _ 1 _ 6 7 ) x. ( 1 . _ 4 _ 1 4 ) )
181		2nn0	|- 2 e. NN0
182		3nn0	|- 3 e. NN0
183		1lt10	|- 1 < ; 1 0
184		3lt10	|- 3 < ; 1 0
185		8lt10	|- 8 < ; 1 0
186	130 53	deccl	|- ; ; 1 0 9 e. NN0
187		eqid	|- ; ; ; 1 0 9 2 = ; ; ; 1 0 9 2
188	53	dec0h	|- 9 = ; 0 9
189	186	nn0cni	|- ; ; 1 0 9 e. CC
190	189	addridi	|- ( ; ; 1 0 9 + 0 ) = ; ; 1 0 9
191		dec10p	|- ( ; 1 0 + 0 ) = ; 1 0
192	138	addridi	|- ( 1 + 0 ) = 1
193	1 51 51 1 191 152 192 153	decadd	|- ( ( ; 1 0 + 0 ) + 1 ) = ; 1 1
194		9p1e10	|- ( 9 + 1 ) = ; 1 0
195	130 53 51 1 190 152 193 51 194	decaddc	|- ( ( ; ; 1 0 9 + 0 ) + 1 ) = ; ; 1 1 0
196		9cn	|- 9 e. CC
197		2cn	|- 2 e. CC
198	196 197	addcomi	|- ( 9 + 2 ) = ( 2 + 9 )
199		9p2e11	|- ( 9 + 2 ) = ; 1 1
200	198 199	eqtr3i	|- ( 2 + 9 ) = ; 1 1
201	186 181 51 53 187 188 195 1 200	decaddc	|- ( ; ; ; 1 0 9 2 + 9 ) = ; ; ; 1 1 0 1
202	113 138	mulcomi	|- ( 4 x. 1 ) = ( 1 x. 4 )
203	113	mulridi	|- ( 4 x. 1 ) = 4
204	202 203	eqtr3i	|- ( 1 x. 4 ) = 4
205	24	dec0h	|- 4 = ; 0 4
206	203 202 205	3eqtr3i	|- ( 1 x. 4 ) = ; 0 4
207	138 113	addcli	|- ( 1 + 4 ) e. CC
208	207	addridi	|- ( ( 1 + 4 ) + 0 ) = ( 1 + 4 )
209	113 138	addcomi	|- ( 4 + 1 ) = ( 1 + 4 )
210		4p1e5	|- ( 4 + 1 ) = 5
211	208 209 210	3eqtr2i	|- ( ( 1 + 4 ) + 0 ) = 5
212	54	dec0h	|- 5 = ; 0 5
213	211 212	eqtri	|- ( ( 1 + 4 ) + 0 ) = ; 0 5
214	1 1 1 24 51 51 54 24 116 204 116 206 213 192	dpmul	|- ( ( 1 . 1 ) x. ( 1 . 4 ) ) = ( 1 . _ 5 4 )
215	110	mulridi	|- ( 6 x. 1 ) = 6
216		6t4e24	|- ( 6 x. 4 ) = ; 2 4
217		7cn	|- 7 e. CC
218	217	mulridi	|- ( 7 x. 1 ) = 7
219		7t4e28	|- ( 7 x. 4 ) = ; 2 8
220	181 24	deccl	|- ; 2 4 e. NN0
221	220	nn0cni	|- ; 2 4 e. CC
222	221 217	addcomi	|- ( ; 2 4 + 7 ) = ( 7 + ; 2 4 )
223		eqid	|- ; 2 4 = ; 2 4
224		2p1e3	|- ( 2 + 1 ) = 3
225	217 113 146	addcomli	|- ( 4 + 7 ) = ; 1 1
226	181 24 52 223 224 1 225	decaddci	|- ( ; 2 4 + 7 ) = ; 3 1
227	222 226	eqtr3i	|- ( 7 + ; 2 4 ) = ; 3 1
228	227	oveq1i	|- ( ( 7 + ; 2 4 ) + 2 ) = ( ; 3 1 + 2 )
229		eqid	|- ; 3 1 = ; 3 1
230	197 138 224	addcomli	|- ( 1 + 2 ) = 3
231	182 1 181 229 230	decaddi	|- ( ; 3 1 + 2 ) = ; 3 3
232	228 231	eqtri	|- ( ( 7 + ; 2 4 ) + 2 ) = ; 3 3
233		6p3e9	|- ( 6 + 3 ) = 9
234	98 52 1 24 181 182 182 73 215 216 218 219 232 233	dpmul	|- ( ( 6 . 7 ) x. ( 1 . 4 ) ) = ( 9 . _ 3 8 )
235	1 54	deccl	|- ; 1 5 e. NN0
236	235 24	deccl	|- ; ; 1 5 4 e. NN0
237	51 1	deccl	|- ; 0 1 e. NN0
238	237 1	deccl	|- ; ; 0 1 1 e. NN0
239		eqid	|- ; ; ; 1 5 4 1 = ; ; ; 1 5 4 1
240	152	deceq1i	|- ; 1 1 = ; ; 0 1 1
241	240	deceq1i	|- ; ; 1 1 0 = ; ; ; 0 1 1 0
242		eqid	|- ; ; 1 5 4 = ; ; 1 5 4
243		eqid	|- ; ; 0 1 1 = ; ; 0 1 1
244	152	oveq2i	|- ( ; 1 5 + 1 ) = ( ; 1 5 + ; 0 1 )
245		eqid	|- ; 1 5 = ; 1 5
246		5p1e6	|- ( 5 + 1 ) = 6
247	1 54 1 245 246	decaddi	|- ( ; 1 5 + 1 ) = ; 1 6
248	244 247	eqtr3i	|- ( ; 1 5 + ; 0 1 ) = ; 1 6
249	235 24 237 1 242 243 248 210	decadd	|- ( ; ; 1 5 4 + ; ; 0 1 1 ) = ; ; 1 6 5
250	236 1 238 51 239 241 249 192	decadd	|- ( ; ; ; 1 5 4 1 + ; ; 1 1 0 ) = ; ; ; 1 6 5 1
251		7t2e14	|- ( 7 x. 2 ) = ; 1 4
252		8t7e56	|- ( 8 x. 7 ) = ; 5 6
253	158 217 252	mulcomli	|- ( 7 x. 8 ) = ; 5 6
254		8t2e16	|- ( 8 x. 2 ) = ; 1 6
255		eqid	|- ; 5 6 = ; 5 6
256		5cn	|- 5 e. CC
257	256 138 246	addcomli	|- ( 1 + 5 ) = 6
258	257	oveq1i	|- ( ( 1 + 5 ) + 1 ) = ( 6 + 1 )
259	258 140	eqtri	|- ( ( 1 + 5 ) + 1 ) = 7
260		6p6e12	|- ( 6 + 6 ) = ; 1 2
261	1 98 54 98 135 255 259 181 260	decaddc	|- ( ; 1 6 + ; 5 6 ) = ; 7 2
262	261	oveq1i	|- ( ( ; 1 6 + ; 5 6 ) + 6 ) = ( ; 7 2 + 6 )
263		eqid	|- ; 7 2 = ; 7 2
264		6p2e8	|- ( 6 + 2 ) = 8
265	110 197 264	addcomli	|- ( 2 + 6 ) = 8
266	52 181 98 263 265	decaddi	|- ( ; 7 2 + 6 ) = ; 7 8
267	262 266	eqtri	|- ( ( ; 1 6 + ; 5 6 ) + 6 ) = ; 7 8
268		eqid	|- ; 1 4 = ; 1 4
269		1p1e2	|- ( 1 + 1 ) = 2
270	1 24 52 268 269 1 225	decaddci	|- ( ; 1 4 + 7 ) = ; 2 1
271	52 73 181 73 98 52 73 24 251 253 254 123 267 270	dpmul	|- ( ( 7 . 8 ) x. ( 2 . 8 ) ) = ( ; 2 1 . _ 8 4 )
272		eqid	|- ; 1 1 = ; 1 1
273		eqid	|- ; 6 7 = ; 6 7
274	217 138 71	addcomli	|- ( 1 + 7 ) = 8
275	1 1 98 52 272 273 141 274	decadd	|- ( ; 1 1 + ; 6 7 ) = ; 7 8
276	1 1 98 52 52 73 275	dpadd	|- ( ( 1 . 1 ) + ( 6 . 7 ) ) = ( 7 . 8 )
277		4p4e8	|- ( 4 + 4 ) = 8
278	1 24 1 24 268 268 269 277	decadd	|- ( ; 1 4 + ; 1 4 ) = ; 2 8
279	1 24 1 24 181 73 278	dpadd	|- ( ( 1 . 4 ) + ( 1 . 4 ) ) = ( 2 . 8 )
280	276 279	oveq12i	|- ( ( ( 1 . 1 ) + ( 6 . 7 ) ) x. ( ( 1 . 4 ) + ( 1 . 4 ) ) ) = ( ( 7 . 8 ) x. ( 2 . 8 ) )
281	1 181	deccl	|- ; 1 2 e. NN0
282		eqid	|- ; ; 1 0 9 = ; ; 1 0 9
283	130	nn0cni	|- ; 1 0 e. CC
284	283 138 136	addcomli	|- ( 1 + ; 1 0 ) = ; 1 1
285	1 1 269 284	decsuc	|- ( ( 1 + ; 1 0 ) + 1 ) = ; 1 2
286		9p5e14	|- ( 9 + 5 ) = ; 1 4
287	196 256 286	addcomli	|- ( 5 + 9 ) = ; 1 4
288	1 54 130 53 245 282 285 24 287	decaddc	|- ( ; 1 5 + ; ; 1 0 9 ) = ; ; 1 2 4
289		4p2e6	|- ( 4 + 2 ) = 6
290	235 24 186 181 242 187 288 289	decadd	|- ( ; ; 1 5 4 + ; ; ; 1 0 9 2 ) = ; ; ; 1 2 4 6
291	1 54 24 130 53 281 181 24 98 290	dpadd3	|- ( ( 1 . _ 5 4 ) + ( ; 1 0 . _ 9 2 ) ) = ( ; 1 2 . _ 4 6 )
292	291	oveq1i	|- ( ( ( 1 . _ 5 4 ) + ( ; 1 0 . _ 9 2 ) ) + ( 9 . _ 3 8 ) ) = ( ( ; 1 2 . _ 4 6 ) + ( 9 . _ 3 8 ) )
293	181 1	deccl	|- ; 2 1 e. NN0
294	281 24	deccl	|- ; ; 1 2 4 e. NN0
295	53 182	deccl	|- ; 9 3 e. NN0
296		eqid	|- ; ; ; 1 2 4 6 = ; ; ; 1 2 4 6
297		eqid	|- ; ; 9 3 8 = ; ; 9 3 8
298		eqid	|- ; ; 1 2 4 = ; ; 1 2 4
299		eqid	|- ; 9 3 = ; 9 3
300		eqid	|- ; 1 2 = ; 1 2
301	1 181 53 300 269 1 200	decaddci	|- ( ; 1 2 + 9 ) = ; 2 1
302		4p3e7	|- ( 4 + 3 ) = 7
303	281 24 53 182 298 299 301 302	decadd	|- ( ; ; 1 2 4 + ; 9 3 ) = ; ; 2 1 7
304	293 52 71 303	decsuc	|- ( ( ; ; 1 2 4 + ; 9 3 ) + 1 ) = ; ; 2 1 8
305		8p6e14	|- ( 8 + 6 ) = ; 1 4
306	158 110 305	addcomli	|- ( 6 + 8 ) = ; 1 4
307	294 98 295 73 296 297 304 24 306	decaddc	|- ( ; ; ; 1 2 4 6 + ; ; 9 3 8 ) = ; ; ; 2 1 8 4
308	281 24 98 53 182 293 73 73 24 307	dpadd3	|- ( ( ; 1 2 . _ 4 6 ) + ( 9 . _ 3 8 ) ) = ( ; 2 1 . _ 8 4 )
309	292 308	eqtri	|- ( ( ( 1 . _ 5 4 ) + ( ; 1 0 . _ 9 2 ) ) + ( 9 . _ 3 8 ) ) = ( ; 2 1 . _ 8 4 )
310	271 280 309	3eqtr4i	|- ( ( ( 1 . 1 ) + ( 6 . 7 ) ) x. ( ( 1 . 4 ) + ( 1 . 4 ) ) ) = ( ( ( 1 . _ 5 4 ) + ( ; 1 0 . _ 9 2 ) ) + ( 9 . _ 3 8 ) )
311	1 1 98 52 1 1 54 24 24 24 1 130 53 181 53 182 73 1 1 51 1 1 98 54 1 183 184 185 201 214 234 250 310	dpmul4	|- ( ( 1 . _ 1 _ 6 7 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 )
312	176 32	remulcli	|- ( ( 1 . _ 1 _ 6 7 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR
313	33 312 43	lttri	|- ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( ( 1 . _ 1 _ 6 7 ) x. ( 1 . _ 4 _ 1 4 ) ) /\ ( ( 1 . _ 1 _ 6 7 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) ) -> ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) )
314	180 311 313	mp2an	|- ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 )
315	50 314	pm3.2i	|- ( 0 <_ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) /\ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) )
316	44 315	pm3.2i	|- ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR /\ ( 1 . _ 6 _ 5 1 ) e. RR ) /\ ( 0 <_ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) /\ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) ) )
317		4re	|- 4 e. RR
318		2re	|- 2 e. RR
319		3re	|- 3 e. RR
320	34 319	pm3.2i	|- ( 6 e. RR /\ 3 e. RR )
321		dp2cl	|- ( ( 6 e. RR /\ 3 e. RR ) -> _ 6 3 e. RR )
322	320 321	ax-mp	|- _ 6 3 e. RR
323	318 322	pm3.2i	|- ( 2 e. RR /\ _ 6 3 e. RR )
324		dp2cl	|- ( ( 2 e. RR /\ _ 6 3 e. RR ) -> _ 2 _ 6 3 e. RR )
325	323 324	ax-mp	|- _ 2 _ 6 3 e. RR
326	317 325	pm3.2i	|- ( 4 e. RR /\ _ 2 _ 6 3 e. RR )
327		dp2cl	|- ( ( 4 e. RR /\ _ 2 _ 6 3 e. RR ) -> _ 4 _ 2 _ 6 3 e. RR )
328	326 327	ax-mp	|- _ 4 _ 2 _ 6 3 e. RR
329		dpcl	|- ( ( 1 e. NN0 /\ _ 4 _ 2 _ 6 3 e. RR ) -> ( 1 . _ 4 _ 2 _ 6 3 ) e. RR )
330	1 328 329	mp2an	|- ( 1 . _ 4 _ 2 _ 6 3 ) e. RR
331	84 319	pm3.2i	|- ( 8 e. RR /\ 3 e. RR )
332		dp2cl	|- ( ( 8 e. RR /\ 3 e. RR ) -> _ 8 3 e. RR )
333	331 332	ax-mp	|- _ 8 3 e. RR
334	84 333	pm3.2i	|- ( 8 e. RR /\ _ 8 3 e. RR )
335		dp2cl	|- ( ( 8 e. RR /\ _ 8 3 e. RR ) -> _ 8 _ 8 3 e. RR )
336	334 335	ax-mp	|- _ 8 _ 8 3 e. RR
337	319 336	pm3.2i	|- ( 3 e. RR /\ _ 8 _ 8 3 e. RR )
338		dp2cl	|- ( ( 3 e. RR /\ _ 8 _ 8 3 e. RR ) -> _ 3 _ 8 _ 8 3 e. RR )
339	337 338	ax-mp	|- _ 3 _ 8 _ 8 3 e. RR
340	2 339	pm3.2i	|- ( 0 e. RR /\ _ 3 _ 8 _ 8 3 e. RR )
341		dp2cl	|- ( ( 0 e. RR /\ _ 3 _ 8 _ 8 3 e. RR ) -> _ 0 _ 3 _ 8 _ 8 3 e. RR )
342	340 341	ax-mp	|- _ 0 _ 3 _ 8 _ 8 3 e. RR
343		dpcl	|- ( ( 1 e. NN0 /\ _ 0 _ 3 _ 8 _ 8 3 e. RR ) -> ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR )
344	1 342 343	mp2an	|- ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR
345	330 344	remulcli	|- ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) e. RR
346	317 333	pm3.2i	|- ( 4 e. RR /\ _ 8 3 e. RR )
347		dp2cl	|- ( ( 4 e. RR /\ _ 8 3 e. RR ) -> _ 4 _ 8 3 e. RR )
348	346 347	ax-mp	|- _ 4 _ 8 3 e. RR
349		dpcl	|- ( ( 1 e. NN0 /\ _ 4 _ 8 3 e. RR ) -> ( 1 . _ 4 _ 8 3 ) e. RR )
350	1 348 349	mp2an	|- ( 1 . _ 4 _ 8 3 ) e. RR
351	345 350	pm3.2i	|- ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) e. RR /\ ( 1 . _ 4 _ 8 3 ) e. RR )
352		3rp	|- 3 e. RR+
353	98 352	rpdp2cl	|- _ 6 3 e. RR+
354	181 353	rpdp2cl	|- _ 2 _ 6 3 e. RR+
355	24 354	rpdp2cl	|- _ 4 _ 2 _ 6 3 e. RR+
356	1 355	rpdpcl	|- ( 1 . _ 4 _ 2 _ 6 3 ) e. RR+
357		rpge0	|- ( ( 1 . _ 4 _ 2 _ 6 3 ) e. RR+ -> 0 <_ ( 1 . _ 4 _ 2 _ 6 3 ) )
358	356 357	ax-mp	|- 0 <_ ( 1 . _ 4 _ 2 _ 6 3 )
359	73 352	rpdp2cl	|- _ 8 3 e. RR+
360	73 359	rpdp2cl	|- _ 8 _ 8 3 e. RR+
361	182 360	rpdp2cl	|- _ 3 _ 8 _ 8 3 e. RR+
362	51 361	rpdp2cl	|- _ 0 _ 3 _ 8 _ 8 3 e. RR+
363	1 362	rpdpcl	|- ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR+
364		rpge0	|- ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR+ -> 0 <_ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) )
365	363 364	ax-mp	|- 0 <_ ( 1 . _ 0 _ 3 _ 8 _ 8 3 )
366	330 344	mulge0i	|- ( ( 0 <_ ( 1 . _ 4 _ 2 _ 6 3 ) /\ 0 <_ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) -> 0 <_ ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) )
367	358 365 366	mp2an	|- 0 <_ ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) )
368	318 3	pm3.2i	|- ( 2 e. RR /\ 7 e. RR )
369		dp2cl	|- ( ( 2 e. RR /\ 7 e. RR ) -> _ 2 7 e. RR )
370	368 369	ax-mp	|- _ 2 7 e. RR
371	317 370	pm3.2i	|- ( 4 e. RR /\ _ 2 7 e. RR )
372		dp2cl	|- ( ( 4 e. RR /\ _ 2 7 e. RR ) -> _ 4 _ 2 7 e. RR )
373	371 372	ax-mp	|- _ 4 _ 2 7 e. RR
374		dpcl	|- ( ( 1 e. NN0 /\ _ 4 _ 2 7 e. RR ) -> ( 1 . _ 4 _ 2 7 ) e. RR )
375	1 373 374	mp2an	|- ( 1 . _ 4 _ 2 7 ) e. RR
376	330 375	pm3.2i	|- ( ( 1 . _ 4 _ 2 _ 6 3 ) e. RR /\ ( 1 . _ 4 _ 2 7 ) e. RR )
377		7nn	|- 7 e. NN
378		nnrp	|- ( 7 e. NN -> 7 e. RR+ )
379	377 378	ax-mp	|- 7 e. RR+
380	181 379	rpdp2cl	|- _ 2 7 e. RR+
381	24 380	rpdp2cl	|- _ 4 _ 2 7 e. RR+
382	98 352 184 140	dp2ltsuc	|- _ 6 3 < 7
383	181 353 379 382	dp2lt	|- _ 2 _ 6 3 < _ 2 7
384	24 354 380 383	dp2lt	|- _ 4 _ 2 _ 6 3 < _ 4 _ 2 7
385	1 355 381 384	dplt	|- ( 1 . _ 4 _ 2 _ 6 3 ) < ( 1 . _ 4 _ 2 7 )
386	358 385	pm3.2i	|- ( 0 <_ ( 1 . _ 4 _ 2 _ 6 3 ) /\ ( 1 . _ 4 _ 2 _ 6 3 ) < ( 1 . _ 4 _ 2 7 ) )
387	376 386	pm3.2i	|- ( ( ( 1 . _ 4 _ 2 _ 6 3 ) e. RR /\ ( 1 . _ 4 _ 2 7 ) e. RR ) /\ ( 0 <_ ( 1 . _ 4 _ 2 _ 6 3 ) /\ ( 1 . _ 4 _ 2 _ 6 3 ) < ( 1 . _ 4 _ 2 7 ) ) )
388	319 4	pm3.2i	|- ( 3 e. RR /\ 9 e. RR )
389		dp2cl	|- ( ( 3 e. RR /\ 9 e. RR ) -> _ 3 9 e. RR )
390	388 389	ax-mp	|- _ 3 9 e. RR
391	2 390	pm3.2i	|- ( 0 e. RR /\ _ 3 9 e. RR )
392		dp2cl	|- ( ( 0 e. RR /\ _ 3 9 e. RR ) -> _ 0 _ 3 9 e. RR )
393	391 392	ax-mp	|- _ 0 _ 3 9 e. RR
394		dpcl	|- ( ( 1 e. NN0 /\ _ 0 _ 3 9 e. RR ) -> ( 1 . _ 0 _ 3 9 ) e. RR )
395	1 393 394	mp2an	|- ( 1 . _ 0 _ 3 9 ) e. RR
396	344 395	pm3.2i	|- ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR /\ ( 1 . _ 0 _ 3 9 ) e. RR )
397		9nn	|- 9 e. NN
398		nnrp	|- ( 9 e. NN -> 9 e. RR+ )
399	397 398	ax-mp	|- 9 e. RR+
400	182 399	rpdp2cl	|- _ 3 9 e. RR+
401	51 400	rpdp2cl	|- _ 0 _ 3 9 e. RR+
402	73 352 185 184	dp2lt10	|- _ 8 3 < ; 1 0
403	73 359 402 160	dp2ltsuc	|- _ 8 _ 8 3 < 9
404	182 360 399 403	dp2lt	|- _ 3 _ 8 _ 8 3 < _ 3 9
405	51 361 400 404	dp2lt	|- _ 0 _ 3 _ 8 _ 8 3 < _ 0 _ 3 9
406	1 362 401 405	dplt	|- ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) < ( 1 . _ 0 _ 3 9 )
407	365 406	pm3.2i	|- ( 0 <_ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) /\ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) < ( 1 . _ 0 _ 3 9 ) )
408	396 407	pm3.2i	|- ( ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR /\ ( 1 . _ 0 _ 3 9 ) e. RR ) /\ ( 0 <_ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) /\ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) < ( 1 . _ 0 _ 3 9 ) ) )
409		ltmul12a	|- ( ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) e. RR /\ ( 1 . _ 4 _ 2 7 ) e. RR ) /\ ( 0 <_ ( 1 . _ 4 _ 2 _ 6 3 ) /\ ( 1 . _ 4 _ 2 _ 6 3 ) < ( 1 . _ 4 _ 2 7 ) ) ) /\ ( ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR /\ ( 1 . _ 0 _ 3 9 ) e. RR ) /\ ( 0 <_ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) /\ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) < ( 1 . _ 0 _ 3 9 ) ) ) ) -> ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( ( 1 . _ 4 _ 2 7 ) x. ( 1 . _ 0 _ 3 9 ) ) )
410	387 408 409	mp2an	|- ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( ( 1 . _ 4 _ 2 7 ) x. ( 1 . _ 0 _ 3 9 ) )
411		6lt10	|- 6 < ; 1 0
412	73 1	deccl	|- ; 8 1 e. NN0
413		eqid	|- ; ; 8 1 6 = ; ; 8 1 6
414		eqid	|- ; 1 0 = ; 1 0
415		eqid	|- ; 8 1 = ; 8 1
416	73 1 269 415	decsuc	|- ( ; 8 1 + 1 ) = ; 8 2
417	73	dec0h	|- 8 = ; 0 8
418	417	deceq1i	|- ; 8 2 = ; ; 0 8 2
419	416 418	eqtri	|- ( ; 8 1 + 1 ) = ; ; 0 8 2
420	110	addridi	|- ( 6 + 0 ) = 6
421	412 98 1 51 413 414 419 420	decadd	|- ( ; ; 8 1 6 + ; 1 0 ) = ; ; ; 0 8 2 6
422	138	mul01i	|- ( 1 x. 0 ) = 0
423	113	mul01i	|- ( 4 x. 0 ) = 0
424	51	dec0h	|- 0 = ; 0 0
425	423 424	eqtri	|- ( 4 x. 0 ) = ; 0 0
426	113	addridi	|- ( 4 + 0 ) = 4
427	426	oveq1i	|- ( ( 4 + 0 ) + 0 ) = ( 4 + 0 )
428	427 426 205	3eqtri	|- ( ( 4 + 0 ) + 0 ) = ; 0 4
429	1 24 1 51 51 51 24 51 116 422 203 425 428 192	dpmul	|- ( ( 1 . 4 ) x. ( 1 . 0 ) ) = ( 1 . _ 4 0 )
430		2t3e6	|- ( 2 x. 3 ) = 6
431		9t2e18	|- ( 9 x. 2 ) = ; 1 8
432	196 197 431	mulcomli	|- ( 2 x. 9 ) = ; 1 8
433		7t3e21	|- ( 7 x. 3 ) = ; 2 1
434		9t7e63	|- ( 9 x. 7 ) = ; 6 3
435	196 217 434	mulcomli	|- ( 7 x. 9 ) = ; 6 3
436		eqid	|- ; 2 1 = ; 2 1
437		eqid	|- ; 1 8 = ; 1 8
438	159 160	eqtri	|- ( 1 + 8 ) = 9
439	181 1 1 73 436 437 224 438	decadd	|- ( ; 2 1 + ; 1 8 ) = ; 3 9
440	439	oveq1i	|- ( ( ; 2 1 + ; 1 8 ) + 6 ) = ( ; 3 9 + 6 )
441		eqid	|- ; 3 9 = ; 3 9
442		3p1e4	|- ( 3 + 1 ) = 4
443		9p6e15	|- ( 9 + 6 ) = ; 1 5
444	182 53 98 441 442 54 443	decaddci	|- ( ; 3 9 + 6 ) = ; 4 5
445	440 444	eqtri	|- ( ( ; 2 1 + ; 1 8 ) + 6 ) = ; 4 5
446		6p4e10	|- ( 6 + 4 ) = ; 1 0
447	181 52 182 53 98 24 54 182 430 432 433 435 445 446	dpmul	|- ( ( 2 . 7 ) x. ( 3 . 9 ) ) = ( ; 1 0 . _ 5 3 )
448	1 24	deccl	|- ; 1 4 e. NN0
449	448 51	deccl	|- ; ; 1 4 0 e. NN0
450	417 73	eqeltrri	|- ; 0 8 e. NN0
451		eqid	|- ; ; ; 1 4 0 1 = ; ; ; 1 4 0 1
452		eqid	|- ; ; 0 8 2 = ; ; 0 8 2
453		eqid	|- ; ; 1 4 0 = ; ; 1 4 0
454	417 158	eqeltrri	|- ; 0 8 e. CC
455		0cn	|- 0 e. CC
456	417	oveq1i	|- ( 8 + 0 ) = ( ; 0 8 + 0 )
457	158	addridi	|- ( 8 + 0 ) = 8
458	456 457	eqtr3i	|- ( ; 0 8 + 0 ) = 8
459	454 455 458	addcomli	|- ( 0 + ; 0 8 ) = 8
460	448 51 450 453 459	decaddi	|- ( ; ; 1 4 0 + ; 0 8 ) = ; ; 1 4 8
461	449 1 450 181 451 452 460 230	decadd	|- ( ; ; ; 1 4 0 1 + ; ; 0 8 2 ) = ; ; ; 1 4 8 3
462		4t4e16	|- ( 4 x. 4 ) = ; 1 6
463		9t4e36	|- ( 9 x. 4 ) = ; 3 6
464	196 113 463	mulcomli	|- ( 4 x. 9 ) = ; 3 6
465	196	mulridi	|- ( 9 x. 1 ) = 9
466	465 188	eqtri	|- ( 9 x. 1 ) = ; 0 9
467	196 138 466	mulcomli	|- ( 1 x. 9 ) = ; 0 9
468	182 98	deccl	|- ; 3 6 e. NN0
469	468	nn0cni	|- ; 3 6 e. CC
470		eqid	|- ; 3 6 = ; 3 6
471	182 98 24 470 442 51 446	decaddci	|- ( ; 3 6 + 4 ) = ; 4 0
472	469 113 471	addcomli	|- ( 4 + ; 3 6 ) = ; 4 0
473	472	oveq1i	|- ( ( 4 + ; 3 6 ) + 0 ) = ( ; 4 0 + 0 )
474	24 51	deccl	|- ; 4 0 e. NN0
475	474	nn0cni	|- ; 4 0 e. CC
476	475	addridi	|- ( ; 4 0 + 0 ) = ; 4 0
477	473 476	eqtri	|- ( ( 4 + ; 3 6 ) + 0 ) = ; 4 0
478	1 98 24 135 269 51 446	decaddci	|- ( ; 1 6 + 4 ) = ; 2 0
479	24 1 24 53 51 24 51 53 462 464 204 467 477 478	dpmul	|- ( ( 4 . 1 ) x. ( 4 . 9 ) ) = ( ; 2 0 . _ 0 9 )
480		eqid	|- ; 2 7 = ; 2 7
481	230	oveq1i	|- ( ( 1 + 2 ) + 1 ) = ( 3 + 1 )
482	481 442	eqtri	|- ( ( 1 + 2 ) + 1 ) = 4
483	1 24 181 52 268 480 482 1 225	decaddc	|- ( ; 1 4 + ; 2 7 ) = ; 4 1
484	1 24 181 52 24 1 483	dpadd	|- ( ( 1 . 4 ) + ( 2 . 7 ) ) = ( 4 . 1 )
485		3cn	|- 3 e. CC
486	485 138 442	addcomli	|- ( 1 + 3 ) = 4
487	196	addlidi	|- ( 0 + 9 ) = 9
488	1 51 182 53 414 441 486 487	decadd	|- ( ; 1 0 + ; 3 9 ) = ; 4 9
489	1 51 182 53 24 53 488	dpadd	|- ( ( 1 . 0 ) + ( 3 . 9 ) ) = ( 4 . 9 )
490	484 489	oveq12i	|- ( ( ( 1 . 4 ) + ( 2 . 7 ) ) x. ( ( 1 . 0 ) + ( 3 . 9 ) ) ) = ( ( 4 . 1 ) x. ( 4 . 9 ) )
491	1 24 73 1 268 415 438 210	decadd	|- ( ; 1 4 + ; 8 1 ) = ; 9 5
492	448 51 412 98 453 413 491 111	decadd	|- ( ; ; 1 4 0 + ; ; 8 1 6 ) = ; ; 9 5 6
493	1 24 51 73 1 53 98 54 98 492	dpadd3	|- ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) = ( 9 . _ 5 6 )
494	493	oveq1i	|- ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) ) = ( ( 9 . _ 5 6 ) + ( ; 1 0 . _ 5 3 ) )
495	181 51	deccl	|- ; 2 0 e. NN0
496	53 54	deccl	|- ; 9 5 e. NN0
497	130 54	deccl	|- ; ; 1 0 5 e. NN0
498		eqid	|- ; ; 9 5 6 = ; ; 9 5 6
499		eqid	|- ; ; ; 1 0 5 3 = ; ; ; 1 0 5 3
500		eqid	|- ; 9 5 = ; 9 5
501		eqid	|- ; ; 1 0 5 = ; ; 1 0 5
502		dec10p	|- ( ; 1 0 + 9 ) = ; 1 9
503	283 196 502	addcomli	|- ( 9 + ; 1 0 ) = ; 1 9
504	503	oveq1i	|- ( ( 9 + ; 1 0 ) + 1 ) = ( ; 1 9 + 1 )
505		eqid	|- ; 1 9 = ; 1 9
506	1 53 1 505 269 51 194	decaddci	|- ( ; 1 9 + 1 ) = ; 2 0
507	504 506	eqtri	|- ( ( 9 + ; 1 0 ) + 1 ) = ; 2 0
508		5p5e10	|- ( 5 + 5 ) = ; 1 0
509	53 54 130 54 500 501 507 51 508	decaddc	|- ( ; 9 5 + ; ; 1 0 5 ) = ; ; 2 0 0
510	496 98 497 182 498 499 509 233	decadd	|- ( ; ; 9 5 6 + ; ; ; 1 0 5 3 ) = ; ; ; 2 0 0 9
511	53 54 98 130 54 495 182 51 53 510	dpadd3	|- ( ( 9 . _ 5 6 ) + ( ; 1 0 . _ 5 3 ) ) = ( ; 2 0 . _ 0 9 )
512	494 511	eqtri	|- ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) ) = ( ; 2 0 . _ 0 9 )
513	479 490 512	3eqtr4i	|- ( ( ( 1 . 4 ) + ( 2 . 7 ) ) x. ( ( 1 . 0 ) + ( 3 . 9 ) ) ) = ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) )
514	1 24 181 52 1 182 24 51 51 53 1 73 1 98 130 54 182 51 73 181 98 1 24 73 182 411 67 184 421 429 447 461 513	dpmul4	|- ( ( 1 . _ 4 _ 2 7 ) x. ( 1 . _ 0 _ 3 9 ) ) < ( 1 . _ 4 _ 8 3 )
515	375 395	remulcli	|- ( ( 1 . _ 4 _ 2 7 ) x. ( 1 . _ 0 _ 3 9 ) ) e. RR
516	345 515 350	lttri	|- ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( ( 1 . _ 4 _ 2 7 ) x. ( 1 . _ 0 _ 3 9 ) ) /\ ( ( 1 . _ 4 _ 2 7 ) x. ( 1 . _ 0 _ 3 9 ) ) < ( 1 . _ 4 _ 8 3 ) ) -> ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) )
517	410 514 516	mp2an	|- ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 )
518	367 517	pm3.2i	|- ( 0 <_ ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) /\ ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) )
519	351 518	pm3.2i	|- ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) e. RR /\ ( 1 . _ 4 _ 8 3 ) e. RR ) /\ ( 0 <_ ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) /\ ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) ) )
520		ltmul12a	|- ( ( ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR /\ ( 1 . _ 6 _ 5 1 ) e. RR ) /\ ( 0 <_ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) /\ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) ) ) /\ ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) e. RR /\ ( 1 . _ 4 _ 8 3 ) e. RR ) /\ ( 0 <_ ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) /\ ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) ) ) ) -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( ( 1 . _ 6 _ 5 1 ) x. ( 1 . _ 4 _ 8 3 ) ) )
521	316 519 520	mp2an	|- ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( ( 1 . _ 6 _ 5 1 ) x. ( 1 . _ 4 _ 8 3 ) )
522	24 181	deccl	|- ; 4 2 e. NN0
523	495 24	deccl	|- ; ; 2 0 4 e. NN0
524		eqid	|- ; ; ; 2 0 4 2 = ; ; ; 2 0 4 2
525		eqid	|- ; 4 2 = ; 4 2
526		eqid	|- ; ; 2 0 4 = ; ; 2 0 4
527	495 24 24 526 277	decaddi	|- ( ; ; 2 0 4 + 4 ) = ; ; 2 0 8
528		2p2e4	|- ( 2 + 2 ) = 4
529	523 181 24 181 524 525 527 528	decadd	|- ( ; ; ; 2 0 4 2 + ; 4 2 ) = ; ; ; 2 0 8 4
530	446	oveq1i	|- ( ( 6 + 4 ) + 2 ) = ( ; 1 0 + 2 )
531		dec10p	|- ( ; 1 0 + 2 ) = ; 1 2
532	530 531	eqtri	|- ( ( 6 + 4 ) + 2 ) = ; 1 2
533	1 98 1 24 181 1 181 24 116 204 215 216 532 269	dpmul	|- ( ( 1 . 6 ) x. ( 1 . 4 ) ) = ( 2 . _ 2 4 )
534		8t5e40	|- ( 8 x. 5 ) = ; 4 0
535	158 256 534	mulcomli	|- ( 5 x. 8 ) = ; 4 0
536		5t3e15	|- ( 5 x. 3 ) = ; 1 5
537	158	mullidi	|- ( 1 x. 8 ) = 8
538	485	mullidi	|- ( 1 x. 3 ) = 3
539	182	dec0h	|- 3 = ; 0 3
540	538 539	eqtri	|- ( 1 x. 3 ) = ; 0 3
541	235	nn0cni	|- ; 1 5 e. CC
542		8p5e13	|- ( 8 + 5 ) = ; 1 3
543	158 256 542	addcomli	|- ( 5 + 8 ) = ; 1 3
544	1 54 73 245 269 182 543	decaddci	|- ( ; 1 5 + 8 ) = ; 2 3
545	541 158 544	addcomli	|- ( 8 + ; 1 5 ) = ; 2 3
546	545	oveq1i	|- ( ( 8 + ; 1 5 ) + 0 ) = ( ; 2 3 + 0 )
547	181 182	deccl	|- ; 2 3 e. NN0
548	547	nn0cni	|- ; 2 3 e. CC
549	548	addridi	|- ( ; 2 3 + 0 ) = ; 2 3
550	546 549	eqtri	|- ( ( 8 + ; 1 5 ) + 0 ) = ; 2 3
551		eqid	|- ; 4 0 = ; 4 0
552	197	addlidi	|- ( 0 + 2 ) = 2
553	24 51 181 551 552	decaddi	|- ( ; 4 0 + 2 ) = ; 4 2
554	54 1 73 182 51 181 182 182 535 536 537 540 550 553	dpmul	|- ( ( 5 . 1 ) x. ( 8 . 3 ) ) = ( ; 4 2 . _ 3 3 )
555	181 181	deccl	|- ; 2 2 e. NN0
556	555 24	deccl	|- ; ; 2 2 4 e. NN0
557		eqid	|- ; ; ; 2 2 4 1 = ; ; ; 2 2 4 1
558		eqid	|- ; ; 2 0 8 = ; ; 2 0 8
559		eqid	|- ; ; 2 2 4 = ; ; 2 2 4
560		eqid	|- ; 2 0 = ; 2 0
561		eqid	|- ; 2 2 = ; 2 2
562	181 181 181 561 528	decaddi	|- ( ; 2 2 + 2 ) = ; 2 4
563	555 24 181 51 559 560 562 426	decadd	|- ( ; ; 2 2 4 + ; 2 0 ) = ; ; 2 4 4
564	556 1 495 73 557 558 563 438	decadd	|- ( ; ; ; 2 2 4 1 + ; ; 2 0 8 ) = ; ; ; 2 4 4 9
565	555 98	deccl	|- ; ; 2 2 6 e. NN0
566	522 182	deccl	|- ; ; 4 2 3 e. NN0
567		eqid	|- ; ; ; 2 2 6 6 = ; ; ; 2 2 6 6
568		eqid	|- ; ; ; 4 2 3 3 = ; ; ; 4 2 3 3
569		eqid	|- ; ; 2 2 6 = ; ; 2 2 6
570		eqid	|- ; ; 4 2 3 = ; ; 4 2 3
571	113 197 289	addcomli	|- ( 2 + 4 ) = 6
572	181 181 24 181 561 525 571 528	decadd	|- ( ; 2 2 + ; 4 2 ) = ; 6 4
573	555 98 522 182 569 570 572 233	decadd	|- ( ; ; 2 2 6 + ; ; 4 2 3 ) = ; ; 6 4 9
574	565 98 566 182 567 568 573 233	decadd	|- ( ; ; ; 2 2 6 6 + ; ; ; 4 2 3 3 ) = ; ; ; 6 4 9 9
575	555 98 98 522 182 100 182 53 53 574	dpadd3	|- ( ( ; 2 2 . _ 6 6 ) + ( ; 4 2 . _ 3 3 ) ) = ( ; 6 4 . _ 9 9 )
576	495	nn0cni	|- ; 2 0 e. CC
577	181 51 181 560 552	decaddi	|- ( ; 2 0 + 2 ) = ; 2 2
578	576 197 577	addcomli	|- ( 2 + ; 2 0 ) = ; 2 2
579	181 181 495 24 561 526 578 571	decadd	|- ( ; 2 2 + ; ; 2 0 4 ) = ; ; 2 2 6
580	555 24 523 181 559 524 579 289	decadd	|- ( ; ; 2 2 4 + ; ; ; 2 0 4 2 ) = ; ; ; 2 2 6 6
581	181 181 24 495 24 555 181 98 98 580	dpadd3	|- ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) = ( ; 2 2 . _ 6 6 )
582	581	oveq1i	|- ( ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) + ( ; 4 2 . _ 3 3 ) ) = ( ( ; 2 2 . _ 6 6 ) + ( ; 4 2 . _ 3 3 ) )
583		eqid	|- ; 5 1 = ; 5 1
584	1 98 54 1 135 583 257 140	decadd	|- ( ; 1 6 + ; 5 1 ) = ; 6 7
585	1 98 54 1 98 52 584	dpadd	|- ( ( 1 . 6 ) + ( 5 . 1 ) ) = ( 6 . 7 )
586		eqid	|- ; 8 3 = ; 8 3
587	1 24 73 182 268 586 438 302	decadd	|- ( ; 1 4 + ; 8 3 ) = ; 9 7
588	1 24 73 182 53 52 587	dpadd	|- ( ( 1 . 4 ) + ( 8 . 3 ) ) = ( 9 . 7 )
589	585 588	oveq12i	|- ( ( ( 1 . 6 ) + ( 5 . 1 ) ) x. ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ( 6 . 7 ) x. ( 9 . 7 ) )
590		9t6e54	|- ( 9 x. 6 ) = ; 5 4
591	196 110 590	mulcomli	|- ( 6 x. 9 ) = ; 5 4
592		7t6e42	|- ( 7 x. 6 ) = ; 4 2
593	217 110 592	mulcomli	|- ( 6 x. 7 ) = ; 4 2
594		7t7e49	|- ( 7 x. 7 ) = ; 4 9
595		eqid	|- ; 6 3 = ; 6 3
596		3p2e5	|- ( 3 + 2 ) = 5
597	98 182 24 181 595 525 446 596	decadd	|- ( ; 6 3 + ; 4 2 ) = ; ; 1 0 5
598	597	oveq1i	|- ( ( ; 6 3 + ; 4 2 ) + 4 ) = ( ; ; 1 0 5 + 4 )
599		5p4e9	|- ( 5 + 4 ) = 9
600	130 54 24 501 599	decaddi	|- ( ; ; 1 0 5 + 4 ) = ; ; 1 0 9
601	598 600	eqtri	|- ( ( ; 6 3 + ; 4 2 ) + 4 ) = ; ; 1 0 9
602		eqid	|- ; 5 4 = ; 5 4
603	54 24 1 51 602 414 246 426	decadd	|- ( ; 5 4 + ; 1 0 ) = ; 6 4
604	98 52 53 52 24 130 53 53 591 593 435 594 601 603	dpmul	|- ( ( 6 . 7 ) x. ( 9 . 7 ) ) = ( ; 6 4 . _ 9 9 )
605	589 604	eqtri	|- ( ( ( 1 . 6 ) + ( 5 . 1 ) ) x. ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ; 6 4 . _ 9 9 )
606	575 582 605	3eqtr4ri	|- ( ( ( 1 . 6 ) + ( 5 . 1 ) ) x. ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) + ( ; 4 2 . _ 3 3 ) )
607	1 98 54 1 1 73 181 24 24 182 181 495 24 181 522 182 182 181 51 73 24 181 24 24 53 101 184 184 529 533 554 564 606	dpmul4	|- ( ( 1 . _ 6 _ 5 1 ) x. ( 1 . _ 4 _ 8 3 ) ) < ( 2 . _ 4 _ 4 9 )
608	33 345	remulcli	|- ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) e. RR
609	43 350	remulcli	|- ( ( 1 . _ 6 _ 5 1 ) x. ( 1 . _ 4 _ 8 3 ) ) e. RR
610	24 399	rpdp2cl	|- _ 4 9 e. RR+
611	24 610	rpdp2cl	|- _ 4 _ 4 9 e. RR+
612	181 611	rpdpcl	|- ( 2 . _ 4 _ 4 9 ) e. RR+
613		rpre	|- ( ( 2 . _ 4 _ 4 9 ) e. RR+ -> ( 2 . _ 4 _ 4 9 ) e. RR )
614	612 613	ax-mp	|- ( 2 . _ 4 _ 4 9 ) e. RR
615	608 609 614	lttri	|- ( ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( ( 1 . _ 6 _ 5 1 ) x. ( 1 . _ 4 _ 8 3 ) ) /\ ( ( 1 . _ 6 _ 5 1 ) x. ( 1 . _ 4 _ 8 3 ) ) < ( 2 . _ 4 _ 4 9 ) ) -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( 2 . _ 4 _ 4 9 ) )
616	521 607 615	mp2an	|- ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( 2 . _ 4 _ 4 9 )
617		3pos	|- 0 < 3
618	608 614 319	ltmul2i	|- ( 0 < 3 -> ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( 2 . _ 4 _ 4 9 ) <-> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 3 x. ( 2 . _ 4 _ 4 9 ) ) ) )
619	617 618	ax-mp	|- ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( 2 . _ 4 _ 4 9 ) <-> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 3 x. ( 2 . _ 4 _ 4 9 ) ) )
620	616 619	mpbi	|- ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 3 x. ( 2 . _ 4 _ 4 9 ) )
621	119	dp2eq2i	|- _ 0 _ 0 0 = _ 0 0
622	621 119	eqtri	|- _ 0 _ 0 0 = 0
623	622	oveq2i	|- ( 3 . _ 0 _ 0 0 ) = ( 3 . 0 )
624	182	dp0u	|- ( 3 . 0 ) = 3
625	623 624	eqtr2i	|- 3 = ( 3 . _ 0 _ 0 0 )
626	625	oveq1i	|- ( 3 x. ( 2 . _ 4 _ 4 9 ) ) = ( ( 3 . _ 0 _ 0 0 ) x. ( 2 . _ 4 _ 4 9 ) )
627	448 52	deccl	|- ; ; 1 4 7 e. NN0
628	627 51	deccl	|- ; ; ; 1 4 7 0 e. NN0
629	628	nn0cni	|- ; ; ; 1 4 7 0 e. CC
630	629	addridi	|- ( ; ; ; 1 4 7 0 + 0 ) = ; ; ; 1 4 7 0
631		3t2e6	|- ( 3 x. 2 ) = 6
632		4t3e12	|- ( 4 x. 3 ) = ; 1 2
633	113 485 632	mulcomli	|- ( 3 x. 4 ) = ; 1 2
634	197	mul02i	|- ( 0 x. 2 ) = 0
635	113 455 425	mulcomli	|- ( 0 x. 4 ) = ; 0 0
636	51 51 1 181 424 300 153 552	decadd	|- ( 0 + ; 1 2 ) = ; 1 2
637	636	oveq1i	|- ( ( 0 + ; 1 2 ) + 0 ) = ( ; 1 2 + 0 )
638	281	nn0cni	|- ; 1 2 e. CC
639	638	addridi	|- ( ; 1 2 + 0 ) = ; 1 2
640	637 639	eqtri	|- ( ( 0 + ; 1 2 ) + 0 ) = ; 1 2
641	182 51 181 24 51 1 181 51 631 633 634 635 640 140	dpmul	|- ( ( 3 . 0 ) x. ( 2 . 4 ) ) = ( 7 . _ 2 0 )
642	51	dp0u	|- ( 0 . 0 ) = 0
643	642	oveq1i	|- ( ( 0 . 0 ) x. ( 4 . 9 ) ) = ( 0 x. ( 4 . 9 ) )
644		dpcl	|- ( ( 4 e. NN0 /\ 9 e. RR ) -> ( 4 . 9 ) e. RR )
645	24 4 644	mp2an	|- ( 4 . 9 ) e. RR
646	645	recni	|- ( 4 . 9 ) e. CC
647	646	mul02i	|- ( 0 x. ( 4 . 9 ) ) = 0
648	643 647	eqtri	|- ( ( 0 . 0 ) x. ( 4 . 9 ) ) = 0
649	119	oveq2i	|- ( 0 . _ 0 0 ) = ( 0 . 0 )
650	649 642	eqtri	|- ( 0 . _ 0 0 ) = 0
651	648 650	eqtr4i	|- ( ( 0 . 0 ) x. ( 4 . 9 ) ) = ( 0 . _ 0 0 )
652	52 181	deccl	|- ; 7 2 e. NN0
653	652 51	deccl	|- ; ; 7 2 0 e. NN0
654		eqid	|- ; ; ; 7 2 0 1 = ; ; ; 7 2 0 1
655		eqid	|- ; ; 1 4 7 = ; ; 1 4 7
656		eqid	|- ; ; 7 2 0 = ; ; 7 2 0
657	52 181 224 263	decsuc	|- ( ; 7 2 + 1 ) = ; 7 3
658	652 51 1 24 656 268 657 114	decadd	|- ( ; ; 7 2 0 + ; 1 4 ) = ; ; 7 3 4
659	653 1 448 52 654 655 658 274	decadd	|- ( ; ; ; 7 2 0 1 + ; ; 1 4 7 ) = ; ; ; 7 3 4 8
660	642	oveq2i	|- ( ( 3 . 0 ) + ( 0 . 0 ) ) = ( ( 3 . 0 ) + 0 )
661	624 485	eqeltri	|- ( 3 . 0 ) e. CC
662	661	addridi	|- ( ( 3 . 0 ) + 0 ) = ( 3 . 0 )
663	660 662	eqtri	|- ( ( 3 . 0 ) + ( 0 . 0 ) ) = ( 3 . 0 )
664		eqid	|- ; 4 9 = ; 4 9
665	571	oveq1i	|- ( ( 2 + 4 ) + 1 ) = ( 6 + 1 )
666	665 140	eqtri	|- ( ( 2 + 4 ) + 1 ) = 7
667		9p4e13	|- ( 9 + 4 ) = ; 1 3
668	196 113 667	addcomli	|- ( 4 + 9 ) = ; 1 3
669	181 24 24 53 223 664 666 182 668	decaddc	|- ( ; 2 4 + ; 4 9 ) = ; 7 3
670	181 24 24 53 52 182 669	dpadd	|- ( ( 2 . 4 ) + ( 4 . 9 ) ) = ( 7 . 3 )
671	663 670	oveq12i	|- ( ( ( 3 . 0 ) + ( 0 . 0 ) ) x. ( ( 2 . 4 ) + ( 4 . 9 ) ) ) = ( ( 3 . 0 ) x. ( 7 . 3 ) )
672	217 485 433	mulcomli	|- ( 3 x. 7 ) = ; 2 1
673		3t3e9	|- ( 3 x. 3 ) = 9
674	217	mul01i	|- ( 7 x. 0 ) = 0
675	217 455 674	mulcomli	|- ( 0 x. 7 ) = 0
676	485	mul01i	|- ( 3 x. 0 ) = 0
677	676 424	eqtri	|- ( 3 x. 0 ) = ; 0 0
678	485 455 677	mulcomli	|- ( 0 x. 3 ) = ; 0 0
679	196	addridi	|- ( 9 + 0 ) = 9
680	679	oveq1i	|- ( ( 9 + 0 ) + 0 ) = ( 9 + 0 )
681	680 679 188	3eqtri	|- ( ( 9 + 0 ) + 0 ) = ; 0 9
682	196 455	addcomi	|- ( 9 + 0 ) = ( 0 + 9 )
683	682	oveq1i	|- ( ( 9 + 0 ) + 0 ) = ( ( 0 + 9 ) + 0 )
684	683	eqeq1i	|- ( ( ( 9 + 0 ) + 0 ) = ; 0 9 <-> ( ( 0 + 9 ) + 0 ) = ; 0 9 )
685	681 684	mpbi	|- ( ( 0 + 9 ) + 0 ) = ; 0 9
686	181 1 51 436 192	decaddi	|- ( ; 2 1 + 0 ) = ; 2 1
687	182 51 52 182 51 51 53 51 672 673 675 678 685 686	dpmul	|- ( ( 3 . 0 ) x. ( 7 . 3 ) ) = ( ; 2 1 . _ 9 0 )
688	671 687	eqtri	|- ( ( ( 3 . 0 ) + ( 0 . 0 ) ) x. ( ( 2 . 4 ) + ( 4 . 9 ) ) ) = ( ; 2 1 . _ 9 0 )
689	650	oveq2i	|- ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + ( 0 . _ 0 0 ) ) = ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + 0 )
690	318 2	pm3.2i	|- ( 2 e. RR /\ 0 e. RR )
691		dp2cl	|- ( ( 2 e. RR /\ 0 e. RR ) -> _ 2 0 e. RR )
692	690 691	ax-mp	|- _ 2 0 e. RR
693		dpcl	|- ( ( 7 e. NN0 /\ _ 2 0 e. RR ) -> ( 7 . _ 2 0 ) e. RR )
694	52 692 693	mp2an	|- ( 7 . _ 2 0 ) e. RR
695	694	recni	|- ( 7 . _ 2 0 ) e. CC
696	3 2	pm3.2i	|- ( 7 e. RR /\ 0 e. RR )
697		dp2cl	|- ( ( 7 e. RR /\ 0 e. RR ) -> _ 7 0 e. RR )
698	696 697	ax-mp	|- _ 7 0 e. RR
699		dpcl	|- ( ( ; 1 4 e. NN0 /\ _ 7 0 e. RR ) -> ( ; 1 4 . _ 7 0 ) e. RR )
700	448 698 699	mp2an	|- ( ; 1 4 . _ 7 0 ) e. RR
701	700	recni	|- ( ; 1 4 . _ 7 0 ) e. CC
702	695 701	addcli	|- ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) e. CC
703	702	addridi	|- ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + 0 ) = ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) )
704		eqid	|- ; ; ; 1 4 7 0 = ; ; ; 1 4 7 0
705	448	nn0cni	|- ; 1 4 e. CC
706	705 217 270	addcomli	|- ( 7 + ; 1 4 ) = ; 2 1
707		7p2e9	|- ( 7 + 2 ) = 9
708	217 197 707	addcomli	|- ( 2 + 7 ) = 9
709	52 181 448 52 263 655 706 708	decadd	|- ( ; 7 2 + ; ; 1 4 7 ) = ; ; 2 1 9
710		00id	|- ( 0 + 0 ) = 0
711	652 51 627 51 656 704 709 710	decadd	|- ( ; ; 7 2 0 + ; ; ; 1 4 7 0 ) = ; ; ; 2 1 9 0
712	52 181 51 448 52 293 51 53 51 711	dpadd3	|- ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) = ( ; 2 1 . _ 9 0 )
713	689 703 712	3eqtri	|- ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + ( 0 . _ 0 0 ) ) = ( ; 2 1 . _ 9 0 )
714	688 713	eqtr4i	|- ( ( ( 3 . 0 ) + ( 0 . 0 ) ) x. ( ( 2 . 4 ) + ( 4 . 9 ) ) ) = ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + ( 0 . _ 0 0 ) )
715	182 51 51 51 181 24 181 51 24 53 52 448 52 51 51 51 51 1 24 52 51 52 182 24 73 102 102 102 630 641 651 659 714	dpmul4	|- ( ( 3 . _ 0 _ 0 0 ) x. ( 2 . _ 4 _ 4 9 ) ) < ( 7 . _ 3 _ 4 8 )
716	626 715	eqbrtri	|- ( 3 x. ( 2 . _ 4 _ 4 9 ) ) < ( 7 . _ 3 _ 4 8 )
717	319 608	remulcli	|- ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) e. RR
718	319 614	remulcli	|- ( 3 x. ( 2 . _ 4 _ 4 9 ) ) e. RR
719		nnrp	|- ( 8 e. NN -> 8 e. RR+ )
720	63 719	ax-mp	|- 8 e. RR+
721	24 720	rpdp2cl	|- _ 4 8 e. RR+
722	182 721	rpdp2cl	|- _ 3 _ 4 8 e. RR+
723	52 722	rpdpcl	|- ( 7 . _ 3 _ 4 8 ) e. RR+
724		rpre	|- ( ( 7 . _ 3 _ 4 8 ) e. RR+ -> ( 7 . _ 3 _ 4 8 ) e. RR )
725	723 724	ax-mp	|- ( 7 . _ 3 _ 4 8 ) e. RR
726	717 718 725	lttri	|- ( ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 3 x. ( 2 . _ 4 _ 4 9 ) ) /\ ( 3 x. ( 2 . _ 4 _ 4 9 ) ) < ( 7 . _ 3 _ 4 8 ) ) -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 7 . _ 3 _ 4 8 ) )
727	620 716 726	mp2an	|- ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 7 . _ 3 _ 4 8 )