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	addid1i	|- ( ; 1 6 + 0 ) = ; 1 6
110		6cn	|- 6 e. CC
111	110	addid2i	|- ( 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	addid2i	|- ( 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	addid2i	|- ( 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	addid1i	|- ( ; ; 1 0 9 + 0 ) = ; ; 1 0 9
191		dec10p	|- ( ; 1 0 + 0 ) = ; 1 0
192	138	addid1i	|- ( 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	mulid1i	|- ( 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	addid1i	|- ( ( 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	mulid1i	|- ( 6 x. 1 ) = 6
216		6t4e24	|- ( 6 x. 4 ) = ; 2 4
217		7cn	|- 7 e. CC
218	217	mulid1i	|- ( 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	addid1i	|- ( 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	addid1i	|- ( 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		3cn	|- 3 e. CC
431		3t2e6	|- ( 3 x. 2 ) = 6
432	430 197 431	mulcomli	|- ( 2 x. 3 ) = 6
433		9t2e18	|- ( 9 x. 2 ) = ; 1 8
434	196 197 433	mulcomli	|- ( 2 x. 9 ) = ; 1 8
435		7t3e21	|- ( 7 x. 3 ) = ; 2 1
436		9t7e63	|- ( 9 x. 7 ) = ; 6 3
437	196 217 436	mulcomli	|- ( 7 x. 9 ) = ; 6 3
438		eqid	|- ; 2 1 = ; 2 1
439		eqid	|- ; 1 8 = ; 1 8
440	159 160	eqtri	|- ( 1 + 8 ) = 9
441	181 1 1 73 438 439 224 440	decadd	|- ( ; 2 1 + ; 1 8 ) = ; 3 9
442	441	oveq1i	|- ( ( ; 2 1 + ; 1 8 ) + 6 ) = ( ; 3 9 + 6 )
443		eqid	|- ; 3 9 = ; 3 9
444		3p1e4	|- ( 3 + 1 ) = 4
445		9p6e15	|- ( 9 + 6 ) = ; 1 5
446	182 53 98 443 444 54 445	decaddci	|- ( ; 3 9 + 6 ) = ; 4 5
447	442 446	eqtri	|- ( ( ; 2 1 + ; 1 8 ) + 6 ) = ; 4 5
448		6p4e10	|- ( 6 + 4 ) = ; 1 0
449	181 52 182 53 98 24 54 182 432 434 435 437 447 448	dpmul	|- ( ( 2 . 7 ) x. ( 3 . 9 ) ) = ( ; 1 0 . _ 5 3 )
450	1 24	deccl	|- ; 1 4 e. NN0
451	450 51	deccl	|- ; ; 1 4 0 e. NN0
452	417 73	eqeltrri	|- ; 0 8 e. NN0
453		eqid	|- ; ; ; 1 4 0 1 = ; ; ; 1 4 0 1
454		eqid	|- ; ; 0 8 2 = ; ; 0 8 2
455		eqid	|- ; ; 1 4 0 = ; ; 1 4 0
456	417 158	eqeltrri	|- ; 0 8 e. CC
457		0cn	|- 0 e. CC
458	417	oveq1i	|- ( 8 + 0 ) = ( ; 0 8 + 0 )
459	158	addid1i	|- ( 8 + 0 ) = 8
460	458 459	eqtr3i	|- ( ; 0 8 + 0 ) = 8
461	456 457 460	addcomli	|- ( 0 + ; 0 8 ) = 8
462	450 51 452 455 461	decaddi	|- ( ; ; 1 4 0 + ; 0 8 ) = ; ; 1 4 8
463	451 1 452 181 453 454 462 230	decadd	|- ( ; ; ; 1 4 0 1 + ; ; 0 8 2 ) = ; ; ; 1 4 8 3
464		4t4e16	|- ( 4 x. 4 ) = ; 1 6
465		9t4e36	|- ( 9 x. 4 ) = ; 3 6
466	196 113 465	mulcomli	|- ( 4 x. 9 ) = ; 3 6
467	196	mulid1i	|- ( 9 x. 1 ) = 9
468	467 188	eqtri	|- ( 9 x. 1 ) = ; 0 9
469	196 138 468	mulcomli	|- ( 1 x. 9 ) = ; 0 9
470	182 98	deccl	|- ; 3 6 e. NN0
471	470	nn0cni	|- ; 3 6 e. CC
472		eqid	|- ; 3 6 = ; 3 6
473	182 98 24 472 444 51 448	decaddci	|- ( ; 3 6 + 4 ) = ; 4 0
474	471 113 473	addcomli	|- ( 4 + ; 3 6 ) = ; 4 0
475	474	oveq1i	|- ( ( 4 + ; 3 6 ) + 0 ) = ( ; 4 0 + 0 )
476	24 51	deccl	|- ; 4 0 e. NN0
477	476	nn0cni	|- ; 4 0 e. CC
478	477	addid1i	|- ( ; 4 0 + 0 ) = ; 4 0
479	475 478	eqtri	|- ( ( 4 + ; 3 6 ) + 0 ) = ; 4 0
480	1 98 24 135 269 51 448	decaddci	|- ( ; 1 6 + 4 ) = ; 2 0
481	24 1 24 53 51 24 51 53 464 466 204 469 479 480	dpmul	|- ( ( 4 . 1 ) x. ( 4 . 9 ) ) = ( ; 2 0 . _ 0 9 )
482		eqid	|- ; 2 7 = ; 2 7
483	230	oveq1i	|- ( ( 1 + 2 ) + 1 ) = ( 3 + 1 )
484	483 444	eqtri	|- ( ( 1 + 2 ) + 1 ) = 4
485	1 24 181 52 268 482 484 1 225	decaddc	|- ( ; 1 4 + ; 2 7 ) = ; 4 1
486	1 24 181 52 24 1 485	dpadd	|- ( ( 1 . 4 ) + ( 2 . 7 ) ) = ( 4 . 1 )
487	430 138 444	addcomli	|- ( 1 + 3 ) = 4
488	196	addid2i	|- ( 0 + 9 ) = 9
489	1 51 182 53 414 443 487 488	decadd	|- ( ; 1 0 + ; 3 9 ) = ; 4 9
490	1 51 182 53 24 53 489	dpadd	|- ( ( 1 . 0 ) + ( 3 . 9 ) ) = ( 4 . 9 )
491	486 490	oveq12i	|- ( ( ( 1 . 4 ) + ( 2 . 7 ) ) x. ( ( 1 . 0 ) + ( 3 . 9 ) ) ) = ( ( 4 . 1 ) x. ( 4 . 9 ) )
492	1 24 73 1 268 415 440 210	decadd	|- ( ; 1 4 + ; 8 1 ) = ; 9 5
493	450 51 412 98 455 413 492 111	decadd	|- ( ; ; 1 4 0 + ; ; 8 1 6 ) = ; ; 9 5 6
494	1 24 51 73 1 53 98 54 98 493	dpadd3	|- ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) = ( 9 . _ 5 6 )
495	494	oveq1i	|- ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) ) = ( ( 9 . _ 5 6 ) + ( ; 1 0 . _ 5 3 ) )
496	181 51	deccl	|- ; 2 0 e. NN0
497	53 54	deccl	|- ; 9 5 e. NN0
498	130 54	deccl	|- ; ; 1 0 5 e. NN0
499		eqid	|- ; ; 9 5 6 = ; ; 9 5 6
500		eqid	|- ; ; ; 1 0 5 3 = ; ; ; 1 0 5 3
501		eqid	|- ; 9 5 = ; 9 5
502		eqid	|- ; ; 1 0 5 = ; ; 1 0 5
503		dec10p	|- ( ; 1 0 + 9 ) = ; 1 9
504	283 196 503	addcomli	|- ( 9 + ; 1 0 ) = ; 1 9
505	504	oveq1i	|- ( ( 9 + ; 1 0 ) + 1 ) = ( ; 1 9 + 1 )
506		eqid	|- ; 1 9 = ; 1 9
507	1 53 1 506 269 51 194	decaddci	|- ( ; 1 9 + 1 ) = ; 2 0
508	505 507	eqtri	|- ( ( 9 + ; 1 0 ) + 1 ) = ; 2 0
509		5p5e10	|- ( 5 + 5 ) = ; 1 0
510	53 54 130 54 501 502 508 51 509	decaddc	|- ( ; 9 5 + ; ; 1 0 5 ) = ; ; 2 0 0
511	497 98 498 182 499 500 510 233	decadd	|- ( ; ; 9 5 6 + ; ; ; 1 0 5 3 ) = ; ; ; 2 0 0 9
512	53 54 98 130 54 496 182 51 53 511	dpadd3	|- ( ( 9 . _ 5 6 ) + ( ; 1 0 . _ 5 3 ) ) = ( ; 2 0 . _ 0 9 )
513	495 512	eqtri	|- ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) ) = ( ; 2 0 . _ 0 9 )
514	481 491 513	3eqtr4i	|- ( ( ( 1 . 4 ) + ( 2 . 7 ) ) x. ( ( 1 . 0 ) + ( 3 . 9 ) ) ) = ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) )
515	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 449 463 514	dpmul4	|- ( ( 1 . _ 4 _ 2 7 ) x. ( 1 . _ 0 _ 3 9 ) ) < ( 1 . _ 4 _ 8 3 )
516	375 395	remulcli	|- ( ( 1 . _ 4 _ 2 7 ) x. ( 1 . _ 0 _ 3 9 ) ) e. RR
517	345 516 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 ) )
518	410 515 517	mp2an	|- ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 )
519	367 518	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 ) )
520	351 519	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 ) ) )
521		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 ) ) )
522	316 520 521	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 ) )
523	24 181	deccl	|- ; 4 2 e. NN0
524	496 24	deccl	|- ; ; 2 0 4 e. NN0
525		eqid	|- ; ; ; 2 0 4 2 = ; ; ; 2 0 4 2
526		eqid	|- ; 4 2 = ; 4 2
527		eqid	|- ; ; 2 0 4 = ; ; 2 0 4
528	496 24 24 527 277	decaddi	|- ( ; ; 2 0 4 + 4 ) = ; ; 2 0 8
529		2p2e4	|- ( 2 + 2 ) = 4
530	524 181 24 181 525 526 528 529	decadd	|- ( ; ; ; 2 0 4 2 + ; 4 2 ) = ; ; ; 2 0 8 4
531	448	oveq1i	|- ( ( 6 + 4 ) + 2 ) = ( ; 1 0 + 2 )
532		dec10p	|- ( ; 1 0 + 2 ) = ; 1 2
533	531 532	eqtri	|- ( ( 6 + 4 ) + 2 ) = ; 1 2
534	1 98 1 24 181 1 181 24 116 204 215 216 533 269	dpmul	|- ( ( 1 . 6 ) x. ( 1 . 4 ) ) = ( 2 . _ 2 4 )
535		8t5e40	|- ( 8 x. 5 ) = ; 4 0
536	158 256 535	mulcomli	|- ( 5 x. 8 ) = ; 4 0
537		5t3e15	|- ( 5 x. 3 ) = ; 1 5
538	158	mulid2i	|- ( 1 x. 8 ) = 8
539	430	mulid2i	|- ( 1 x. 3 ) = 3
540	182	dec0h	|- 3 = ; 0 3
541	539 540	eqtri	|- ( 1 x. 3 ) = ; 0 3
542	235	nn0cni	|- ; 1 5 e. CC
543		8p5e13	|- ( 8 + 5 ) = ; 1 3
544	158 256 543	addcomli	|- ( 5 + 8 ) = ; 1 3
545	1 54 73 245 269 182 544	decaddci	|- ( ; 1 5 + 8 ) = ; 2 3
546	542 158 545	addcomli	|- ( 8 + ; 1 5 ) = ; 2 3
547	546	oveq1i	|- ( ( 8 + ; 1 5 ) + 0 ) = ( ; 2 3 + 0 )
548	181 182	deccl	|- ; 2 3 e. NN0
549	548	nn0cni	|- ; 2 3 e. CC
550	549	addid1i	|- ( ; 2 3 + 0 ) = ; 2 3
551	547 550	eqtri	|- ( ( 8 + ; 1 5 ) + 0 ) = ; 2 3
552		eqid	|- ; 4 0 = ; 4 0
553	197	addid2i	|- ( 0 + 2 ) = 2
554	24 51 181 552 553	decaddi	|- ( ; 4 0 + 2 ) = ; 4 2
555	54 1 73 182 51 181 182 182 536 537 538 541 551 554	dpmul	|- ( ( 5 . 1 ) x. ( 8 . 3 ) ) = ( ; 4 2 . _ 3 3 )
556	181 181	deccl	|- ; 2 2 e. NN0
557	556 24	deccl	|- ; ; 2 2 4 e. NN0
558		eqid	|- ; ; ; 2 2 4 1 = ; ; ; 2 2 4 1
559		eqid	|- ; ; 2 0 8 = ; ; 2 0 8
560		eqid	|- ; ; 2 2 4 = ; ; 2 2 4
561		eqid	|- ; 2 0 = ; 2 0
562		eqid	|- ; 2 2 = ; 2 2
563	181 181 181 562 529	decaddi	|- ( ; 2 2 + 2 ) = ; 2 4
564	556 24 181 51 560 561 563 426	decadd	|- ( ; ; 2 2 4 + ; 2 0 ) = ; ; 2 4 4
565	557 1 496 73 558 559 564 440	decadd	|- ( ; ; ; 2 2 4 1 + ; ; 2 0 8 ) = ; ; ; 2 4 4 9
566	556 98	deccl	|- ; ; 2 2 6 e. NN0
567	523 182	deccl	|- ; ; 4 2 3 e. NN0
568		eqid	|- ; ; ; 2 2 6 6 = ; ; ; 2 2 6 6
569		eqid	|- ; ; ; 4 2 3 3 = ; ; ; 4 2 3 3
570		eqid	|- ; ; 2 2 6 = ; ; 2 2 6
571		eqid	|- ; ; 4 2 3 = ; ; 4 2 3
572	113 197 289	addcomli	|- ( 2 + 4 ) = 6
573	181 181 24 181 562 526 572 529	decadd	|- ( ; 2 2 + ; 4 2 ) = ; 6 4
574	556 98 523 182 570 571 573 233	decadd	|- ( ; ; 2 2 6 + ; ; 4 2 3 ) = ; ; 6 4 9
575	566 98 567 182 568 569 574 233	decadd	|- ( ; ; ; 2 2 6 6 + ; ; ; 4 2 3 3 ) = ; ; ; 6 4 9 9
576	556 98 98 523 182 100 182 53 53 575	dpadd3	|- ( ( ; 2 2 . _ 6 6 ) + ( ; 4 2 . _ 3 3 ) ) = ( ; 6 4 . _ 9 9 )
577	496	nn0cni	|- ; 2 0 e. CC
578	181 51 181 561 553	decaddi	|- ( ; 2 0 + 2 ) = ; 2 2
579	577 197 578	addcomli	|- ( 2 + ; 2 0 ) = ; 2 2
580	181 181 496 24 562 527 579 572	decadd	|- ( ; 2 2 + ; ; 2 0 4 ) = ; ; 2 2 6
581	556 24 524 181 560 525 580 289	decadd	|- ( ; ; 2 2 4 + ; ; ; 2 0 4 2 ) = ; ; ; 2 2 6 6
582	181 181 24 496 24 556 181 98 98 581	dpadd3	|- ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) = ( ; 2 2 . _ 6 6 )
583	582	oveq1i	|- ( ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) + ( ; 4 2 . _ 3 3 ) ) = ( ( ; 2 2 . _ 6 6 ) + ( ; 4 2 . _ 3 3 ) )
584		eqid	|- ; 5 1 = ; 5 1
585	1 98 54 1 135 584 257 140	decadd	|- ( ; 1 6 + ; 5 1 ) = ; 6 7
586	1 98 54 1 98 52 585	dpadd	|- ( ( 1 . 6 ) + ( 5 . 1 ) ) = ( 6 . 7 )
587		eqid	|- ; 8 3 = ; 8 3
588	1 24 73 182 268 587 440 302	decadd	|- ( ; 1 4 + ; 8 3 ) = ; 9 7
589	1 24 73 182 53 52 588	dpadd	|- ( ( 1 . 4 ) + ( 8 . 3 ) ) = ( 9 . 7 )
590	586 589	oveq12i	|- ( ( ( 1 . 6 ) + ( 5 . 1 ) ) x. ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ( 6 . 7 ) x. ( 9 . 7 ) )
591		9t6e54	|- ( 9 x. 6 ) = ; 5 4
592	196 110 591	mulcomli	|- ( 6 x. 9 ) = ; 5 4
593		7t6e42	|- ( 7 x. 6 ) = ; 4 2
594	217 110 593	mulcomli	|- ( 6 x. 7 ) = ; 4 2
595		7t7e49	|- ( 7 x. 7 ) = ; 4 9
596		eqid	|- ; 6 3 = ; 6 3
597		3p2e5	|- ( 3 + 2 ) = 5
598	98 182 24 181 596 526 448 597	decadd	|- ( ; 6 3 + ; 4 2 ) = ; ; 1 0 5
599	598	oveq1i	|- ( ( ; 6 3 + ; 4 2 ) + 4 ) = ( ; ; 1 0 5 + 4 )
600		5p4e9	|- ( 5 + 4 ) = 9
601	130 54 24 502 600	decaddi	|- ( ; ; 1 0 5 + 4 ) = ; ; 1 0 9
602	599 601	eqtri	|- ( ( ; 6 3 + ; 4 2 ) + 4 ) = ; ; 1 0 9
603		eqid	|- ; 5 4 = ; 5 4
604	54 24 1 51 603 414 246 426	decadd	|- ( ; 5 4 + ; 1 0 ) = ; 6 4
605	98 52 53 52 24 130 53 53 592 594 437 595 602 604	dpmul	|- ( ( 6 . 7 ) x. ( 9 . 7 ) ) = ( ; 6 4 . _ 9 9 )
606	590 605	eqtri	|- ( ( ( 1 . 6 ) + ( 5 . 1 ) ) x. ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ; 6 4 . _ 9 9 )
607	576 583 606	3eqtr4ri	|- ( ( ( 1 . 6 ) + ( 5 . 1 ) ) x. ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) + ( ; 4 2 . _ 3 3 ) )
608	1 98 54 1 1 73 181 24 24 182 181 496 24 181 523 182 182 181 51 73 24 181 24 24 53 101 184 184 530 534 555 565 607	dpmul4	|- ( ( 1 . _ 6 _ 5 1 ) x. ( 1 . _ 4 _ 8 3 ) ) < ( 2 . _ 4 _ 4 9 )
609	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
610	43 350	remulcli	|- ( ( 1 . _ 6 _ 5 1 ) x. ( 1 . _ 4 _ 8 3 ) ) e. RR
611	24 399	rpdp2cl	|- _ 4 9 e. RR+
612	24 611	rpdp2cl	|- _ 4 _ 4 9 e. RR+
613	181 612	rpdpcl	|- ( 2 . _ 4 _ 4 9 ) e. RR+
614		rpre	|- ( ( 2 . _ 4 _ 4 9 ) e. RR+ -> ( 2 . _ 4 _ 4 9 ) e. RR )
615	613 614	ax-mp	|- ( 2 . _ 4 _ 4 9 ) e. RR
616	609 610 615	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 ) )
617	522 608 616	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 )
618		3pos	|- 0 < 3
619	609 615 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 ) ) ) )
620	618 619	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 ) ) )
621	617 620	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 ) )
622	119	dp2eq2i	|- _ 0 _ 0 0 = _ 0 0
623	622 119	eqtri	|- _ 0 _ 0 0 = 0
624	623	oveq2i	|- ( 3 . _ 0 _ 0 0 ) = ( 3 . 0 )
625	182	dp0u	|- ( 3 . 0 ) = 3
626	624 625	eqtr2i	|- 3 = ( 3 . _ 0 _ 0 0 )
627	626	oveq1i	|- ( 3 x. ( 2 . _ 4 _ 4 9 ) ) = ( ( 3 . _ 0 _ 0 0 ) x. ( 2 . _ 4 _ 4 9 ) )
628	450 52	deccl	|- ; ; 1 4 7 e. NN0
629	628 51	deccl	|- ; ; ; 1 4 7 0 e. NN0
630	629	nn0cni	|- ; ; ; 1 4 7 0 e. CC
631	630	addid1i	|- ( ; ; ; 1 4 7 0 + 0 ) = ; ; ; 1 4 7 0
632		4t3e12	|- ( 4 x. 3 ) = ; 1 2
633	113 430 632	mulcomli	|- ( 3 x. 4 ) = ; 1 2
634	197	mul02i	|- ( 0 x. 2 ) = 0
635	113 457 425	mulcomli	|- ( 0 x. 4 ) = ; 0 0
636	51 51 1 181 424 300 153 553	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	addid1i	|- ( ; 1 2 + 0 ) = ; 1 2
640	637 639	eqtri	|- ( ( 0 + ; 1 2 ) + 0 ) = ; 1 2
641	182 51 181 24 51 1 181 51 431 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 450 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	625 430	eqeltri	|- ( 3 . 0 ) e. CC
662	661	addid1i	|- ( ( 3 . 0 ) + 0 ) = ( 3 . 0 )
663	660 662	eqtri	|- ( ( 3 . 0 ) + ( 0 . 0 ) ) = ( 3 . 0 )
664		eqid	|- ; 4 9 = ; 4 9
665	572	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 430 435	mulcomli	|- ( 3 x. 7 ) = ; 2 1
673		3t3e9	|- ( 3 x. 3 ) = 9
674	217	mul01i	|- ( 7 x. 0 ) = 0
675	217 457 674	mulcomli	|- ( 0 x. 7 ) = 0
676	430	mul01i	|- ( 3 x. 0 ) = 0
677	676 424	eqtri	|- ( 3 x. 0 ) = ; 0 0
678	430 457 677	mulcomli	|- ( 0 x. 3 ) = ; 0 0
679	196	addid1i	|- ( 9 + 0 ) = 9
680	679	oveq1i	|- ( ( 9 + 0 ) + 0 ) = ( 9 + 0 )
681	680 679 188	3eqtri	|- ( ( 9 + 0 ) + 0 ) = ; 0 9
682	196 457	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 438 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	450 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	addid1i	|- ( ( ( 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	450	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 450 52 263 655 706 708	decadd	|- ( ; 7 2 + ; ; 1 4 7 ) = ; ; 2 1 9
710		00id	|- ( 0 + 0 ) = 0
711	652 51 628 51 656 704 709 710	decadd	|- ( ; ; 7 2 0 + ; ; ; 1 4 7 0 ) = ; ; ; 2 1 9 0
712	52 181 51 450 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 450 52 51 51 51 51 1 24 52 51 52 182 24 73 102 102 102 631 641 651 659 714	dpmul4	|- ( ( 3 . _ 0 _ 0 0 ) x. ( 2 . _ 4 _ 4 9 ) ) < ( 7 . _ 3 _ 4 8 )
716	627 715	eqbrtri	|- ( 3 x. ( 2 . _ 4 _ 4 9 ) ) < ( 7 . _ 3 _ 4 8 )
717	319 609	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 615	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	621 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 )