quart1lem - Metamath Proof Explorer

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

Theorem quart1lem 22250

Description: Lemma for quart1 22251. (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 9406	. . . . . . . . . 10
5	4	halfcld 10569	. . . . . . . . 9
6	1, 5	subcld 9719	. . . . . . . 8
7		3nn0 10597	. . . . . . . . . 10
8		expcl 11883	. . . . . . . . . 10 $/\$
9	2, 7, 8	sylancl 662	. . . . . . . . 9
10		8cn 10407	. . . . . . . . . 10
11	10	a1i 11	. . . . . . . . 9
12		8nn 10485	. . . . . . . . . . 11
13	12	nnne0i 10356	. . . . . . . . . 10
14	13	a1i 11	. . . . . . . . 9
15	9, 11, 14	divcld 10107	. . . . . . . 8
16		4cn 10399	. . . . . . . . . 10
17	16	a1i 11	. . . . . . . . 9
18		4ne0 10418	. . . . . . . . . 10
19	18	a1i 11	. . . . . . . . 9
20	2, 17, 19	divcld 10107	. . . . . . . 8
21	6, 15, 20	adddird 9411	. . . . . . 7
22		quart1.q	. . . . . . . 8
23	22	oveq1d 6106	. . . . . . 7
24	1, 2, 17, 19	divassd 10142	. . . . . . . . . 10
25	2	sqvald 12005	. . . . . . . . . . . . . . 15
26	25	oveq1d 6106	. . . . . . . . . . . . . 14
27	2, 2, 3	mul32d 9579	. . . . . . . . . . . . . 14
28	26, 27	eqtrd 2475	. . . . . . . . . . . . 13
29	28	oveq1d 6106	. . . . . . . . . . . 12
30		2cn 10392	. . . . . . . . . . . . . 14
31		4t2e8 10475	. . . . . . . . . . . . . 14
32	16, 30, 31	mulcomli 9393	. . . . . . . . . . . . 13
33	32	oveq2i 6102	. . . . . . . . . . . 12
34	29, 33	syl6eqr 2493	. . . . . . . . . . 11
35	30	a1i 11	. . . . . . . . . . . 12
36		2ne0 10414	. . . . . . . . . . . . 13
37	36	a1i 11	. . . . . . . . . . . 12
38	4, 35, 2, 17, 37, 19	divmuldivd 10148	. . . . . . . . . . 11
39	34, 38	eqtr4d 2478	. . . . . . . . . 10
40	24, 39	oveq12d 6109	. . . . . . . . 9
41	1, 5, 20	subdird 9801	. . . . . . . . 9
42	40, 41	eqtr4d 2478	. . . . . . . 8
43		df-4 10382	. . . . . . . . . . . . . 14
44	43	oveq2i 6102	. . . . . . . . . . . . 13
45		expp1 11872	. . . . . . . . . . . . . 14 $/\$
46	2, 7, 45	sylancl 662	. . . . . . . . . . . . 13
47	44, 46	syl5eq 2487	. . . . . . . . . . . 12
48	47	oveq1d 6106	. . . . . . . . . . 11
49	9, 2, 11, 14	div23d 10144	. . . . . . . . . . 11
50	48, 49	eqtrd 2475	. . . . . . . . . 10
51	50	oveq1d 6106	. . . . . . . . 9
52	15, 2, 17, 19	divassd 10142	. . . . . . . . 9
53	51, 52	eqtrd 2475	. . . . . . . 8
54	42, 53	oveq12d 6109	. . . . . . 7
55	21, 23, 54	3eqtr4d 2485	. . . . . 6
56	1, 2	mulcld 9406	. . . . . . . 8
57	56, 17, 19	divcld 10107	. . . . . . 7
58	2	sqcld 12006	. . . . . . . . 9
59	58, 3	mulcld 9406	. . . . . . . 8
60	59, 11, 14	divcld 10107	. . . . . . 7
61		4nn0 10598	. . . . . . . . . 10
62		expcl 11883	. . . . . . . . . 10 $/\$
63	2, 61, 62	sylancl 662	. . . . . . . . 9
64	63, 11, 14	divcld 10107	. . . . . . . 8
65	64, 17, 19	divcld 10107	. . . . . . 7
66	57, 60, 65	subadd23d 9741	. . . . . 6
67	65, 60	subcld 9719	. . . . . . 7
68	57, 67	addcomd 9571	. . . . . 6
69	55, 66, 68	3eqtrd 2479	. . . . 5
70		quart1.r	. . . . . 6 ; ;;
71		quart1.d	. . . . . . 7
72		1nn0 10595	. . . . . . . . . . . 12
73		6nn 10483	. . . . . . . . . . . 12
74	72, 73	decnncl 10768	. . . . . . . . . . 11 ;
75	74	nncni 10332	. . . . . . . . . 10 ;
76	75	a1i 11	. . . . . . . . 9 ;
77	74	nnne0i 10356	. . . . . . . . . 10 ;
78	77	a1i 11	. . . . . . . . 9 ;
79	59, 76, 78	divcld 10107	. . . . . . . 8 ;
80		3cn 10396	. . . . . . . . . 10
81		2nn0 10596	. . . . . . . . . . . . 13
82		5nn0 10599	. . . . . . . . . . . . 13
83	81, 82	deccl 10769	. . . . . . . . . . . 12 ;
84	83, 73	decnncl 10768	. . . . . . . . . . 11 ;;
85	84	nncni 10332	. . . . . . . . . 10 ;;
86	84	nnne0i 10356	. . . . . . . . . 10 ;;
87	80, 85, 86	divcli 10073	. . . . . . . . 9 ;;
88		mulcl 9366	. . . . . . . . 9 ;; $/\$ ;;
89	87, 63, 88	sylancr 663	. . . . . . . 8 ;;
90	79, 89	subcld 9719	. . . . . . 7 ; ;;
91	71, 90, 57	addsubd 9740	. . . . . 6 ; ;; ; ;;
92	70, 91	eqtr4d 2478	. . . . 5 ; ;;
93	69, 92	oveq12d 6109	. . . 4 ; ;;
94	71, 90	addcld 9405	. . . . 5 ; ;;
95	67, 57, 94	ppncand 9759	. . . 4 ; ;; ; ;;
96	67, 71, 90	add12d 9591	. . . . 5 ; ;; ; ;;
97	60, 89	addcld 9405	. . . . . . . 8 ;;
98	65, 79	addcld 9405	. . . . . . . 8 ;
99	97, 98	negsubdi2d 9735	. . . . . . 7 ;; ; ; ;;
100	65, 79	addcomd 9571	. . . . . . . . . 10 ; ;
101	100	oveq2d 6107	. . . . . . . . 9 ;; ; ;; ;
102	60, 89, 79, 65	addsub4d 9766	. . . . . . . . 9 ;; ; ; ;;
103	80	a1i 11	. . . . . . . . . . . . . . . 16
104	85	a1i 11	. . . . . . . . . . . . . . . 16 ;;
105	86	a1i 11	. . . . . . . . . . . . . . . 16 ;;
106	103, 63, 104, 105	divassd 10142	. . . . . . . . . . . . . . 15 ;; ;;
107	103, 63, 104, 105	div23d 10144	. . . . . . . . . . . . . . 15 ;; ;;
108		1p2e3 10446	. . . . . . . . . . . . . . . . . 18
109	108	oveq1i 6101	. . . . . . . . . . . . . . . . 17 ;; ;;
110		ax-1cn 9340	. . . . . . . . . . . . . . . . . . 19
111	110	a1i 11	. . . . . . . . . . . . . . . . . 18
112	63, 104, 105	divcld 10107	. . . . . . . . . . . . . . . . . 18 ;;
113	111, 35, 112	adddird 9411	. . . . . . . . . . . . . . . . 17 ;; ;; ;;
114	109, 113	syl5eqr 2489	. . . . . . . . . . . . . . . 16 ;; ;; ;;
115	112	mulid2d 9404	. . . . . . . . . . . . . . . . 17 ;; ;;
116	115	oveq1d 6106	. . . . . . . . . . . . . . . 16 ;; ;; ;; ;;
117	114, 116	eqtrd 2475	. . . . . . . . . . . . . . 15 ;; ;; ;;
118	106, 107, 117	3eqtr3d 2483	. . . . . . . . . . . . . 14 ;; ;; ;;
119	43	oveq1i 6101	. . . . . . . . . . . . . . . 16
120	65, 17, 19	divcld 10107	. . . . . . . . . . . . . . . . 17
121	103, 111, 120	adddird 9411	. . . . . . . . . . . . . . . 16
122	119, 121	syl5eq 2487	. . . . . . . . . . . . . . 15
123	65, 17, 19	divcan2d 10109	. . . . . . . . . . . . . . 15
124	120	mulid2d 9404	. . . . . . . . . . . . . . . . 17
125	64, 17, 17, 19, 19	divdiv1d 10138	. . . . . . . . . . . . . . . . . 18
126		4t4e16 10828	. . . . . . . . . . . . . . . . . . 19 ;
127	126	oveq2i 6102	. . . . . . . . . . . . . . . . . 18 ;
128	125, 127	syl6eq 2491	. . . . . . . . . . . . . . . . 17 ;
129	63, 11, 76, 14, 78	divdiv1d 10138	. . . . . . . . . . . . . . . . . 18 ; ;
130	10, 75	mulcli 9391	. . . . . . . . . . . . . . . . . . . . 21 ;
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
132	10, 75, 13, 77	mulne0i 9979	. . . . . . . . . . . . . . . . . . . . 21 ;
133	132	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
134	63, 131, 133	divcld 10107	. . . . . . . . . . . . . . . . . . 19 ;
135	134, 35, 37	divcan2d 10109	. . . . . . . . . . . . . . . . . 18 ; ;
136	63, 131, 35, 133, 37	divdiv1d 10138	. . . . . . . . . . . . . . . . . . . 20 ; ;
137	10, 75, 30	mul32i 9565	. . . . . . . . . . . . . . . . . . . . . 22 ; ;
138		2exp4 14114	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
139		8t2e16 10843	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
140	138, 139	eqtr4i 2466	. . . . . . . . . . . . . . . . . . . . . . 23
141	140, 138	oveq12i 6103	. . . . . . . . . . . . . . . . . . . . . 22 ;
142		4p4e8 10458	. . . . . . . . . . . . . . . . . . . . . . . 24
143	142	oveq2i 6102	. . . . . . . . . . . . . . . . . . . . . . 23
144		expadd 11906	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
145	30, 61, 61, 144	mp3an 1314	. . . . . . . . . . . . . . . . . . . . . . 23
146		2exp8 14116	. . . . . . . . . . . . . . . . . . . . . . 23 ;;
147	143, 145, 146	3eqtr3i 2471	. . . . . . . . . . . . . . . . . . . . . 22 ;;
148	137, 141, 147	3eqtr2i 2469	. . . . . . . . . . . . . . . . . . . . 21 ; ;;
149	148	oveq2i 6102	. . . . . . . . . . . . . . . . . . . 20 ; ;;
150	136, 149	syl6eq 2491	. . . . . . . . . . . . . . . . . . 19 ; ;;
151	150	oveq2d 6107	. . . . . . . . . . . . . . . . . 18 ; ;;
152	129, 135, 151	3eqtr2d 2481	. . . . . . . . . . . . . . . . 17 ; ;;
153	124, 128, 152	3eqtrd 2479	. . . . . . . . . . . . . . . 16 ;;
154	153	oveq2d 6107	. . . . . . . . . . . . . . 15 ;;
155	122, 123, 154	3eqtr3d 2483	. . . . . . . . . . . . . 14 ;;
156	118, 155	oveq12d 6109	. . . . . . . . . . . . 13 ;; ;; ;; ;;
157		mulcl 9366	. . . . . . . . . . . . . . 15 $/\$
158	80, 120, 157	sylancr 663	. . . . . . . . . . . . . 14
159		mulcl 9366	. . . . . . . . . . . . . . 15 $/\$ ;; ;;
160	30, 112, 159	sylancr 663	. . . . . . . . . . . . . 14 ;;
161	112, 158, 160	pnpcan2d 9757	. . . . . . . . . . . . 13 ;; ;; ;; ;;
162	156, 161	eqtrd 2475	. . . . . . . . . . . 12 ;; ;;
163	162	oveq2d 6107	. . . . . . . . . . 11 ; ;; ; ;;
164	79, 112, 158	addsub12d 9742	. . . . . . . . . . 11 ; ;; ;; ;
165	163, 164	eqtrd 2475	. . . . . . . . . 10 ; ;; ;; ;
166	59, 11, 35, 14, 37	divdiv1d 10138	. . . . . . . . . . . . . . . 16
167	139	oveq2i 6102	. . . . . . . . . . . . . . . 16 ;
168	166, 167	syl6eq 2491	. . . . . . . . . . . . . . 15 ;
169	168	oveq2d 6107	. . . . . . . . . . . . . 14 ;
170	60, 35, 37	divcan2d 10109	. . . . . . . . . . . . . 14
171	79	2timesd 10567	. . . . . . . . . . . . . 14 ; ; ;
172	169, 170, 171	3eqtr3d 2483	. . . . . . . . . . . . 13 ; ;
173	172	oveq1d 6106	. . . . . . . . . . . 12 ; ; ; ;
174	79, 79	pncand 9720	. . . . . . . . . . . 12 ; ; ; ;
175	173, 174	eqtrd 2475	. . . . . . . . . . 11 ; ;
176	175	oveq1d 6106	. . . . . . . . . 10 ; ;; ; ;;
177		quart1.p	. . . . . . . . . . . . 13
178	177	oveq1d 6106	. . . . . . . . . . . 12
179	80, 10, 13	divcli 10073	. . . . . . . . . . . . . 14
180		mulcl 9366	. . . . . . . . . . . . . 14 $/\$
181	179, 58, 180	sylancr 663	. . . . . . . . . . . . 13
182	20	sqcld 12006	. . . . . . . . . . . . 13
183	3, 181, 182	subdird 9801	. . . . . . . . . . . 12
184	2, 17, 19	sqdivd 12021	. . . . . . . . . . . . . . . 16
185	16	sqvali 11945	. . . . . . . . . . . . . . . . . 18
186	185, 126	eqtri 2463	. . . . . . . . . . . . . . . . 17 ;
187	186	oveq2i 6102	. . . . . . . . . . . . . . . 16 ;
188	184, 187	syl6eq 2491	. . . . . . . . . . . . . . 15 ;
189	188	oveq2d 6107	. . . . . . . . . . . . . 14 ;
190	3, 58, 76, 78	divassd 10142	. . . . . . . . . . . . . 14 ; ;
191	3, 58	mulcomd 9407	. . . . . . . . . . . . . . 15
192	191	oveq1d 6106	. . . . . . . . . . . . . 14 ; ;
193	189, 190, 192	3eqtr2d 2481	. . . . . . . . . . . . 13 ;
194	179	a1i 11	. . . . . . . . . . . . . . . . . 18
195	194, 58, 58	mulassd 9409	. . . . . . . . . . . . . . . . 17
196	103, 63, 11, 14	div23d 10144	. . . . . . . . . . . . . . . . . 18
197		2p2e4 10439	. . . . . . . . . . . . . . . . . . . . 21
198	197	oveq2i 6102	. . . . . . . . . . . . . . . . . . . 20
199	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
200	2, 199, 199	expaddd 12010	. . . . . . . . . . . . . . . . . . . 20
201	198, 200	syl5eqr 2489	. . . . . . . . . . . . . . . . . . 19
202	201	oveq2d 6107	. . . . . . . . . . . . . . . . . 18
203	196, 202	eqtrd 2475	. . . . . . . . . . . . . . . . 17
204	103, 63, 11, 14	divassd 10142	. . . . . . . . . . . . . . . . 17
205	195, 203, 204	3eqtr2d 2481	. . . . . . . . . . . . . . . 16
206	205	oveq1d 6106	. . . . . . . . . . . . . . 15
207	186, 76	syl5eqel 2527	. . . . . . . . . . . . . . . 16
208	186, 77	eqnetri 2625	. . . . . . . . . . . . . . . . 17
209	208	a1i 11	. . . . . . . . . . . . . . . 16
210	181, 58, 207, 209	divassd 10142	. . . . . . . . . . . . . . 15
211	103, 64, 207, 209	divassd 10142	. . . . . . . . . . . . . . 15
212	206, 210, 211	3eqtr3d 2483	. . . . . . . . . . . . . 14
213	184	oveq2d 6107	. . . . . . . . . . . . . 14
214	186	oveq2i 6102	. . . . . . . . . . . . . . . 16 ;
215	128, 214	syl6eqr 2493	. . . . . . . . . . . . . . 15
216	215	oveq2d 6107	. . . . . . . . . . . . . 14
217	212, 213, 216	3eqtr4d 2485	. . . . . . . . . . . . 13
218	193, 217	oveq12d 6109	. . . . . . . . . . . 12 ;
219	178, 183, 218	3eqtrd 2479	. . . . . . . . . . 11 ;
220	219	oveq2d 6107	. . . . . . . . . 10 ;; ;; ;
221	165, 176, 220	3eqtr4d 2485	. . . . . . . . 9 ; ;; ;;
222	101, 102, 221	3eqtrd 2479	. . . . . . . 8 ;; ; ;;
223	222	negeqd 9604	. . . . . . 7 ;; ; ;;
224	65, 79, 60, 89	addsub4d 9766	. . . . . . 7 ; ;; ; ;;
225	99, 223, 224	3eqtr3rd 2484	. . . . . 6 ; ;; ;;
226	225	oveq2d 6107	. . . . 5 ; ;; ;;
227	3, 181	subcld 9719	. . . . . . . . 9
228	177, 227	eqeltrd 2517	. . . . . . . 8
229	228, 182	mulcld 9406	. . . . . . 7
230	112, 229	addcld 9405	. . . . . 6 ;;
231	71, 230	negsubd 9725	. . . . 5 ;; ;;
232	96, 226, 231	3eqtrd 2479	. . . 4 ; ;; ;;
233	93, 95, 232	3eqtrd 2479	. . 3 ;;
234	233	oveq2d 6107	. 2 ;; ;; ;;
235	230, 71	pncan3d 9722	. 2 ;; ;;
236	234, 235	eqtr2d 2476	1 ;;

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1369

wcel 1756

wne 2606 (class class class)co 6091

cc 9280

cc0 9282

c1 9283

caddc 9285

cmul 9287

cmin 9595

cneg 9596

cdiv 9993

c2 10371

c3 10372

c4 10373

c5 10374

c6 10375

c8 10377

cn0 10579 ;cdc 10755

cexp 11865

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-cnex 9338 ax-resscn 9339 ax-1cn 9340 ax-icn 9341 ax-addcl 9342 ax-addrcl 9343 ax-mulcl 9344 ax-mulrcl 9345 ax-mulcom 9346 ax-addass 9347 ax-mulass 9348 ax-distr 9349 ax-i2m1 9350 ax-1ne0 9351 ax-1rid 9352 ax-rnegex 9353 ax-rrecex 9354 ax-cnre 9355 ax-pre-lttri 9356 ax-pre-lttrn 9357 ax-pre-ltadd 9358 ax-pre-mulgt0 9359

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-nel 2609 df-ral 2720 df-rex 2721 df-reu 2722 df-rmo 2723 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-om 6477 df-2nd 6578 df-recs 6832 df-rdg 6866 df-er 7101 df-en 7311 df-dom 7312 df-sdom 7313 df-pnf 9420 df-mnf 9421 df-xr 9422 df-ltxr 9423 df-le 9424 df-sub 9597 df-neg 9598 df-div 9994 df-nn 10323 df-2 10380 df-3 10381 df-4 10382 df-5 10383 df-6 10384 df-7 10385 df-8 10386 df-9 10387 df-10 10388 df-n0 10580 df-z 10647 df-dec 10756 df-uz 10862 df-seq 11807 df-exp 11866

This theorem is referenced by: quart1 22251

W3C validator