quart1lem - Metamath Proof Explorer

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

Theorem quart1lem 22942

Description: Lemma for quart1 22943. (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 9616	. . . . . . . . . 10
5	4	halfcld 10783	. . . . . . . . 9
6	1, 5	subcld 9930	. . . . . . . 8
7		3nn0 10813	. . . . . . . . . 10
8		expcl 12152	. . . . . . . . . 10 $/\$
9	2, 7, 8	sylancl 662	. . . . . . . . 9
10		8cn 10621	. . . . . . . . . 10
11	10	a1i 11	. . . . . . . . 9
12		8nn 10699	. . . . . . . . . . 11
13	12	nnne0i 10570	. . . . . . . . . 10
14	13	a1i 11	. . . . . . . . 9
15	9, 11, 14	divcld 10320	. . . . . . . 8
16		4cn 10613	. . . . . . . . . 10
17	16	a1i 11	. . . . . . . . 9
18		4ne0 10632	. . . . . . . . . 10
19	18	a1i 11	. . . . . . . . 9
20	2, 17, 19	divcld 10320	. . . . . . . 8
21	6, 15, 20	adddird 9621	. . . . . . 7
22		quart1.q	. . . . . . . 8
23	22	oveq1d 6299	. . . . . . 7
24	1, 2, 17, 19	divassd 10355	. . . . . . . . . 10
25	2	sqvald 12275	. . . . . . . . . . . . . . 15
26	25	oveq1d 6299	. . . . . . . . . . . . . 14
27	2, 2, 3	mul32d 9789	. . . . . . . . . . . . . 14
28	26, 27	eqtrd 2508	. . . . . . . . . . . . 13
29	28	oveq1d 6299	. . . . . . . . . . . 12
30		2cn 10606	. . . . . . . . . . . . . 14
31		4t2e8 10689	. . . . . . . . . . . . . 14
32	16, 30, 31	mulcomli 9603	. . . . . . . . . . . . 13
33	32	oveq2i 6295	. . . . . . . . . . . 12
34	29, 33	syl6eqr 2526	. . . . . . . . . . 11
35	30	a1i 11	. . . . . . . . . . . 12
36		2ne0 10628	. . . . . . . . . . . . 13
37	36	a1i 11	. . . . . . . . . . . 12
38	4, 35, 2, 17, 37, 19	divmuldivd 10361	. . . . . . . . . . 11
39	34, 38	eqtr4d 2511	. . . . . . . . . 10
40	24, 39	oveq12d 6302	. . . . . . . . 9
41	1, 5, 20	subdird 10013	. . . . . . . . 9
42	40, 41	eqtr4d 2511	. . . . . . . 8
43		df-4 10596	. . . . . . . . . . . . . 14
44	43	oveq2i 6295	. . . . . . . . . . . . 13
45		expp1 12141	. . . . . . . . . . . . . 14 $/\$
46	2, 7, 45	sylancl 662	. . . . . . . . . . . . 13
47	44, 46	syl5eq 2520	. . . . . . . . . . . 12
48	47	oveq1d 6299	. . . . . . . . . . 11
49	9, 2, 11, 14	div23d 10357	. . . . . . . . . . 11
50	48, 49	eqtrd 2508	. . . . . . . . . 10
51	50	oveq1d 6299	. . . . . . . . 9
52	15, 2, 17, 19	divassd 10355	. . . . . . . . 9
53	51, 52	eqtrd 2508	. . . . . . . 8
54	42, 53	oveq12d 6302	. . . . . . 7
55	21, 23, 54	3eqtr4d 2518	. . . . . 6
56	1, 2	mulcld 9616	. . . . . . . 8
57	56, 17, 19	divcld 10320	. . . . . . 7
58	2	sqcld 12276	. . . . . . . . 9
59	58, 3	mulcld 9616	. . . . . . . 8
60	59, 11, 14	divcld 10320	. . . . . . 7
61		4nn0 10814	. . . . . . . . . 10
62		expcl 12152	. . . . . . . . . 10 $/\$
63	2, 61, 62	sylancl 662	. . . . . . . . 9
64	63, 11, 14	divcld 10320	. . . . . . . 8
65	64, 17, 19	divcld 10320	. . . . . . 7
66	57, 60, 65	subadd23d 9952	. . . . . 6
67	65, 60	subcld 9930	. . . . . . 7
68	57, 67	addcomd 9781	. . . . . 6
69	55, 66, 68	3eqtrd 2512	. . . . 5
70		quart1.r	. . . . . 6 ; ;;
71		quart1.d	. . . . . . 7
72		1nn0 10811	. . . . . . . . . . . 12
73		6nn 10697	. . . . . . . . . . . 12
74	72, 73	decnncl 10989	. . . . . . . . . . 11 ;
75	74	nncni 10546	. . . . . . . . . 10 ;
76	75	a1i 11	. . . . . . . . 9 ;
77	74	nnne0i 10570	. . . . . . . . . 10 ;
78	77	a1i 11	. . . . . . . . 9 ;
79	59, 76, 78	divcld 10320	. . . . . . . 8 ;
80		3cn 10610	. . . . . . . . . 10
81		2nn0 10812	. . . . . . . . . . . . 13
82		5nn0 10815	. . . . . . . . . . . . 13
83	81, 82	deccl 10990	. . . . . . . . . . . 12 ;
84	83, 73	decnncl 10989	. . . . . . . . . . 11 ;;
85	84	nncni 10546	. . . . . . . . . 10 ;;
86	84	nnne0i 10570	. . . . . . . . . 10 ;;
87	80, 85, 86	divcli 10286	. . . . . . . . 9 ;;
88		mulcl 9576	. . . . . . . . 9 ;; $/\$ ;;
89	87, 63, 88	sylancr 663	. . . . . . . 8 ;;
90	79, 89	subcld 9930	. . . . . . 7 ; ;;
91	71, 90, 57	addsubd 9951	. . . . . 6 ; ;; ; ;;
92	70, 91	eqtr4d 2511	. . . . 5 ; ;;
93	69, 92	oveq12d 6302	. . . 4 ; ;;
94	71, 90	addcld 9615	. . . . 5 ; ;;
95	67, 57, 94	ppncand 9970	. . . 4 ; ;; ; ;;
96	67, 71, 90	add12d 9801	. . . . 5 ; ;; ; ;;
97	60, 89	addcld 9615	. . . . . . . 8 ;;
98	65, 79	addcld 9615	. . . . . . . 8 ;
99	97, 98	negsubdi2d 9946	. . . . . . 7 ;; ; ; ;;
100	65, 79	addcomd 9781	. . . . . . . . . 10 ; ;
101	100	oveq2d 6300	. . . . . . . . 9 ;; ; ;; ;
102	60, 89, 79, 65	addsub4d 9977	. . . . . . . . 9 ;; ; ; ;;
103	80	a1i 11	. . . . . . . . . . . . . . . 16
104	85	a1i 11	. . . . . . . . . . . . . . . 16 ;;
105	86	a1i 11	. . . . . . . . . . . . . . . 16 ;;
106	103, 63, 104, 105	divassd 10355	. . . . . . . . . . . . . . 15 ;; ;;
107	103, 63, 104, 105	div23d 10357	. . . . . . . . . . . . . . 15 ;; ;;
108		1p2e3 10660	. . . . . . . . . . . . . . . . . 18
109	108	oveq1i 6294	. . . . . . . . . . . . . . . . 17 ;; ;;
110		ax-1cn 9550	. . . . . . . . . . . . . . . . . . 19
111	110	a1i 11	. . . . . . . . . . . . . . . . . 18
112	63, 104, 105	divcld 10320	. . . . . . . . . . . . . . . . . 18 ;;
113	111, 35, 112	adddird 9621	. . . . . . . . . . . . . . . . 17 ;; ;; ;;
114	109, 113	syl5eqr 2522	. . . . . . . . . . . . . . . 16 ;; ;; ;;
115	112	mulid2d 9614	. . . . . . . . . . . . . . . . 17 ;; ;;
116	115	oveq1d 6299	. . . . . . . . . . . . . . . 16 ;; ;; ;; ;;
117	114, 116	eqtrd 2508	. . . . . . . . . . . . . . 15 ;; ;; ;;
118	106, 107, 117	3eqtr3d 2516	. . . . . . . . . . . . . 14 ;; ;; ;;
119	43	oveq1i 6294	. . . . . . . . . . . . . . . 16
120	65, 17, 19	divcld 10320	. . . . . . . . . . . . . . . . 17
121	103, 111, 120	adddird 9621	. . . . . . . . . . . . . . . 16
122	119, 121	syl5eq 2520	. . . . . . . . . . . . . . 15
123	65, 17, 19	divcan2d 10322	. . . . . . . . . . . . . . 15
124	120	mulid2d 9614	. . . . . . . . . . . . . . . . 17
125	64, 17, 17, 19, 19	divdiv1d 10351	. . . . . . . . . . . . . . . . . 18
126		4t4e16 11049	. . . . . . . . . . . . . . . . . . 19 ;
127	126	oveq2i 6295	. . . . . . . . . . . . . . . . . 18 ;
128	125, 127	syl6eq 2524	. . . . . . . . . . . . . . . . 17 ;
129	63, 11, 76, 14, 78	divdiv1d 10351	. . . . . . . . . . . . . . . . . 18 ; ;
130	10, 75	mulcli 9601	. . . . . . . . . . . . . . . . . . . . 21 ;
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
132	10, 75, 13, 77	mulne0i 10192	. . . . . . . . . . . . . . . . . . . . 21 ;
133	132	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
134	63, 131, 133	divcld 10320	. . . . . . . . . . . . . . . . . . 19 ;
135	134, 35, 37	divcan2d 10322	. . . . . . . . . . . . . . . . . 18 ; ;
136	63, 131, 35, 133, 37	divdiv1d 10351	. . . . . . . . . . . . . . . . . . . 20 ; ;
137	10, 75, 30	mul32i 9775	. . . . . . . . . . . . . . . . . . . . . 22 ; ;
138		2exp4 14430	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
139		8t2e16 11064	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
140	138, 139	eqtr4i 2499	. . . . . . . . . . . . . . . . . . . . . . 23
141	140, 138	oveq12i 6296	. . . . . . . . . . . . . . . . . . . . . 22 ;
142		4p4e8 10672	. . . . . . . . . . . . . . . . . . . . . . . 24
143	142	oveq2i 6295	. . . . . . . . . . . . . . . . . . . . . . 23
144		expadd 12176	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
145	30, 61, 61, 144	mp3an 1324	. . . . . . . . . . . . . . . . . . . . . . 23
146		2exp8 14432	. . . . . . . . . . . . . . . . . . . . . . 23 ;;
147	143, 145, 146	3eqtr3i 2504	. . . . . . . . . . . . . . . . . . . . . 22 ;;
148	137, 141, 147	3eqtr2i 2502	. . . . . . . . . . . . . . . . . . . . 21 ; ;;
149	148	oveq2i 6295	. . . . . . . . . . . . . . . . . . . 20 ; ;;
150	136, 149	syl6eq 2524	. . . . . . . . . . . . . . . . . . 19 ; ;;
151	150	oveq2d 6300	. . . . . . . . . . . . . . . . . 18 ; ;;
152	129, 135, 151	3eqtr2d 2514	. . . . . . . . . . . . . . . . 17 ; ;;
153	124, 128, 152	3eqtrd 2512	. . . . . . . . . . . . . . . 16 ;;
154	153	oveq2d 6300	. . . . . . . . . . . . . . 15 ;;
155	122, 123, 154	3eqtr3d 2516	. . . . . . . . . . . . . 14 ;;
156	118, 155	oveq12d 6302	. . . . . . . . . . . . 13 ;; ;; ;; ;;
157		mulcl 9576	. . . . . . . . . . . . . . 15 $/\$
158	80, 120, 157	sylancr 663	. . . . . . . . . . . . . 14
159		mulcl 9576	. . . . . . . . . . . . . . 15 $/\$ ;; ;;
160	30, 112, 159	sylancr 663	. . . . . . . . . . . . . 14 ;;
161	112, 158, 160	pnpcan2d 9968	. . . . . . . . . . . . 13 ;; ;; ;; ;;
162	156, 161	eqtrd 2508	. . . . . . . . . . . 12 ;; ;;
163	162	oveq2d 6300	. . . . . . . . . . 11 ; ;; ; ;;
164	79, 112, 158	addsub12d 9953	. . . . . . . . . . 11 ; ;; ;; ;
165	163, 164	eqtrd 2508	. . . . . . . . . 10 ; ;; ;; ;
166	59, 11, 35, 14, 37	divdiv1d 10351	. . . . . . . . . . . . . . . 16
167	139	oveq2i 6295	. . . . . . . . . . . . . . . 16 ;
168	166, 167	syl6eq 2524	. . . . . . . . . . . . . . 15 ;
169	168	oveq2d 6300	. . . . . . . . . . . . . 14 ;
170	60, 35, 37	divcan2d 10322	. . . . . . . . . . . . . 14
171	79	2timesd 10781	. . . . . . . . . . . . . 14 ; ; ;
172	169, 170, 171	3eqtr3d 2516	. . . . . . . . . . . . 13 ; ;
173	172	oveq1d 6299	. . . . . . . . . . . 12 ; ; ; ;
174	79, 79	pncand 9931	. . . . . . . . . . . 12 ; ; ; ;
175	173, 174	eqtrd 2508	. . . . . . . . . . 11 ; ;
176	175	oveq1d 6299	. . . . . . . . . 10 ; ;; ; ;;
177		quart1.p	. . . . . . . . . . . . 13
178	177	oveq1d 6299	. . . . . . . . . . . 12
179	80, 10, 13	divcli 10286	. . . . . . . . . . . . . 14
180		mulcl 9576	. . . . . . . . . . . . . 14 $/\$
181	179, 58, 180	sylancr 663	. . . . . . . . . . . . 13
182	20	sqcld 12276	. . . . . . . . . . . . 13
183	3, 181, 182	subdird 10013	. . . . . . . . . . . 12
184	2, 17, 19	sqdivd 12291	. . . . . . . . . . . . . . . 16
185	16	sqvali 12215	. . . . . . . . . . . . . . . . . 18
186	185, 126	eqtri 2496	. . . . . . . . . . . . . . . . 17 ;
187	186	oveq2i 6295	. . . . . . . . . . . . . . . 16 ;
188	184, 187	syl6eq 2524	. . . . . . . . . . . . . . 15 ;
189	188	oveq2d 6300	. . . . . . . . . . . . . 14 ;
190	3, 58, 76, 78	divassd 10355	. . . . . . . . . . . . . 14 ; ;
191	3, 58	mulcomd 9617	. . . . . . . . . . . . . . 15
192	191	oveq1d 6299	. . . . . . . . . . . . . 14 ; ;
193	189, 190, 192	3eqtr2d 2514	. . . . . . . . . . . . 13 ;
194	179	a1i 11	. . . . . . . . . . . . . . . . . 18
195	194, 58, 58	mulassd 9619	. . . . . . . . . . . . . . . . 17
196	103, 63, 11, 14	div23d 10357	. . . . . . . . . . . . . . . . . 18
197		2p2e4 10653	. . . . . . . . . . . . . . . . . . . . 21
198	197	oveq2i 6295	. . . . . . . . . . . . . . . . . . . 20
199	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
200	2, 199, 199	expaddd 12280	. . . . . . . . . . . . . . . . . . . 20
201	198, 200	syl5eqr 2522	. . . . . . . . . . . . . . . . . . 19
202	201	oveq2d 6300	. . . . . . . . . . . . . . . . . 18
203	196, 202	eqtrd 2508	. . . . . . . . . . . . . . . . 17
204	103, 63, 11, 14	divassd 10355	. . . . . . . . . . . . . . . . 17
205	195, 203, 204	3eqtr2d 2514	. . . . . . . . . . . . . . . 16
206	205	oveq1d 6299	. . . . . . . . . . . . . . 15
207	186, 76	syl5eqel 2559	. . . . . . . . . . . . . . . 16
208	186, 77	eqnetri 2763	. . . . . . . . . . . . . . . . 17
209	208	a1i 11	. . . . . . . . . . . . . . . 16
210	181, 58, 207, 209	divassd 10355	. . . . . . . . . . . . . . 15
211	103, 64, 207, 209	divassd 10355	. . . . . . . . . . . . . . 15
212	206, 210, 211	3eqtr3d 2516	. . . . . . . . . . . . . 14
213	184	oveq2d 6300	. . . . . . . . . . . . . 14
214	186	oveq2i 6295	. . . . . . . . . . . . . . . 16 ;
215	128, 214	syl6eqr 2526	. . . . . . . . . . . . . . 15
216	215	oveq2d 6300	. . . . . . . . . . . . . 14
217	212, 213, 216	3eqtr4d 2518	. . . . . . . . . . . . 13
218	193, 217	oveq12d 6302	. . . . . . . . . . . 12 ;
219	178, 183, 218	3eqtrd 2512	. . . . . . . . . . 11 ;
220	219	oveq2d 6300	. . . . . . . . . 10 ;; ;; ;
221	165, 176, 220	3eqtr4d 2518	. . . . . . . . 9 ; ;; ;;
222	101, 102, 221	3eqtrd 2512	. . . . . . . 8 ;; ; ;;
223	222	negeqd 9814	. . . . . . 7 ;; ; ;;
224	65, 79, 60, 89	addsub4d 9977	. . . . . . 7 ; ;; ; ;;
225	99, 223, 224	3eqtr3rd 2517	. . . . . 6 ; ;; ;;
226	225	oveq2d 6300	. . . . 5 ; ;; ;;
227	3, 181	subcld 9930	. . . . . . . . 9
228	177, 227	eqeltrd 2555	. . . . . . . 8
229	228, 182	mulcld 9616	. . . . . . 7
230	112, 229	addcld 9615	. . . . . 6 ;;
231	71, 230	negsubd 9936	. . . . 5 ;; ;;
232	96, 226, 231	3eqtrd 2512	. . . 4 ; ;; ;;
233	93, 95, 232	3eqtrd 2512	. . 3 ;;
234	233	oveq2d 6300	. 2 ;; ;; ;;
235	230, 71	pncan3d 9933	. 2 ;; ;;
236	234, 235	eqtr2d 2509	1 ;;

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1379

wcel 1767

wne 2662 (class class class)co 6284

cc 9490

cc0 9492

c1 9493

caddc 9495

cmul 9497

cmin 9805

cneg 9806

cdiv 10206

c2 10585

c3 10586

c4 10587

c5 10588

c6 10589

c8 10591

cn0 10795 ;cdc 10976

cexp 12134

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-2nd 6785 df-recs 7042 df-rdg 7076 df-er 7311 df-en 7517 df-dom 7518 df-sdom 7519 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-4 10596 df-5 10597 df-6 10598 df-7 10599 df-8 10600 df-9 10601 df-10 10602 df-n0 10796 df-z 10865 df-dec 10977 df-uz 11083 df-seq 12076 df-exp 12135

This theorem is referenced by: quart1 22943

W3C validator