quart1lem - Metamath Proof Explorer

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

Theorem quart1lem 22137

Description: Lemma for quart1 22138. (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 9396	. . . . . . . . . 10
5	4	halfcld 10559	. . . . . . . . 9
6	1, 5	subcld 9709	. . . . . . . 8
7		3nn0 10587	. . . . . . . . . 10
8		expcl 11869	. . . . . . . . . 10 $/\$
9	2, 7, 8	sylancl 657	. . . . . . . . 9
10		8cn 10397	. . . . . . . . . 10
11	10	a1i 11	. . . . . . . . 9
12		8nn 10475	. . . . . . . . . . 11
13	12	nnne0i 10346	. . . . . . . . . 10
14	13	a1i 11	. . . . . . . . 9
15	9, 11, 14	divcld 10097	. . . . . . . 8
16		4cn 10389	. . . . . . . . . 10
17	16	a1i 11	. . . . . . . . 9
18		4ne0 10408	. . . . . . . . . 10
19	18	a1i 11	. . . . . . . . 9
20	2, 17, 19	divcld 10097	. . . . . . . 8
21	6, 15, 20	adddird 9401	. . . . . . 7
22		quart1.q	. . . . . . . 8
23	22	oveq1d 6097	. . . . . . 7
24	1, 2, 17, 19	divassd 10132	. . . . . . . . . 10
25	2	sqvald 11991	. . . . . . . . . . . . . . 15
26	25	oveq1d 6097	. . . . . . . . . . . . . 14
27	2, 2, 3	mul32d 9569	. . . . . . . . . . . . . 14
28	26, 27	eqtrd 2467	. . . . . . . . . . . . 13
29	28	oveq1d 6097	. . . . . . . . . . . 12
30		2cn 10382	. . . . . . . . . . . . . 14
31		4t2e8 10465	. . . . . . . . . . . . . 14
32	16, 30, 31	mulcomli 9383	. . . . . . . . . . . . 13
33	32	oveq2i 6093	. . . . . . . . . . . 12
34	29, 33	syl6eqr 2485	. . . . . . . . . . 11
35	30	a1i 11	. . . . . . . . . . . 12
36		2ne0 10404	. . . . . . . . . . . . 13
37	36	a1i 11	. . . . . . . . . . . 12
38	4, 35, 2, 17, 37, 19	divmuldivd 10138	. . . . . . . . . . 11
39	34, 38	eqtr4d 2470	. . . . . . . . . 10
40	24, 39	oveq12d 6100	. . . . . . . . 9
41	1, 5, 20	subdird 9791	. . . . . . . . 9
42	40, 41	eqtr4d 2470	. . . . . . . 8
43		df-4 10372	. . . . . . . . . . . . . 14
44	43	oveq2i 6093	. . . . . . . . . . . . 13
45		expp1 11858	. . . . . . . . . . . . . 14 $/\$
46	2, 7, 45	sylancl 657	. . . . . . . . . . . . 13
47	44, 46	syl5eq 2479	. . . . . . . . . . . 12
48	47	oveq1d 6097	. . . . . . . . . . 11
49	9, 2, 11, 14	div23d 10134	. . . . . . . . . . 11
50	48, 49	eqtrd 2467	. . . . . . . . . 10
51	50	oveq1d 6097	. . . . . . . . 9
52	15, 2, 17, 19	divassd 10132	. . . . . . . . 9
53	51, 52	eqtrd 2467	. . . . . . . 8
54	42, 53	oveq12d 6100	. . . . . . 7
55	21, 23, 54	3eqtr4d 2477	. . . . . 6
56	1, 2	mulcld 9396	. . . . . . . 8
57	56, 17, 19	divcld 10097	. . . . . . 7
58	2	sqcld 11992	. . . . . . . . 9
59	58, 3	mulcld 9396	. . . . . . . 8
60	59, 11, 14	divcld 10097	. . . . . . 7
61		4nn0 10588	. . . . . . . . . 10
62		expcl 11869	. . . . . . . . . 10 $/\$
63	2, 61, 62	sylancl 657	. . . . . . . . 9
64	63, 11, 14	divcld 10097	. . . . . . . 8
65	64, 17, 19	divcld 10097	. . . . . . 7
66	57, 60, 65	subadd23d 9731	. . . . . 6
67	65, 60	subcld 9709	. . . . . . 7
68	57, 67	addcomd 9561	. . . . . 6
69	55, 66, 68	3eqtrd 2471	. . . . 5
70		quart1.r	. . . . . 6 ; ;;
71		quart1.d	. . . . . . 7
72		1nn0 10585	. . . . . . . . . . . 12
73		6nn 10473	. . . . . . . . . . . 12
74	72, 73	decnncl 10758	. . . . . . . . . . 11 ;
75	74	nncni 10322	. . . . . . . . . 10 ;
76	75	a1i 11	. . . . . . . . 9 ;
77	74	nnne0i 10346	. . . . . . . . . 10 ;
78	77	a1i 11	. . . . . . . . 9 ;
79	59, 76, 78	divcld 10097	. . . . . . . 8 ;
80		3cn 10386	. . . . . . . . . 10
81		2nn0 10586	. . . . . . . . . . . . 13
82		5nn0 10589	. . . . . . . . . . . . 13
83	81, 82	deccl 10759	. . . . . . . . . . . 12 ;
84	83, 73	decnncl 10758	. . . . . . . . . . 11 ;;
85	84	nncni 10322	. . . . . . . . . 10 ;;
86	84	nnne0i 10346	. . . . . . . . . 10 ;;
87	80, 85, 86	divcli 10063	. . . . . . . . 9 ;;
88		mulcl 9356	. . . . . . . . 9 ;; $/\$ ;;
89	87, 63, 88	sylancr 658	. . . . . . . 8 ;;
90	79, 89	subcld 9709	. . . . . . 7 ; ;;
91	71, 90, 57	addsubd 9730	. . . . . 6 ; ;; ; ;;
92	70, 91	eqtr4d 2470	. . . . 5 ; ;;
93	69, 92	oveq12d 6100	. . . 4 ; ;;
94	71, 90	addcld 9395	. . . . 5 ; ;;
95	67, 57, 94	ppncand 9749	. . . 4 ; ;; ; ;;
96	67, 71, 90	add12d 9581	. . . . 5 ; ;; ; ;;
97	60, 89	addcld 9395	. . . . . . . 8 ;;
98	65, 79	addcld 9395	. . . . . . . 8 ;
99	97, 98	negsubdi2d 9725	. . . . . . 7 ;; ; ; ;;
100	65, 79	addcomd 9561	. . . . . . . . . 10 ; ;
101	100	oveq2d 6098	. . . . . . . . 9 ;; ; ;; ;
102	60, 89, 79, 65	addsub4d 9756	. . . . . . . . 9 ;; ; ; ;;
103	80	a1i 11	. . . . . . . . . . . . . . . 16
104	85	a1i 11	. . . . . . . . . . . . . . . 16 ;;
105	86	a1i 11	. . . . . . . . . . . . . . . 16 ;;
106	103, 63, 104, 105	divassd 10132	. . . . . . . . . . . . . . 15 ;; ;;
107	103, 63, 104, 105	div23d 10134	. . . . . . . . . . . . . . 15 ;; ;;
108		1p2e3 10436	. . . . . . . . . . . . . . . . . 18
109	108	oveq1i 6092	. . . . . . . . . . . . . . . . 17 ;; ;;
110		ax-1cn 9330	. . . . . . . . . . . . . . . . . . 19
111	110	a1i 11	. . . . . . . . . . . . . . . . . 18
112	63, 104, 105	divcld 10097	. . . . . . . . . . . . . . . . . 18 ;;
113	111, 35, 112	adddird 9401	. . . . . . . . . . . . . . . . 17 ;; ;; ;;
114	109, 113	syl5eqr 2481	. . . . . . . . . . . . . . . 16 ;; ;; ;;
115	112	mulid2d 9394	. . . . . . . . . . . . . . . . 17 ;; ;;
116	115	oveq1d 6097	. . . . . . . . . . . . . . . 16 ;; ;; ;; ;;
117	114, 116	eqtrd 2467	. . . . . . . . . . . . . . 15 ;; ;; ;;
118	106, 107, 117	3eqtr3d 2475	. . . . . . . . . . . . . 14 ;; ;; ;;
119	43	oveq1i 6092	. . . . . . . . . . . . . . . 16
120	65, 17, 19	divcld 10097	. . . . . . . . . . . . . . . . 17
121	103, 111, 120	adddird 9401	. . . . . . . . . . . . . . . 16
122	119, 121	syl5eq 2479	. . . . . . . . . . . . . . 15
123	65, 17, 19	divcan2d 10099	. . . . . . . . . . . . . . 15
124	120	mulid2d 9394	. . . . . . . . . . . . . . . . 17
125	64, 17, 17, 19, 19	divdiv1d 10128	. . . . . . . . . . . . . . . . . 18
126		4t4e16 10818	. . . . . . . . . . . . . . . . . . 19 ;
127	126	oveq2i 6093	. . . . . . . . . . . . . . . . . 18 ;
128	125, 127	syl6eq 2483	. . . . . . . . . . . . . . . . 17 ;
129	63, 11, 76, 14, 78	divdiv1d 10128	. . . . . . . . . . . . . . . . . 18 ; ;
130	10, 75	mulcli 9381	. . . . . . . . . . . . . . . . . . . . 21 ;
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
132	10, 75, 13, 77	mulne0i 9969	. . . . . . . . . . . . . . . . . . . . 21 ;
133	132	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
134	63, 131, 133	divcld 10097	. . . . . . . . . . . . . . . . . . 19 ;
135	134, 35, 37	divcan2d 10099	. . . . . . . . . . . . . . . . . 18 ; ;
136	63, 131, 35, 133, 37	divdiv1d 10128	. . . . . . . . . . . . . . . . . . . 20 ; ;
137	10, 75, 30	mul32i 9555	. . . . . . . . . . . . . . . . . . . . . 22 ; ;
138		2exp4 14099	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
139		8t2e16 10833	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
140	138, 139	eqtr4i 2458	. . . . . . . . . . . . . . . . . . . . . . 23
141	140, 138	oveq12i 6094	. . . . . . . . . . . . . . . . . . . . . 22 ;
142		4p4e8 10448	. . . . . . . . . . . . . . . . . . . . . . . 24
143	142	oveq2i 6093	. . . . . . . . . . . . . . . . . . . . . . 23
144		expadd 11892	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
145	30, 61, 61, 144	mp3an 1309	. . . . . . . . . . . . . . . . . . . . . . 23
146		2exp8 14101	. . . . . . . . . . . . . . . . . . . . . . 23 ;;
147	143, 145, 146	3eqtr3i 2463	. . . . . . . . . . . . . . . . . . . . . 22 ;;
148	137, 141, 147	3eqtr2i 2461	. . . . . . . . . . . . . . . . . . . . 21 ; ;;
149	148	oveq2i 6093	. . . . . . . . . . . . . . . . . . . 20 ; ;;
150	136, 149	syl6eq 2483	. . . . . . . . . . . . . . . . . . 19 ; ;;
151	150	oveq2d 6098	. . . . . . . . . . . . . . . . . 18 ; ;;
152	129, 135, 151	3eqtr2d 2473	. . . . . . . . . . . . . . . . 17 ; ;;
153	124, 128, 152	3eqtrd 2471	. . . . . . . . . . . . . . . 16 ;;
154	153	oveq2d 6098	. . . . . . . . . . . . . . 15 ;;
155	122, 123, 154	3eqtr3d 2475	. . . . . . . . . . . . . 14 ;;
156	118, 155	oveq12d 6100	. . . . . . . . . . . . 13 ;; ;; ;; ;;
157		mulcl 9356	. . . . . . . . . . . . . . 15 $/\$
158	80, 120, 157	sylancr 658	. . . . . . . . . . . . . 14
159		mulcl 9356	. . . . . . . . . . . . . . 15 $/\$ ;; ;;
160	30, 112, 159	sylancr 658	. . . . . . . . . . . . . 14 ;;
161	112, 158, 160	pnpcan2d 9747	. . . . . . . . . . . . 13 ;; ;; ;; ;;
162	156, 161	eqtrd 2467	. . . . . . . . . . . 12 ;; ;;
163	162	oveq2d 6098	. . . . . . . . . . 11 ; ;; ; ;;
164	79, 112, 158	addsub12d 9732	. . . . . . . . . . 11 ; ;; ;; ;
165	163, 164	eqtrd 2467	. . . . . . . . . 10 ; ;; ;; ;
166	59, 11, 35, 14, 37	divdiv1d 10128	. . . . . . . . . . . . . . . 16
167	139	oveq2i 6093	. . . . . . . . . . . . . . . 16 ;
168	166, 167	syl6eq 2483	. . . . . . . . . . . . . . 15 ;
169	168	oveq2d 6098	. . . . . . . . . . . . . 14 ;
170	60, 35, 37	divcan2d 10099	. . . . . . . . . . . . . 14
171	79	2timesd 10557	. . . . . . . . . . . . . 14 ; ; ;
172	169, 170, 171	3eqtr3d 2475	. . . . . . . . . . . . 13 ; ;
173	172	oveq1d 6097	. . . . . . . . . . . 12 ; ; ; ;
174	79, 79	pncand 9710	. . . . . . . . . . . 12 ; ; ; ;
175	173, 174	eqtrd 2467	. . . . . . . . . . 11 ; ;
176	175	oveq1d 6097	. . . . . . . . . 10 ; ;; ; ;;
177		quart1.p	. . . . . . . . . . . . 13
178	177	oveq1d 6097	. . . . . . . . . . . 12
179	80, 10, 13	divcli 10063	. . . . . . . . . . . . . 14
180		mulcl 9356	. . . . . . . . . . . . . 14 $/\$
181	179, 58, 180	sylancr 658	. . . . . . . . . . . . 13
182	20	sqcld 11992	. . . . . . . . . . . . 13
183	3, 181, 182	subdird 9791	. . . . . . . . . . . 12
184	2, 17, 19	sqdivd 12007	. . . . . . . . . . . . . . . 16
185	16	sqvali 11931	. . . . . . . . . . . . . . . . . 18
186	185, 126	eqtri 2455	. . . . . . . . . . . . . . . . 17 ;
187	186	oveq2i 6093	. . . . . . . . . . . . . . . 16 ;
188	184, 187	syl6eq 2483	. . . . . . . . . . . . . . 15 ;
189	188	oveq2d 6098	. . . . . . . . . . . . . 14 ;
190	3, 58, 76, 78	divassd 10132	. . . . . . . . . . . . . 14 ; ;
191	3, 58	mulcomd 9397	. . . . . . . . . . . . . . 15
192	191	oveq1d 6097	. . . . . . . . . . . . . 14 ; ;
193	189, 190, 192	3eqtr2d 2473	. . . . . . . . . . . . 13 ;
194	179	a1i 11	. . . . . . . . . . . . . . . . . 18
195	194, 58, 58	mulassd 9399	. . . . . . . . . . . . . . . . 17
196	103, 63, 11, 14	div23d 10134	. . . . . . . . . . . . . . . . . 18
197		2p2e4 10429	. . . . . . . . . . . . . . . . . . . . 21
198	197	oveq2i 6093	. . . . . . . . . . . . . . . . . . . 20
199	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
200	2, 199, 199	expaddd 11996	. . . . . . . . . . . . . . . . . . . 20
201	198, 200	syl5eqr 2481	. . . . . . . . . . . . . . . . . . 19
202	201	oveq2d 6098	. . . . . . . . . . . . . . . . . 18
203	196, 202	eqtrd 2467	. . . . . . . . . . . . . . . . 17
204	103, 63, 11, 14	divassd 10132	. . . . . . . . . . . . . . . . 17
205	195, 203, 204	3eqtr2d 2473	. . . . . . . . . . . . . . . 16
206	205	oveq1d 6097	. . . . . . . . . . . . . . 15
207	186, 76	syl5eqel 2519	. . . . . . . . . . . . . . . 16
208	186, 77	eqnetri 2617	. . . . . . . . . . . . . . . . 17
209	208	a1i 11	. . . . . . . . . . . . . . . 16
210	181, 58, 207, 209	divassd 10132	. . . . . . . . . . . . . . 15
211	103, 64, 207, 209	divassd 10132	. . . . . . . . . . . . . . 15
212	206, 210, 211	3eqtr3d 2475	. . . . . . . . . . . . . 14
213	184	oveq2d 6098	. . . . . . . . . . . . . 14
214	186	oveq2i 6093	. . . . . . . . . . . . . . . 16 ;
215	128, 214	syl6eqr 2485	. . . . . . . . . . . . . . 15
216	215	oveq2d 6098	. . . . . . . . . . . . . 14
217	212, 213, 216	3eqtr4d 2477	. . . . . . . . . . . . 13
218	193, 217	oveq12d 6100	. . . . . . . . . . . 12 ;
219	178, 183, 218	3eqtrd 2471	. . . . . . . . . . 11 ;
220	219	oveq2d 6098	. . . . . . . . . 10 ;; ;; ;
221	165, 176, 220	3eqtr4d 2477	. . . . . . . . 9 ; ;; ;;
222	101, 102, 221	3eqtrd 2471	. . . . . . . 8 ;; ; ;;
223	222	negeqd 9594	. . . . . . 7 ;; ; ;;
224	65, 79, 60, 89	addsub4d 9756	. . . . . . 7 ; ;; ; ;;
225	99, 223, 224	3eqtr3rd 2476	. . . . . 6 ; ;; ;;
226	225	oveq2d 6098	. . . . 5 ; ;; ;;
227	3, 181	subcld 9709	. . . . . . . . 9
228	177, 227	eqeltrd 2509	. . . . . . . 8
229	228, 182	mulcld 9396	. . . . . . 7
230	112, 229	addcld 9395	. . . . . 6 ;;
231	71, 230	negsubd 9715	. . . . 5 ;; ;;
232	96, 226, 231	3eqtrd 2471	. . . 4 ; ;; ;;
233	93, 95, 232	3eqtrd 2471	. . 3 ;;
234	233	oveq2d 6098	. 2 ;; ;; ;;
235	230, 71	pncan3d 9712	. 2 ;; ;;
236	234, 235	eqtr2d 2468	1 ;;

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1364

wcel 1757

wne 2598 (class class class)co 6082

cc 9270

cc0 9272

c1 9273

caddc 9275

cmul 9277

cmin 9585

cneg 9586

cdiv 9983

c2 10361

c3 10362

c4 10363

c5 10364

c6 10365

c8 10367

cn0 10569 ;cdc 10745

cexp 11851

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1671 ax-6 1709 ax-7 1729 ax-8 1759 ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2416 ax-sep 4403 ax-nul 4411 ax-pow 4460 ax-pr 4521 ax-un 6363 ax-cnex 9328 ax-resscn 9329 ax-1cn 9330 ax-icn 9331 ax-addcl 9332 ax-addrcl 9333 ax-mulcl 9334 ax-mulrcl 9335 ax-mulcom 9336 ax-addass 9337 ax-mulass 9338 ax-distr 9339 ax-i2m1 9340 ax-1ne0 9341 ax-1rid 9342 ax-rnegex 9343 ax-rrecex 9344 ax-cnre 9345 ax-pre-lttri 9346 ax-pre-lttrn 9347 ax-pre-ltadd 9348 ax-pre-mulgt0 9349

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1702 df-eu 2260 df-mo 2261 df-clab 2422 df-cleq 2428 df-clel 2431 df-nfc 2560 df-ne 2600 df-nel 2601 df-ral 2712 df-rex 2713 df-reu 2714 df-rmo 2715 df-rab 2716 df-v 2966 df-sbc 3178 df-csb 3279 df-dif 3321 df-un 3323 df-in 3325 df-ss 3332 df-pss 3334 df-nul 3628 df-if 3782 df-pw 3852 df-sn 3868 df-pr 3870 df-tp 3872 df-op 3874 df-uni 4082 df-iun 4163 df-br 4283 df-opab 4341 df-mpt 4342 df-tr 4376 df-eprel 4621 df-id 4625 df-po 4630 df-so 4631 df-fr 4668 df-we 4670 df-ord 4711 df-on 4712 df-lim 4713 df-suc 4714 df-xp 4835 df-rel 4836 df-cnv 4837 df-co 4838 df-dm 4839 df-rn 4840 df-res 4841 df-ima 4842 df-iota 5371 df-fun 5410 df-fn 5411 df-f 5412 df-f1 5413 df-fo 5414 df-f1o 5415 df-fv 5416 df-riota 6041 df-ov 6085 df-oprab 6086 df-mpt2 6087 df-om 6468 df-2nd 6569 df-recs 6820 df-rdg 6854 df-er 7091 df-en 7301 df-dom 7302 df-sdom 7303 df-pnf 9410 df-mnf 9411 df-xr 9412 df-ltxr 9413 df-le 9414 df-sub 9587 df-neg 9588 df-div 9984 df-nn 10313 df-2 10370 df-3 10371 df-4 10372 df-5 10373 df-6 10374 df-7 10375 df-8 10376 df-9 10377 df-10 10378 df-n0 10570 df-z 10637 df-dec 10746 df-uz 10852 df-seq 11793 df-exp 11852

This theorem is referenced by: quart1 22138

W3C validator