hgt750lem2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hgt750lem2		Structured version Visualization version Unicode version

Theorem hgt750lem2 30730

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

**Assertion**
Ref	Expression
hgt750lem2	_____ __ ___ ____ __

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

Colors of variables: wff setvar class

Syntax hints:

wb 196 $/\$ wa 384

wceq 1483

wcel 1990 class class class wbr 4653 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cn 11020

c2 11070

c3 11071

c4 11072

c5 11073

c6 11074

c7 11075

c8 11076

c9 11077

cn0 11292 ;cdc 11493

crp 11832

cexp 12860 _cdp2 29577

cdp 29595

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-seq 12802 df-exp 12861 df-dp2 29578 df-dp 29596

This theorem is referenced by: hgt750leme 30736

W3C validator