quart1lem - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > quart1lem		Structured version Unicode version

Theorem quart1lem 23162

Description: Lemma for quart1 23163. (Contributed by Mario Carneiro, 6-May-2015.)

**Hypotheses**
Ref	Expression
quart1.a
quart1.b
quart1.c
quart1.d
quart1.p
quart1.q
quart1.r	; ;;
quart1.x
quart1.y

**Assertion**
Ref	Expression
quart1lem	;;

**Proof of Theorem quart1lem**
Step	Hyp	Ref	Expression
1		quart1.c	. . . . . . . . 9
2		quart1.a	. . . . . . . . . . 11
3		quart1.b	. . . . . . . . . . 11
4	2, 3	mulcld 9619	. . . . . . . . . 10
5	4	halfcld 10790	. . . . . . . . 9
6	1, 5	subcld 9936	. . . . . . . 8
7		3nn0 10820	. . . . . . . . . 10
8		expcl 12165	. . . . . . . . . 10 $/\$
9	2, 7, 8	sylancl 662	. . . . . . . . 9
10		8cn 10628	. . . . . . . . . 10
11	10	a1i 11	. . . . . . . . 9
12		8nn 10706	. . . . . . . . . . 11
13	12	nnne0i 10577	. . . . . . . . . 10
14	13	a1i 11	. . . . . . . . 9
15	9, 11, 14	divcld 10327	. . . . . . . 8
16		4cn 10620	. . . . . . . . . 10
17	16	a1i 11	. . . . . . . . 9
18		4ne0 10639	. . . . . . . . . 10
19	18	a1i 11	. . . . . . . . 9
20	2, 17, 19	divcld 10327	. . . . . . . 8
21	6, 15, 20	adddird 9624	. . . . . . 7
22		quart1.q	. . . . . . . 8
23	22	oveq1d 6296	. . . . . . 7
24	1, 2, 17, 19	divassd 10362	. . . . . . . . . 10
25	2	sqvald 12288	. . . . . . . . . . . . . . 15
26	25	oveq1d 6296	. . . . . . . . . . . . . 14
27	2, 2, 3	mul32d 9793	. . . . . . . . . . . . . 14
28	26, 27	eqtrd 2484	. . . . . . . . . . . . 13
29	28	oveq1d 6296	. . . . . . . . . . . 12
30		2cn 10613	. . . . . . . . . . . . . 14
31		4t2e8 10696	. . . . . . . . . . . . . 14
32	16, 30, 31	mulcomli 9606	. . . . . . . . . . . . 13
33	32	oveq2i 6292	. . . . . . . . . . . 12
34	29, 33	syl6eqr 2502	. . . . . . . . . . 11
35	30	a1i 11	. . . . . . . . . . . 12
36		2ne0 10635	. . . . . . . . . . . . 13
37	36	a1i 11	. . . . . . . . . . . 12
38	4, 35, 2, 17, 37, 19	divmuldivd 10368	. . . . . . . . . . 11
39	34, 38	eqtr4d 2487	. . . . . . . . . 10
40	24, 39	oveq12d 6299	. . . . . . . . 9
41	1, 5, 20	subdird 10020	. . . . . . . . 9
42	40, 41	eqtr4d 2487	. . . . . . . 8
43		df-4 10603	. . . . . . . . . . . . . 14
44	43	oveq2i 6292	. . . . . . . . . . . . 13
45		expp1 12154	. . . . . . . . . . . . . 14 $/\$
46	2, 7, 45	sylancl 662	. . . . . . . . . . . . 13
47	44, 46	syl5eq 2496	. . . . . . . . . . . 12
48	47	oveq1d 6296	. . . . . . . . . . 11
49	9, 2, 11, 14	div23d 10364	. . . . . . . . . . 11
50	48, 49	eqtrd 2484	. . . . . . . . . 10
51	50	oveq1d 6296	. . . . . . . . 9
52	15, 2, 17, 19	divassd 10362	. . . . . . . . 9
53	51, 52	eqtrd 2484	. . . . . . . 8
54	42, 53	oveq12d 6299	. . . . . . 7
55	21, 23, 54	3eqtr4d 2494	. . . . . 6
56	1, 2	mulcld 9619	. . . . . . . 8
57	56, 17, 19	divcld 10327	. . . . . . 7
58	2	sqcld 12289	. . . . . . . . 9
59	58, 3	mulcld 9619	. . . . . . . 8
60	59, 11, 14	divcld 10327	. . . . . . 7
61		4nn0 10821	. . . . . . . . . 10
62		expcl 12165	. . . . . . . . . 10 $/\$
63	2, 61, 62	sylancl 662	. . . . . . . . 9
64	63, 11, 14	divcld 10327	. . . . . . . 8
65	64, 17, 19	divcld 10327	. . . . . . 7
66	57, 60, 65	subadd23d 9958	. . . . . 6
67	65, 60	subcld 9936	. . . . . . 7
68	57, 67	addcomd 9785	. . . . . 6
69	55, 66, 68	3eqtrd 2488	. . . . 5
70		quart1.r	. . . . . 6 ; ;;
71		quart1.d	. . . . . . 7
72		1nn0 10818	. . . . . . . . . . . 12
73		6nn 10704	. . . . . . . . . . . 12
74	72, 73	decnncl 10998	. . . . . . . . . . 11 ;
75	74	nncni 10553	. . . . . . . . . 10 ;
76	75	a1i 11	. . . . . . . . 9 ;
77	74	nnne0i 10577	. . . . . . . . . 10 ;
78	77	a1i 11	. . . . . . . . 9 ;
79	59, 76, 78	divcld 10327	. . . . . . . 8 ;
80		3cn 10617	. . . . . . . . . 10
81		2nn0 10819	. . . . . . . . . . . . 13
82		5nn0 10822	. . . . . . . . . . . . 13
83	81, 82	deccl 10999	. . . . . . . . . . . 12 ;
84	83, 73	decnncl 10998	. . . . . . . . . . 11 ;;
85	84	nncni 10553	. . . . . . . . . 10 ;;
86	84	nnne0i 10577	. . . . . . . . . 10 ;;
87	80, 85, 86	divcli 10293	. . . . . . . . 9 ;;
88		mulcl 9579	. . . . . . . . 9 ;; $/\$ ;;
89	87, 63, 88	sylancr 663	. . . . . . . 8 ;;
90	79, 89	subcld 9936	. . . . . . 7 ; ;;
91	71, 90, 57	addsubd 9957	. . . . . 6 ; ;; ; ;;
92	70, 91	eqtr4d 2487	. . . . 5 ; ;;
93	69, 92	oveq12d 6299	. . . 4 ; ;;
94	71, 90	addcld 9618	. . . . 5 ; ;;
95	67, 57, 94	ppncand 9976	. . . 4 ; ;; ; ;;
96	67, 71, 90	add12d 9806	. . . . 5 ; ;; ; ;;
97	60, 89	addcld 9618	. . . . . . . 8 ;;
98	65, 79	addcld 9618	. . . . . . . 8 ;
99	97, 98	negsubdi2d 9952	. . . . . . 7 ;; ; ; ;;
100	65, 79	addcomd 9785	. . . . . . . . . 10 ; ;
101	100	oveq2d 6297	. . . . . . . . 9 ;; ; ;; ;
102	60, 89, 79, 65	addsub4d 9983	. . . . . . . . 9 ;; ; ; ;;
103	80	a1i 11	. . . . . . . . . . . . . . . 16
104	85	a1i 11	. . . . . . . . . . . . . . . 16 ;;
105	86	a1i 11	. . . . . . . . . . . . . . . 16 ;;
106	103, 63, 104, 105	divassd 10362	. . . . . . . . . . . . . . 15 ;; ;;
107	103, 63, 104, 105	div23d 10364	. . . . . . . . . . . . . . 15 ;; ;;
108		1p2e3 10667	. . . . . . . . . . . . . . . . . 18
109	108	oveq1i 6291	. . . . . . . . . . . . . . . . 17 ;; ;;
110		1cnd 9615	. . . . . . . . . . . . . . . . . 18
111	63, 104, 105	divcld 10327	. . . . . . . . . . . . . . . . . 18 ;;
112	110, 35, 111	adddird 9624	. . . . . . . . . . . . . . . . 17 ;; ;; ;;
113	109, 112	syl5eqr 2498	. . . . . . . . . . . . . . . 16 ;; ;; ;;
114	111	mulid2d 9617	. . . . . . . . . . . . . . . . 17 ;; ;;
115	114	oveq1d 6296	. . . . . . . . . . . . . . . 16 ;; ;; ;; ;;
116	113, 115	eqtrd 2484	. . . . . . . . . . . . . . 15 ;; ;; ;;
117	106, 107, 116	3eqtr3d 2492	. . . . . . . . . . . . . 14 ;; ;; ;;
118	43	oveq1i 6291	. . . . . . . . . . . . . . . 16
119	65, 17, 19	divcld 10327	. . . . . . . . . . . . . . . . 17
120	103, 110, 119	adddird 9624	. . . . . . . . . . . . . . . 16
121	118, 120	syl5eq 2496	. . . . . . . . . . . . . . 15
122	65, 17, 19	divcan2d 10329	. . . . . . . . . . . . . . 15
123	119	mulid2d 9617	. . . . . . . . . . . . . . . . 17
124	64, 17, 17, 19, 19	divdiv1d 10358	. . . . . . . . . . . . . . . . . 18
125		4t4e16 11058	. . . . . . . . . . . . . . . . . . 19 ;
126	125	oveq2i 6292	. . . . . . . . . . . . . . . . . 18 ;
127	124, 126	syl6eq 2500	. . . . . . . . . . . . . . . . 17 ;
128	63, 11, 76, 14, 78	divdiv1d 10358	. . . . . . . . . . . . . . . . . 18 ; ;
129	10, 75	mulcli 9604	. . . . . . . . . . . . . . . . . . . . 21 ;
130	129	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
131	10, 75, 13, 77	mulne0i 10199	. . . . . . . . . . . . . . . . . . . . 21 ;
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
133	63, 130, 132	divcld 10327	. . . . . . . . . . . . . . . . . . 19 ;
134	133, 35, 37	divcan2d 10329	. . . . . . . . . . . . . . . . . 18 ; ;
135	63, 130, 35, 132, 37	divdiv1d 10358	. . . . . . . . . . . . . . . . . . . 20 ; ;
136	10, 75, 30	mul32i 9779	. . . . . . . . . . . . . . . . . . . . . 22 ; ;
137		2exp4 14552	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
138		8t2e16 11073	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
139	137, 138	eqtr4i 2475	. . . . . . . . . . . . . . . . . . . . . . 23
140	139, 137	oveq12i 6293	. . . . . . . . . . . . . . . . . . . . . 22 ;
141		4p4e8 10679	. . . . . . . . . . . . . . . . . . . . . . . 24
142	141	oveq2i 6292	. . . . . . . . . . . . . . . . . . . . . . 23
143		expadd 12189	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
144	30, 61, 61, 143	mp3an 1325	. . . . . . . . . . . . . . . . . . . . . . 23
145		2exp8 14555	. . . . . . . . . . . . . . . . . . . . . . 23 ;;
146	142, 144, 145	3eqtr3i 2480	. . . . . . . . . . . . . . . . . . . . . 22 ;;
147	136, 140, 146	3eqtr2i 2478	. . . . . . . . . . . . . . . . . . . . 21 ; ;;
148	147	oveq2i 6292	. . . . . . . . . . . . . . . . . . . 20 ; ;;
149	135, 148	syl6eq 2500	. . . . . . . . . . . . . . . . . . 19 ; ;;
150	149	oveq2d 6297	. . . . . . . . . . . . . . . . . 18 ; ;;
151	128, 134, 150	3eqtr2d 2490	. . . . . . . . . . . . . . . . 17 ; ;;
152	123, 127, 151	3eqtrd 2488	. . . . . . . . . . . . . . . 16 ;;
153	152	oveq2d 6297	. . . . . . . . . . . . . . 15 ;;
154	121, 122, 153	3eqtr3d 2492	. . . . . . . . . . . . . 14 ;;
155	117, 154	oveq12d 6299	. . . . . . . . . . . . 13 ;; ;; ;; ;;
156		mulcl 9579	. . . . . . . . . . . . . . 15 $/\$
157	80, 119, 156	sylancr 663	. . . . . . . . . . . . . 14
158		mulcl 9579	. . . . . . . . . . . . . . 15 $/\$ ;; ;;
159	30, 111, 158	sylancr 663	. . . . . . . . . . . . . 14 ;;
160	111, 157, 159	pnpcan2d 9974	. . . . . . . . . . . . 13 ;; ;; ;; ;;
161	155, 160	eqtrd 2484	. . . . . . . . . . . 12 ;; ;;
162	161	oveq2d 6297	. . . . . . . . . . 11 ; ;; ; ;;
163	79, 111, 157	addsub12d 9959	. . . . . . . . . . 11 ; ;; ;; ;
164	162, 163	eqtrd 2484	. . . . . . . . . 10 ; ;; ;; ;
165	59, 11, 35, 14, 37	divdiv1d 10358	. . . . . . . . . . . . . . . 16
166	138	oveq2i 6292	. . . . . . . . . . . . . . . 16 ;
167	165, 166	syl6eq 2500	. . . . . . . . . . . . . . 15 ;
168	167	oveq2d 6297	. . . . . . . . . . . . . 14 ;
169	60, 35, 37	divcan2d 10329	. . . . . . . . . . . . . 14
170	79	2timesd 10788	. . . . . . . . . . . . . 14 ; ; ;
171	168, 169, 170	3eqtr3d 2492	. . . . . . . . . . . . 13 ; ;
172	171	oveq1d 6296	. . . . . . . . . . . 12 ; ; ; ;
173	79, 79	pncand 9937	. . . . . . . . . . . 12 ; ; ; ;
174	172, 173	eqtrd 2484	. . . . . . . . . . 11 ; ;
175	174	oveq1d 6296	. . . . . . . . . 10 ; ;; ; ;;
176		quart1.p	. . . . . . . . . . . . 13
177	176	oveq1d 6296	. . . . . . . . . . . 12
178	80, 10, 13	divcli 10293	. . . . . . . . . . . . . 14
179		mulcl 9579	. . . . . . . . . . . . . 14 $/\$
180	178, 58, 179	sylancr 663	. . . . . . . . . . . . 13
181	20	sqcld 12289	. . . . . . . . . . . . 13
182	3, 180, 181	subdird 10020	. . . . . . . . . . . 12
183	2, 17, 19	sqdivd 12304	. . . . . . . . . . . . . . . 16
184	16	sqvali 12228	. . . . . . . . . . . . . . . . . 18
185	184, 125	eqtri 2472	. . . . . . . . . . . . . . . . 17 ;
186	185	oveq2i 6292	. . . . . . . . . . . . . . . 16 ;
187	183, 186	syl6eq 2500	. . . . . . . . . . . . . . 15 ;
188	187	oveq2d 6297	. . . . . . . . . . . . . 14 ;
189	3, 58, 76, 78	divassd 10362	. . . . . . . . . . . . . 14 ; ;
190	3, 58	mulcomd 9620	. . . . . . . . . . . . . . 15
191	190	oveq1d 6296	. . . . . . . . . . . . . 14 ; ;
192	188, 189, 191	3eqtr2d 2490	. . . . . . . . . . . . 13 ;
193	178	a1i 11	. . . . . . . . . . . . . . . . . 18
194	193, 58, 58	mulassd 9622	. . . . . . . . . . . . . . . . 17
195	103, 63, 11, 14	div23d 10364	. . . . . . . . . . . . . . . . . 18
196		2p2e4 10660	. . . . . . . . . . . . . . . . . . . . 21
197	196	oveq2i 6292	. . . . . . . . . . . . . . . . . . . 20
198	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
199	2, 198, 198	expaddd 12293	. . . . . . . . . . . . . . . . . . . 20
200	197, 199	syl5eqr 2498	. . . . . . . . . . . . . . . . . . 19
201	200	oveq2d 6297	. . . . . . . . . . . . . . . . . 18
202	195, 201	eqtrd 2484	. . . . . . . . . . . . . . . . 17
203	103, 63, 11, 14	divassd 10362	. . . . . . . . . . . . . . . . 17
204	194, 202, 203	3eqtr2d 2490	. . . . . . . . . . . . . . . 16
205	204	oveq1d 6296	. . . . . . . . . . . . . . 15
206	185, 76	syl5eqel 2535	. . . . . . . . . . . . . . . 16
207	185, 77	eqnetri 2739	. . . . . . . . . . . . . . . . 17
208	207	a1i 11	. . . . . . . . . . . . . . . 16
209	180, 58, 206, 208	divassd 10362	. . . . . . . . . . . . . . 15
210	103, 64, 206, 208	divassd 10362	. . . . . . . . . . . . . . 15
211	205, 209, 210	3eqtr3d 2492	. . . . . . . . . . . . . 14
212	183	oveq2d 6297	. . . . . . . . . . . . . 14
213	185	oveq2i 6292	. . . . . . . . . . . . . . . 16 ;
214	127, 213	syl6eqr 2502	. . . . . . . . . . . . . . 15
215	214	oveq2d 6297	. . . . . . . . . . . . . 14
216	211, 212, 215	3eqtr4d 2494	. . . . . . . . . . . . 13
217	192, 216	oveq12d 6299	. . . . . . . . . . . 12 ;
218	177, 182, 217	3eqtrd 2488	. . . . . . . . . . 11 ;
219	218	oveq2d 6297	. . . . . . . . . 10 ;; ;; ;
220	164, 175, 219	3eqtr4d 2494	. . . . . . . . 9 ; ;; ;;
221	101, 102, 220	3eqtrd 2488	. . . . . . . 8 ;; ; ;;
222	221	negeqd 9819	. . . . . . 7 ;; ; ;;
223	65, 79, 60, 89	addsub4d 9983	. . . . . . 7 ; ;; ; ;;
224	99, 222, 223	3eqtr3rd 2493	. . . . . 6 ; ;; ;;
225	224	oveq2d 6297	. . . . 5 ; ;; ;;
226	3, 180	subcld 9936	. . . . . . . . 9
227	176, 226	eqeltrd 2531	. . . . . . . 8
228	227, 181	mulcld 9619	. . . . . . 7
229	111, 228	addcld 9618	. . . . . 6 ;;
230	71, 229	negsubd 9942	. . . . 5 ;; ;;
231	96, 225, 230	3eqtrd 2488	. . . 4 ; ;; ;;
232	93, 95, 231	3eqtrd 2488	. . 3 ;;
233	232	oveq2d 6297	. 2 ;; ;; ;;
234	229, 71	pncan3d 9939	. 2 ;; ;;
235	233, 234	eqtr2d 2485	1 ;;

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1383

wcel 1804

wne 2638 (class class class)co 6281

cc 9493

cc0 9495

c1 9496

caddc 9498

cmul 9500

cmin 9810

cneg 9811

cdiv 10213

c2 10592

c3 10593

c4 10594

c5 10595

c6 10596

c8 10598

cn0 10802 ;cdc 10985

cexp 12147

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-2nd 6786 df-recs 7044 df-rdg 7078 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10214 df-nn 10544 df-2 10601 df-3 10602 df-4 10603 df-5 10604 df-6 10605 df-7 10606 df-8 10607 df-9 10608 df-10 10609 df-n0 10803 df-z 10872 df-dec 10986 df-uz 11092 df-seq 12089 df-exp 12148

This theorem is referenced by: quart1 23163

W3C validator