dpmul4 - Mathbox for Thierry Arnoux

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

Theorem dpmul4 29622

Description: An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)

**Hypotheses**
Ref	Expression
dpmul.a
dpmul.b
dpmul.c
dpmul.d
dpmul.e
dpmul.g
dpmul.j
dpmul.k
dpmul4.f
dpmul4.h
dpmul4.i
dpmul4.l
dpmul4.m
dpmul4.n
dpmul4.o
dpmul4.p
dpmul4.q
dpmul4.r
dpmul4.s
dpmul4.t
dpmul4.u
dpmul4.w
dpmul4.x
dpmul4.y
dpmul4.z
dpmul4.a	;
dpmul4.b	;
dpmul4.c	;
dpmul4.1	;; ;;;
dpmul4.2	_
dpmul4.3	_
dpmul4.4	;;; ;; ;;;
dpmul4.5	_ _ _

**Assertion**
Ref	Expression
dpmul4	__ __ __

**Proof of Theorem dpmul4**
Step	Hyp	Ref	Expression
1		dpmul.a	. . . . . . . . 9
2		dpmul.b	. . . . . . . . 9
3	1, 2	deccl 11512	. . . . . . . 8 ;
4		dpmul.c	. . . . . . . . 9
5		dpmul.d	. . . . . . . . 9
6	4, 5	deccl 11512	. . . . . . . 8 ;
7		dpmul.e	. . . . . . . . 9
8		dpmul4.f	. . . . . . . . 9
9	7, 8	deccl 11512	. . . . . . . 8 ;
10		dpmul.g	. . . . . . . . 9
11		dpmul4.h	. . . . . . . . 9
12	10, 11	deccl 11512	. . . . . . . 8 ;
13		dpmul4.l	. . . . . . . . . 10
14		dpmul4.m	. . . . . . . . . 10
15	13, 14	deccl 11512	. . . . . . . . 9 ;
16		dpmul4.n	. . . . . . . . 9
17	15, 16	deccl 11512	. . . . . . . 8 ;;
18		2nn0 11309	. . . . . . . 8
19	2	nn0rei 11303	. . . . . . . . . . . . 13
20		dpcl 29598	. . . . . . . . . . . . 13 $/\$
21	1, 19, 20	mp2an 708	. . . . . . . . . . . 12
22	21	recni 10052	. . . . . . . . . . 11
23		10nn 11514	. . . . . . . . . . . 12 ;
24	23	nncni 11030	. . . . . . . . . . 11 ;
25	8	nn0rei 11303	. . . . . . . . . . . . 13
26		dpcl 29598	. . . . . . . . . . . . 13 $/\$
27	7, 25, 26	mp2an 708	. . . . . . . . . . . 12
28	27	recni 10052	. . . . . . . . . . 11
29	22, 24, 28, 24	mul4i 10233	. . . . . . . . . 10 ; ; ; ;
30	22, 28	mulcli 10045	. . . . . . . . . . 11
31	30, 24, 24	mulassi 10049	. . . . . . . . . 10 ; ; ; ;
32		dpmul4.2	. . . . . . . . . . . . 13 _
33	32	oveq1i 6660	. . . . . . . . . . . 12 ; _ ;
34		dpmul4.i	. . . . . . . . . . . . 13
35		dpmul.j	. . . . . . . . . . . . 13
36		dpmul.k	. . . . . . . . . . . . . 14
37	36	nn0rei 11303	. . . . . . . . . . . . 13
38	34, 35, 37	dp3mul10 29606	. . . . . . . . . . . 12 _ ; ;
39	33, 38	eqtri 2644	. . . . . . . . . . 11 ; ;
40	39	oveq1i 6660	. . . . . . . . . 10 ; ; ; ;
41	29, 31, 40	3eqtr2ri 2651	. . . . . . . . 9 ; ; ; ;
42	34, 35	deccl 11512	. . . . . . . . . 10 ;
43	42, 37	dpmul10 29603	. . . . . . . . 9 ; ; ;;
44	1, 19	dpmul10 29603	. . . . . . . . . 10 ; ;
45	7, 25	dpmul10 29603	. . . . . . . . . 10 ; ;
46	44, 45	oveq12i 6662	. . . . . . . . 9 ; ; ; ;
47	41, 43, 46	3eqtr3ri 2653	. . . . . . . 8 ; ; ;;
48	5	nn0rei 11303	. . . . . . . . . . . . 13
49		dpcl 29598	. . . . . . . . . . . . 13 $/\$
50	4, 48, 49	mp2an 708	. . . . . . . . . . . 12
51	50	recni 10052	. . . . . . . . . . 11
52	11	nn0rei 11303	. . . . . . . . . . . . 13
53		dpcl 29598	. . . . . . . . . . . . 13 $/\$
54	10, 52, 53	mp2an 708	. . . . . . . . . . . 12
55	54	recni 10052	. . . . . . . . . . 11
56	51, 24, 55, 24	mul4i 10233	. . . . . . . . . 10 ; ; ; ;
57	51, 55	mulcli 10045	. . . . . . . . . . 11
58	57, 24, 24	mulassi 10049	. . . . . . . . . 10 ; ; ; ;
59		dpmul4.3	. . . . . . . . . . . . 13 _
60	59	oveq1i 6660	. . . . . . . . . . . 12 ; _ ;
61		dpmul4.o	. . . . . . . . . . . . 13
62		dpmul4.p	. . . . . . . . . . . . 13
63		dpmul4.q	. . . . . . . . . . . . . 14
64	63	nn0rei 11303	. . . . . . . . . . . . 13
65	61, 62, 64	dp3mul10 29606	. . . . . . . . . . . 12 _ ; ;
66	60, 65	eqtri 2644	. . . . . . . . . . 11 ; ;
67	66	oveq1i 6660	. . . . . . . . . 10 ; ; ; ;
68	56, 58, 67	3eqtr2ri 2651	. . . . . . . . 9 ; ; ; ;
69	61, 62	deccl 11512	. . . . . . . . . 10 ;
70	69, 64	dpmul10 29603	. . . . . . . . 9 ; ; ;;
71	4, 48	dpmul10 29603	. . . . . . . . . 10 ; ;
72	10, 52	dpmul10 29603	. . . . . . . . . 10 ; ;
73	71, 72	oveq12i 6662	. . . . . . . . 9 ; ; ; ;
74	68, 70, 73	3eqtr3ri 2653	. . . . . . . 8 ; ; ;;
75	22, 51, 24	adddiri 10051	. . . . . . . . . . . 12 ; ; ;
76	44, 71	oveq12i 6662	. . . . . . . . . . . 12 ; ; ; ;
77	75, 76	eqtr2i 2645	. . . . . . . . . . 11 ; ; ;
78	28, 55, 24	adddiri 10051	. . . . . . . . . . . 12 ; ; ;
79	45, 72	oveq12i 6662	. . . . . . . . . . . 12 ; ; ; ;
80	78, 79	eqtr2i 2645	. . . . . . . . . . 11 ; ; ;
81	77, 80	oveq12i 6662	. . . . . . . . . 10 ; ; ; ; ; ;
82	22, 51	addcli 10044	. . . . . . . . . . 11
83	28, 55	addcli 10044	. . . . . . . . . . 11
84	82, 24, 83, 24	mul4i 10233	. . . . . . . . . 10 ; ; ; ;
85		dpmul4.5	. . . . . . . . . . 11 _ _ _
86	85	oveq1i 6660	. . . . . . . . . 10 ; ; _ _ _ ; ;
87	81, 84, 86	3eqtri 2648	. . . . . . . . 9 ; ; ; ; _ _ _ ; ;
88		10nn0 11516	. . . . . . . . . . 11 ;
89	88	dec0u 11520	. . . . . . . . . 10 ; ; ;;
90	89	oveq2i 6661	. . . . . . . . 9 _ _ _ ; ; _ _ _ ;;
91	32, 30	eqeltrri 2698	. . . . . . . . . . . 12 _
92	14	nn0rei 11303	. . . . . . . . . . . . . . 15
93	16	nn0rei 11303	. . . . . . . . . . . . . . 15
94		dp2cl 29587	. . . . . . . . . . . . . . 15 $/\$ _
95	92, 93, 94	mp2an 708	. . . . . . . . . . . . . 14 _
96		dpcl 29598	. . . . . . . . . . . . . 14 $/\$ _ _
97	13, 95, 96	mp2an 708	. . . . . . . . . . . . 13 _
98	97	recni 10052	. . . . . . . . . . . 12 _
99	91, 98	addcli 10044	. . . . . . . . . . 11 _ _
100	59, 57	eqeltrri 2698	. . . . . . . . . . 11 _
101		0nn0 11307	. . . . . . . . . . . . 13
102	88, 101	deccl 11512	. . . . . . . . . . . 12 ;;
103	102	nn0cni 11304	. . . . . . . . . . 11 ;;
104	99, 100, 103	adddiri 10051	. . . . . . . . . 10 _ _ _ ;; _ _ ;; _ ;;
105	91, 98, 103	adddiri 10051	. . . . . . . . . . 11 _ _ ;; _ ;; _ ;;
106	105	oveq1i 6660	. . . . . . . . . 10 _ _ ;; _ ;; _ ;; _ ;; _ ;;
107	34, 35, 37	dpmul100 29605	. . . . . . . . . . . 12 _ ;; ;;
108	13, 14, 93	dpmul100 29605	. . . . . . . . . . . 12 _ ;; ;;
109	107, 108	oveq12i 6662	. . . . . . . . . . 11 _ ;; _ ;; ;; ;;
110	61, 62, 64	dpmul100 29605	. . . . . . . . . . 11 _ ;; ;;
111	109, 110	oveq12i 6662	. . . . . . . . . 10 _ ;; _ ;; _ ;; ;; ;; ;;
112	104, 106, 111	3eqtri 2648	. . . . . . . . 9 _ _ _ ;; ;; ;; ;;
113	87, 90, 112	3eqtri 2648	. . . . . . . 8 ; ; ; ; ;; ;; ;;
114		sq10 13048	. . . . . . . . . . . 12 ; ;;
115	114	oveq2i 6661	. . . . . . . . . . 11 ; ; ; ;;
116	3	nn0cni 11304	. . . . . . . . . . . 12 ;
117	103, 116	mulcomi 10046	. . . . . . . . . . 11 ;; ; ; ;;
118	115, 117	eqtr4i 2647	. . . . . . . . . 10 ; ; ;; ;
119	118	oveq1i 6660	. . . . . . . . 9 ; ; ; ;; ; ;
120	3, 4, 48	dfdec100 29576	. . . . . . . . 9 ;;; ;; ; ;
121	119, 120	eqtr4i 2647	. . . . . . . 8 ; ; ; ;;;
122	114	oveq2i 6661	. . . . . . . . . . 11 ; ; ; ;;
123	9	nn0cni 11304	. . . . . . . . . . . 12 ;
124	103, 123	mulcomi 10046	. . . . . . . . . . 11 ;; ; ; ;;
125	122, 124	eqtr4i 2647	. . . . . . . . . 10 ; ; ;; ;
126	125	oveq1i 6660	. . . . . . . . 9 ; ; ; ;; ; ;
127	9, 10, 52	dfdec100 29576	. . . . . . . . 9 ;;; ;; ; ;
128	126, 127	eqtr4i 2647	. . . . . . . 8 ; ; ; ;;;
129	24	sqvali 12943	. . . . . . . . . . . 12 ; ; ;
130	129	oveq2i 6661	. . . . . . . . . . 11 ;; ; ;; ; ;
131	42, 36	deccl 11512	. . . . . . . . . . . . 13 ;;
132	131	nn0cni 11304	. . . . . . . . . . . 12 ;;
133	132, 24, 24	mulassi 10049	. . . . . . . . . . 11 ;; ; ; ;; ; ;
134	130, 133	eqtr4i 2647	. . . . . . . . . 10 ;; ; ;; ; ;
135		dpmul4.r	. . . . . . . . . . . . . . . 16
136		dpmul4.s	. . . . . . . . . . . . . . . 16
137	135, 136	deccl 11512	. . . . . . . . . . . . . . 15 ;
138		dpmul4.t	. . . . . . . . . . . . . . 15
139	137, 138	deccl 11512	. . . . . . . . . . . . . 14 ;;
140	139	nn0cni 11304	. . . . . . . . . . . . 13 ;;
141		ax-1cn 9994	. . . . . . . . . . . . 13
142	140, 141	addcli 10044	. . . . . . . . . . . 12 ;;
143	132, 24	mulcli 10045	. . . . . . . . . . . 12 ;; ;
144	141, 143	addcomi 10227	. . . . . . . . . . . . . . . 16 ;; ; ;; ;
145	24, 132	mulcomi 10046	. . . . . . . . . . . . . . . . . 18 ; ;; ;; ;
146	131	dec0u 11520	. . . . . . . . . . . . . . . . . 18 ; ;; ;;;
147	145, 146	eqtr3i 2646	. . . . . . . . . . . . . . . . 17 ;; ; ;;;
148	147	oveq1i 6660	. . . . . . . . . . . . . . . 16 ;; ; ;;;
149	141	addid2i 10224	. . . . . . . . . . . . . . . . 17
150		eqid 2622	. . . . . . . . . . . . . . . . 17 ;;; ;;;
151	131, 101, 149, 150	decsuc 11535	. . . . . . . . . . . . . . . 16 ;;; ;;;
152	144, 148, 151	3eqtri 2648	. . . . . . . . . . . . . . 15 ;; ; ;;;
153	152	oveq2i 6661	. . . . . . . . . . . . . 14 ;; ;; ; ;; ;;;
154	140, 141, 143	addassi 10048	. . . . . . . . . . . . . 14 ;; ;; ; ;; ;; ;
155		1nn0 11308	. . . . . . . . . . . . . . . . 17
156	131, 155	deccl 11512	. . . . . . . . . . . . . . . 16 ;;;
157	156	nn0cni 11304	. . . . . . . . . . . . . . 15 ;;;
158	157, 140	addcomi 10227	. . . . . . . . . . . . . 14 ;;; ;; ;; ;;;
159	153, 154, 158	3eqtr4i 2654	. . . . . . . . . . . . 13 ;; ;; ; ;;; ;;
160		dpmul4.4	. . . . . . . . . . . . 13 ;;; ;; ;;;
161	159, 160	eqtri 2644	. . . . . . . . . . . 12 ;; ;; ; ;;;
162	142, 143, 161	mvlladdi 10299	. . . . . . . . . . 11 ;; ; ;;; ;;
163	162	oveq1i 6660	. . . . . . . . . 10 ;; ; ; ;;; ;; ;
164	134, 163	eqtri 2644	. . . . . . . . 9 ;; ; ;;; ;; ;
165	164	oveq1i 6660	. . . . . . . 8 ;; ; ;; ;;; ;; ; ;;
166		eqid 2622	. . . . . . . 8 ;;; ;; ; ;; ; ;; ;;; ;; ; ;; ; ;;
167	3, 6, 9, 12, 17, 18, 47, 74, 113, 121, 128, 165, 166	karatsuba 15792	. . . . . . 7 ;;; ;;; ;;; ;; ; ;; ; ;;
168		dpmul4.w	. . . . . . . . . . . . . . 15
169		dpmul4.x	. . . . . . . . . . . . . . 15
170	168, 169	deccl 11512	. . . . . . . . . . . . . 14 ;
171		dpmul4.y	. . . . . . . . . . . . . 14
172	170, 171	deccl 11512	. . . . . . . . . . . . 13 ;;
173		dpmul4.z	. . . . . . . . . . . . 13
174	172, 173	deccl 11512	. . . . . . . . . . . 12 ;;;
175	174	nn0cni 11304	. . . . . . . . . . 11 ;;;
176	102, 101	deccl 11512	. . . . . . . . . . . 12 ;;;
177	176	nn0cni 11304	. . . . . . . . . . 11 ;;;
178	175, 177	mulcli 10045	. . . . . . . . . 10 ;;; ;;;
179	142, 177	mulcli 10045	. . . . . . . . . 10 ;; ;;;
180	178, 179	subcli 10357	. . . . . . . . 9 ;;; ;;; ;; ;;;
181	17	nn0cni 11304	. . . . . . . . . 10 ;;
182	103, 181	mulcli 10045	. . . . . . . . 9 ;; ;;
183	61, 62, 64	dfdec100 29576	. . . . . . . . . 10 ;; ;; ;
184	69, 63	deccl 11512	. . . . . . . . . . 11 ;;
185	184	nn0cni 11304	. . . . . . . . . 10 ;;
186	183, 185	eqeltrri 2698	. . . . . . . . 9 ;; ;
187	180, 182, 186	addassi 10048	. . . . . . . 8 ;;; ;;; ;; ;;; ;; ;; ;; ; ;;; ;;; ;; ;;; ;; ;; ;; ;
188	24	sqcli 12944	. . . . . . . . . . . . 13 ;
189	132, 188	mulcli 10045	. . . . . . . . . . . 12 ;; ;
190	164, 189	eqeltrri 2698	. . . . . . . . . . 11 ;;; ;; ;
191	190, 181, 103	adddiri 10051	. . . . . . . . . 10 ;;; ;; ; ;; ;; ;;; ;; ; ;; ;; ;;
192	114	oveq2i 6661	. . . . . . . . . 10 ;;; ;; ; ;; ; ;;; ;; ; ;; ;;
193	175, 142	subcli 10357	. . . . . . . . . . . . 13 ;;; ;;
194	193, 24, 103	mulassi 10049	. . . . . . . . . . . 12 ;;; ;; ; ;; ;;; ;; ; ;;
195	102	dec0u 11520	. . . . . . . . . . . . 13 ; ;; ;;;
196	195	oveq2i 6661	. . . . . . . . . . . 12 ;;; ;; ; ;; ;;; ;; ;;;
197	175, 142, 177	subdiri 10480	. . . . . . . . . . . 12 ;;; ;; ;;; ;;; ;;; ;; ;;;
198	194, 196, 197	3eqtrri 2649	. . . . . . . . . . 11 ;;; ;;; ;; ;;; ;;; ;; ; ;;
199	103, 181	mulcomi 10046	. . . . . . . . . . 11 ;; ;; ;; ;;
200	198, 199	oveq12i 6662	. . . . . . . . . 10 ;;; ;;; ;; ;;; ;; ;; ;;; ;; ; ;; ;; ;;
201	191, 192, 200	3eqtr4i 2654	. . . . . . . . 9 ;;; ;; ; ;; ; ;;; ;;; ;; ;;; ;; ;;
202	201, 183	oveq12i 6662	. . . . . . . 8 ;;; ;; ; ;; ; ;; ;;; ;;; ;; ;;; ;; ;; ;; ;
203	182, 186	addcli 10044	. . . . . . . . 9 ;; ;; ;; ;
204		subsub 10311	. . . . . . . . 9 ;;; ;;; $/\$ ;; ;;; $/\$ ;; ;; ;; ; ;;; ;;; ;; ;;; ;; ;; ;; ; ;;; ;;; ;; ;;; ;; ;; ;; ;
205	178, 179, 203, 204	mp3an 1424	. . . . . . . 8 ;;; ;;; ;; ;;; ;; ;; ;; ; ;;; ;;; ;; ;;; ;; ;; ;; ;
206	187, 202, 205	3eqtr4ri 2655	. . . . . . 7 ;;; ;;; ;; ;;; ;; ;; ;; ; ;;; ;; ; ;; ; ;;
207	167, 206	eqtr4i 2647	. . . . . 6 ;;; ;;; ;;; ;;; ;; ;;; ;; ;; ;; ;
208	174	nn0rei 11303	. . . . . . . 8 ;;;
209	176	nn0rei 11303	. . . . . . . 8 ;;;
210	208, 209	remulcli 10054	. . . . . . 7 ;;; ;;;
211	139	nn0rei 11303	. . . . . . . . . . 11 ;;
212		1re 10039	. . . . . . . . . . 11
213	211, 212	readdcli 10053	. . . . . . . . . 10 ;;
214	213, 209	remulcli 10054	. . . . . . . . 9 ;; ;;;
215	102	nn0rei 11303	. . . . . . . . . . 11 ;;
216	17	nn0rei 11303	. . . . . . . . . . 11 ;;
217	215, 216	remulcli 10054	. . . . . . . . . 10 ;; ;;
218	61	nn0rei 11303	. . . . . . . . . . . 12
219	215, 218	remulcli 10054	. . . . . . . . . . 11 ;;
220	62, 63	deccl 11512	. . . . . . . . . . . 12 ;
221	220	nn0rei 11303	. . . . . . . . . . 11 ;
222	219, 221	readdcli 10053	. . . . . . . . . 10 ;; ;
223	217, 222	readdcli 10053	. . . . . . . . 9 ;; ;; ;; ;
224	214, 223	resubcli 10343	. . . . . . . 8 ;; ;;; ;; ;; ;; ;
225	219	recni 10052	. . . . . . . . . . . 12 ;;
226	221	recni 10052	. . . . . . . . . . . 12 ;
227	182, 225, 226	addassi 10048	. . . . . . . . . . 11 ;; ;; ;; ; ;; ;; ;; ;
228	218	recni 10052	. . . . . . . . . . . . . 14
229	103, 181, 228	adddii 10050	. . . . . . . . . . . . 13 ;; ;; ;; ;; ;;
230		dpmul4.1	. . . . . . . . . . . . . 14 ;; ;;;
231	230	oveq2i 6661	. . . . . . . . . . . . 13 ;; ;; ;; ;;;
232	229, 231	eqtr3i 2646	. . . . . . . . . . . 12 ;; ;; ;; ;; ;;;
233	232	oveq1i 6660	. . . . . . . . . . 11 ;; ;; ;; ; ;; ;;; ;
234	227, 233	eqtr3i 2646	. . . . . . . . . 10 ;; ;; ;; ; ;; ;;; ;
235		dpmul4.u	. . . . . . . . . . . . 13
236		dpmul4.a	. . . . . . . . . . . . 13 ;
237		dpmul4.b	. . . . . . . . . . . . 13 ;
238		dpmul4.c	. . . . . . . . . . . . 13 ;
239	235, 88, 62, 101, 63, 101, 236, 237, 238	3decltc 11538	. . . . . . . . . . . 12 ;; ;;;
240	235, 62	deccl 11512	. . . . . . . . . . . . . . 15 ;
241	240, 63	deccl 11512	. . . . . . . . . . . . . 14 ;;
242	241	nn0rei 11303	. . . . . . . . . . . . 13 ;;
243	211, 209	remulcli 10054	. . . . . . . . . . . . 13 ;; ;;;
244	242, 209, 243	ltadd2i 10168	. . . . . . . . . . . 12 ;; ;;; ;; ;;; ;; ;; ;;; ;;;
245	239, 244	mpbi 220	. . . . . . . . . . 11 ;; ;;; ;; ;; ;;; ;;;
246	140, 177	mulcli 10045	. . . . . . . . . . . . 13 ;; ;;;
247	235	nn0cni 11304	. . . . . . . . . . . . . 14
248	103, 247	mulcli 10045	. . . . . . . . . . . . 13 ;;
249	246, 248, 226	addassi 10048	. . . . . . . . . . . 12 ;; ;;; ;; ; ;; ;;; ;; ;
250		dfdec10 11497	. . . . . . . . . . . . . . 15 ;;; ; ;;
251	250	oveq2i 6661	. . . . . . . . . . . . . 14 ;; ;;; ;; ; ;;
252	24, 140	mulcli 10045	. . . . . . . . . . . . . . 15 ; ;;
253	103, 252, 247	adddii 10050	. . . . . . . . . . . . . 14 ;; ; ;; ;; ; ;; ;;
254	140, 177	mulcomi 10046	. . . . . . . . . . . . . . . 16 ;; ;;; ;;; ;;
255	24, 103	mulcomi 10046	. . . . . . . . . . . . . . . . . 18 ; ;; ;; ;
256	255, 195	eqtr3i 2646	. . . . . . . . . . . . . . . . 17 ;; ; ;;;
257	256	oveq1i 6660	. . . . . . . . . . . . . . . 16 ;; ; ;; ;;; ;;
258	103, 24, 140	mulassi 10049	. . . . . . . . . . . . . . . 16 ;; ; ;; ;; ; ;;
259	254, 257, 258	3eqtr2ri 2651	. . . . . . . . . . . . . . 15 ;; ; ;; ;; ;;;
260	259	oveq1i 6660	. . . . . . . . . . . . . 14 ;; ; ;; ;; ;; ;;; ;;
261	251, 253, 260	3eqtri 2648	. . . . . . . . . . . . 13 ;; ;;; ;; ;;; ;;
262	261	oveq1i 6660	. . . . . . . . . . . 12 ;; ;;; ; ;; ;;; ;; ;
263	235, 62, 64	dfdec100 29576	. . . . . . . . . . . . 13 ;; ;; ;
264	263	oveq2i 6661	. . . . . . . . . . . 12 ;; ;;; ;; ;; ;;; ;; ;
265	249, 262, 264	3eqtr4i 2654	. . . . . . . . . . 11 ;; ;;; ; ;; ;;; ;;
266	140, 141, 177	adddiri 10051	. . . . . . . . . . . 12 ;; ;;; ;; ;;; ;;;
267	177	mulid2i 10043	. . . . . . . . . . . . 13 ;;; ;;;
268	267	oveq2i 6661	. . . . . . . . . . . 12 ;; ;;; ;;; ;; ;;; ;;;
269	266, 268	eqtri 2644	. . . . . . . . . . 11 ;; ;;; ;; ;;; ;;;
270	245, 265, 269	3brtr4i 4683	. . . . . . . . . 10 ;; ;;; ; ;; ;;;
271	234, 270	eqbrtri 4674	. . . . . . . . 9 ;; ;; ;; ; ;; ;;;
272	223, 214	posdifi 10578	. . . . . . . . 9 ;; ;; ;; ; ;; ;;; ;; ;;; ;; ;; ;; ;
273	271, 272	mpbi 220	. . . . . . . 8 ;; ;;; ;; ;; ;; ;
274		elrp 11834	. . . . . . . 8 ;; ;;; ;; ;; ;; ; ;; ;;; ;; ;; ;; ; $/\$ ;; ;;; ;; ;; ;; ;
275	224, 273, 274	mpbir2an 955	. . . . . . 7 ;; ;;; ;; ;; ;; ;
276		ltsubrp 11866	. . . . . . 7 ;;; ;;; $/\$ ;; ;;; ;; ;; ;; ; ;;; ;;; ;; ;;; ;; ;; ;; ; ;;; ;;;
277	210, 275, 276	mp2an 708	. . . . . 6 ;;; ;;; ;; ;;; ;; ;; ;; ; ;;; ;;;
278	207, 277	eqbrtri 4674	. . . . 5 ;;; ;;; ;;; ;;;
279	3, 4	deccl 11512	. . . . . . . . 9 ;;
280	279, 5	deccl 11512	. . . . . . . 8 ;;;
281	280	nn0rei 11303	. . . . . . 7 ;;;
282	9, 10	deccl 11512	. . . . . . . . 9 ;;
283	282, 11	deccl 11512	. . . . . . . 8 ;;;
284	283	nn0rei 11303	. . . . . . 7 ;;;
285	281, 284	remulcli 10054	. . . . . 6 ;;; ;;;
286	23	decnncl2 11525	. . . . . . . . 9 ;;
287	286	decnncl2 11525	. . . . . . . 8 ;;;
288	287	nngt0i 11054	. . . . . . 7 ;;;
289	209, 288	pm3.2i 471	. . . . . 6 ;;; $/\$ ;;;
290		ltdiv1 10887	. . . . . 6 ;;; ;;; $/\$ ;;; ;;; $/\$ ;;; $/\$ ;;; ;;; ;;; ;;; ;;; ;;; ;;; ;;; ;;; ;;; ;;;
291	285, 210, 289, 290	mp3an 1424	. . . . 5 ;;; ;;; ;;; ;;; ;;; ;;; ;;; ;;; ;;; ;;;
292	278, 291	mpbi 220	. . . 4 ;;; ;;; ;;; ;;; ;;; ;;;
293	280	nn0cni 11304	. . . . . 6 ;;;
294	283	nn0cni 11304	. . . . . 6 ;;;
295	209, 288	gt0ne0ii 10564	. . . . . 6 ;;;
296	293, 294, 177, 295	div23i 10783	. . . . 5 ;;; ;;; ;;; ;;; ;;; ;;;
297	1, 2, 4, 48	dpmul1000 29607	. . . . . . . 8 __ ;;; ;;;
298	297	oveq1i 6660	. . . . . . 7 __ ;;; ;;; ;;; ;;;
299	4	nn0rei 11303	. . . . . . . . . . . 12
300		dp2cl 29587	. . . . . . . . . . . 12 $/\$ _
301	299, 48, 300	mp2an 708	. . . . . . . . . . 11 _
302		dp2cl 29587	. . . . . . . . . . 11 $/\$ _ __
303	19, 301, 302	mp2an 708	. . . . . . . . . 10 __
304		dpcl 29598	. . . . . . . . . 10 $/\$ __ __
305	1, 303, 304	mp2an 708	. . . . . . . . 9 __
306	305	recni 10052	. . . . . . . 8 __
307	306, 177, 295	divcan4i 10772	. . . . . . 7 __ ;;; ;;; __
308	298, 307	eqtr3i 2646	. . . . . 6 ;;; ;;; __
309	308	oveq1i 6660	. . . . 5 ;;; ;;; ;;; __ ;;;
310	296, 309	eqtri 2644	. . . 4 ;;; ;;; ;;; __ ;;;
311	175, 177, 295	divcan4i 10772	. . . 4 ;;; ;;; ;;; ;;;
312	292, 310, 311	3brtr3i 4682	. . 3 __ ;;; ;;;
313	305, 284	remulcli 10054	. . . 4 __ ;;;
314		ltdiv1 10887	. . . 4 __ ;;; $/\$ ;;; $/\$ ;;; $/\$ ;;; __ ;;; ;;; __ ;;; ;;; ;;; ;;;
315	313, 208, 289, 314	mp3an 1424	. . 3 __ ;;; ;;; __ ;;; ;;; ;;; ;;;
316	312, 315	mpbi 220	. 2 __ ;;; ;;; ;;; ;;;
317	306, 294, 177, 295	divassi 10781	. . 3 __ ;;; ;;; __ ;;; ;;;
318	7, 8, 10, 52	dpmul1000 29607	. . . . . 6 __ ;;; ;;;
319	318	oveq1i 6660	. . . . 5 __ ;;; ;;; ;;; ;;;
320	10	nn0rei 11303	. . . . . . . . . 10
321		dp2cl 29587	. . . . . . . . . 10 $/\$ _
322	320, 52, 321	mp2an 708	. . . . . . . . 9 _
323		dp2cl 29587	. . . . . . . . 9 $/\$ _ __
324	25, 322, 323	mp2an 708	. . . . . . . 8 __
325		dpcl 29598	. . . . . . . 8 $/\$ __ __
326	7, 324, 325	mp2an 708	. . . . . . 7 __
327	326	recni 10052	. . . . . 6 __
328	327, 177, 295	divcan4i 10772	. . . . 5 __ ;;; ;;; __
329	319, 328	eqtr3i 2646	. . . 4 ;;; ;;; __
330	329	oveq2i 6661	. . 3 __ ;;; ;;; __ __
331	317, 330	eqtri 2644	. 2 __ ;;; ;;; __ __
332	173	nn0rei 11303	. . . . 5
333	168, 169, 171, 332	dpmul1000 29607	. . . 4 __ ;;; ;;;
334	333	oveq1i 6660	. . 3 __ ;;; ;;; ;;; ;;;
335	169	nn0rei 11303	. . . . . . 7
336	171	nn0rei 11303	. . . . . . . 8
337		dp2cl 29587	. . . . . . . 8 $/\$ _
338	336, 332, 337	mp2an 708	. . . . . . 7 _
339		dp2cl 29587	. . . . . . 7 $/\$ _ __
340	335, 338, 339	mp2an 708	. . . . . 6 __
341		dpcl 29598	. . . . . 6 $/\$ __ __
342	168, 340, 341	mp2an 708	. . . . 5 __
343	342	recni 10052	. . . 4 __
344	343, 177, 295	divcan4i 10772	. . 3 __ ;;; ;;; __
345	334, 344	eqtr3i 2646	. 2 ;;; ;;; __
346	316, 331, 345	3brtr3i 4682	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

cmin 10266

cdiv 10684

c2 11070

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: hgt750lem2 30730

W3C validator