quart1lem - Metamath Proof Explorer

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

Theorem quart1lem 23386

Description: Lemma for quart1 23387. (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 9605	. . . . . . . . . 10
5	4	halfcld 10779	. . . . . . . . 9
6	1, 5	subcld 9922	. . . . . . . 8
7		3nn0 10809	. . . . . . . . . 10
8		expcl 12169	. . . . . . . . . 10 $/\$
9	2, 7, 8	sylancl 660	. . . . . . . . 9
10		8cn 10617	. . . . . . . . . 10
11	10	a1i 11	. . . . . . . . 9
12		8nn 10695	. . . . . . . . . . 11
13	12	nnne0i 10566	. . . . . . . . . 10
14	13	a1i 11	. . . . . . . . 9
15	9, 11, 14	divcld 10316	. . . . . . . 8
16		4cn 10609	. . . . . . . . . 10
17	16	a1i 11	. . . . . . . . 9
18		4ne0 10628	. . . . . . . . . 10
19	18	a1i 11	. . . . . . . . 9
20	2, 17, 19	divcld 10316	. . . . . . . 8
21	6, 15, 20	adddird 9610	. . . . . . 7
22		quart1.q	. . . . . . . 8
23	22	oveq1d 6285	. . . . . . 7
24	1, 2, 17, 19	divassd 10351	. . . . . . . . . 10
25	2	sqvald 12292	. . . . . . . . . . . . . . 15
26	25	oveq1d 6285	. . . . . . . . . . . . . 14
27	2, 2, 3	mul32d 9779	. . . . . . . . . . . . . 14
28	26, 27	eqtrd 2495	. . . . . . . . . . . . 13
29	28	oveq1d 6285	. . . . . . . . . . . 12
30		2cn 10602	. . . . . . . . . . . . . 14
31		4t2e8 10685	. . . . . . . . . . . . . 14
32	16, 30, 31	mulcomli 9592	. . . . . . . . . . . . 13
33	32	oveq2i 6281	. . . . . . . . . . . 12
34	29, 33	syl6eqr 2513	. . . . . . . . . . 11
35	30	a1i 11	. . . . . . . . . . . 12
36		2ne0 10624	. . . . . . . . . . . . 13
37	36	a1i 11	. . . . . . . . . . . 12
38	4, 35, 2, 17, 37, 19	divmuldivd 10357	. . . . . . . . . . 11
39	34, 38	eqtr4d 2498	. . . . . . . . . 10
40	24, 39	oveq12d 6288	. . . . . . . . 9
41	1, 5, 20	subdird 10009	. . . . . . . . 9
42	40, 41	eqtr4d 2498	. . . . . . . 8
43		df-4 10592	. . . . . . . . . . . . . 14
44	43	oveq2i 6281	. . . . . . . . . . . . 13
45		expp1 12158	. . . . . . . . . . . . . 14 $/\$
46	2, 7, 45	sylancl 660	. . . . . . . . . . . . 13
47	44, 46	syl5eq 2507	. . . . . . . . . . . 12
48	47	oveq1d 6285	. . . . . . . . . . 11
49	9, 2, 11, 14	div23d 10353	. . . . . . . . . . 11
50	48, 49	eqtrd 2495	. . . . . . . . . 10
51	50	oveq1d 6285	. . . . . . . . 9
52	15, 2, 17, 19	divassd 10351	. . . . . . . . 9
53	51, 52	eqtrd 2495	. . . . . . . 8
54	42, 53	oveq12d 6288	. . . . . . 7
55	21, 23, 54	3eqtr4d 2505	. . . . . 6
56	1, 2	mulcld 9605	. . . . . . . 8
57	56, 17, 19	divcld 10316	. . . . . . 7
58	2	sqcld 12293	. . . . . . . . 9
59	58, 3	mulcld 9605	. . . . . . . 8
60	59, 11, 14	divcld 10316	. . . . . . 7
61		4nn0 10810	. . . . . . . . . 10
62		expcl 12169	. . . . . . . . . 10 $/\$
63	2, 61, 62	sylancl 660	. . . . . . . . 9
64	63, 11, 14	divcld 10316	. . . . . . . 8
65	64, 17, 19	divcld 10316	. . . . . . 7
66	57, 60, 65	subadd23d 9944	. . . . . 6
67	65, 60	subcld 9922	. . . . . . 7
68	57, 67	addcomd 9771	. . . . . 6
69	55, 66, 68	3eqtrd 2499	. . . . 5
70		quart1.r	. . . . . 6 ; ;;
71		quart1.d	. . . . . . 7
72		1nn0 10807	. . . . . . . . . . . 12
73		6nn 10693	. . . . . . . . . . . 12
74	72, 73	decnncl 10989	. . . . . . . . . . 11 ;
75	74	nncni 10541	. . . . . . . . . 10 ;
76	75	a1i 11	. . . . . . . . 9 ;
77	74	nnne0i 10566	. . . . . . . . . 10 ;
78	77	a1i 11	. . . . . . . . 9 ;
79	59, 76, 78	divcld 10316	. . . . . . . 8 ;
80		3cn 10606	. . . . . . . . . 10
81		2nn0 10808	. . . . . . . . . . . . 13
82		5nn0 10811	. . . . . . . . . . . . 13
83	81, 82	deccl 10990	. . . . . . . . . . . 12 ;
84	83, 73	decnncl 10989	. . . . . . . . . . 11 ;;
85	84	nncni 10541	. . . . . . . . . 10 ;;
86	84	nnne0i 10566	. . . . . . . . . 10 ;;
87	80, 85, 86	divcli 10282	. . . . . . . . 9 ;;
88		mulcl 9565	. . . . . . . . 9 ;; $/\$ ;;
89	87, 63, 88	sylancr 661	. . . . . . . 8 ;;
90	79, 89	subcld 9922	. . . . . . 7 ; ;;
91	71, 90, 57	addsubd 9943	. . . . . 6 ; ;; ; ;;
92	70, 91	eqtr4d 2498	. . . . 5 ; ;;
93	69, 92	oveq12d 6288	. . . 4 ; ;;
94	71, 90	addcld 9604	. . . . 5 ; ;;
95	67, 57, 94	ppncand 9962	. . . 4 ; ;; ; ;;
96	67, 71, 90	add12d 9792	. . . . 5 ; ;; ; ;;
97	60, 89	addcld 9604	. . . . . . . 8 ;;
98	65, 79	addcld 9604	. . . . . . . 8 ;
99	97, 98	negsubdi2d 9938	. . . . . . 7 ;; ; ; ;;
100	65, 79	addcomd 9771	. . . . . . . . . 10 ; ;
101	100	oveq2d 6286	. . . . . . . . 9 ;; ; ;; ;
102	60, 89, 79, 65	addsub4d 9969	. . . . . . . . 9 ;; ; ; ;;
103	80	a1i 11	. . . . . . . . . . . . . . . 16
104	85	a1i 11	. . . . . . . . . . . . . . . 16 ;;
105	86	a1i 11	. . . . . . . . . . . . . . . 16 ;;
106	103, 63, 104, 105	divassd 10351	. . . . . . . . . . . . . . 15 ;; ;;
107	103, 63, 104, 105	div23d 10353	. . . . . . . . . . . . . . 15 ;; ;;
108		1p2e3 10656	. . . . . . . . . . . . . . . . . 18
109	108	oveq1i 6280	. . . . . . . . . . . . . . . . 17 ;; ;;
110		1cnd 9601	. . . . . . . . . . . . . . . . . 18
111	63, 104, 105	divcld 10316	. . . . . . . . . . . . . . . . . 18 ;;
112	110, 35, 111	adddird 9610	. . . . . . . . . . . . . . . . 17 ;; ;; ;;
113	109, 112	syl5eqr 2509	. . . . . . . . . . . . . . . 16 ;; ;; ;;
114	111	mulid2d 9603	. . . . . . . . . . . . . . . . 17 ;; ;;
115	114	oveq1d 6285	. . . . . . . . . . . . . . . 16 ;; ;; ;; ;;
116	113, 115	eqtrd 2495	. . . . . . . . . . . . . . 15 ;; ;; ;;
117	106, 107, 116	3eqtr3d 2503	. . . . . . . . . . . . . 14 ;; ;; ;;
118	43	oveq1i 6280	. . . . . . . . . . . . . . . 16
119	65, 17, 19	divcld 10316	. . . . . . . . . . . . . . . . 17
120	103, 110, 119	adddird 9610	. . . . . . . . . . . . . . . 16
121	118, 120	syl5eq 2507	. . . . . . . . . . . . . . 15
122	65, 17, 19	divcan2d 10318	. . . . . . . . . . . . . . 15
123	119	mulid2d 9603	. . . . . . . . . . . . . . . . 17
124	64, 17, 17, 19, 19	divdiv1d 10347	. . . . . . . . . . . . . . . . . 18
125		4t4e16 11049	. . . . . . . . . . . . . . . . . . 19 ;
126	125	oveq2i 6281	. . . . . . . . . . . . . . . . . 18 ;
127	124, 126	syl6eq 2511	. . . . . . . . . . . . . . . . 17 ;
128	63, 11, 76, 14, 78	divdiv1d 10347	. . . . . . . . . . . . . . . . . 18 ; ;
129	10, 75	mulcli 9590	. . . . . . . . . . . . . . . . . . . . 21 ;
130	129	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
131	10, 75, 13, 77	mulne0i 10188	. . . . . . . . . . . . . . . . . . . . 21 ;
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
133	63, 130, 132	divcld 10316	. . . . . . . . . . . . . . . . . . 19 ;
134	133, 35, 37	divcan2d 10318	. . . . . . . . . . . . . . . . . 18 ; ;
135	63, 130, 35, 132, 37	divdiv1d 10347	. . . . . . . . . . . . . . . . . . . 20 ; ;
136	10, 75, 30	mul32i 9765	. . . . . . . . . . . . . . . . . . . . . 22 ; ;
137		2exp4 14658	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
138		8t2e16 11064	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
139	137, 138	eqtr4i 2486	. . . . . . . . . . . . . . . . . . . . . . 23
140	139, 137	oveq12i 6282	. . . . . . . . . . . . . . . . . . . . . 22 ;
141		4p4e8 10668	. . . . . . . . . . . . . . . . . . . . . . . 24
142	141	oveq2i 6281	. . . . . . . . . . . . . . . . . . . . . . 23
143		expadd 12193	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
144	30, 61, 61, 143	mp3an 1322	. . . . . . . . . . . . . . . . . . . . . . 23
145		2exp8 14661	. . . . . . . . . . . . . . . . . . . . . . 23 ;;
146	142, 144, 145	3eqtr3i 2491	. . . . . . . . . . . . . . . . . . . . . 22 ;;
147	136, 140, 146	3eqtr2i 2489	. . . . . . . . . . . . . . . . . . . . 21 ; ;;
148	147	oveq2i 6281	. . . . . . . . . . . . . . . . . . . 20 ; ;;
149	135, 148	syl6eq 2511	. . . . . . . . . . . . . . . . . . 19 ; ;;
150	149	oveq2d 6286	. . . . . . . . . . . . . . . . . 18 ; ;;
151	128, 134, 150	3eqtr2d 2501	. . . . . . . . . . . . . . . . 17 ; ;;
152	123, 127, 151	3eqtrd 2499	. . . . . . . . . . . . . . . 16 ;;
153	152	oveq2d 6286	. . . . . . . . . . . . . . 15 ;;
154	121, 122, 153	3eqtr3d 2503	. . . . . . . . . . . . . 14 ;;
155	117, 154	oveq12d 6288	. . . . . . . . . . . . 13 ;; ;; ;; ;;
156		mulcl 9565	. . . . . . . . . . . . . . 15 $/\$
157	80, 119, 156	sylancr 661	. . . . . . . . . . . . . 14
158		mulcl 9565	. . . . . . . . . . . . . . 15 $/\$ ;; ;;
159	30, 111, 158	sylancr 661	. . . . . . . . . . . . . 14 ;;
160	111, 157, 159	pnpcan2d 9960	. . . . . . . . . . . . 13 ;; ;; ;; ;;
161	155, 160	eqtrd 2495	. . . . . . . . . . . 12 ;; ;;
162	161	oveq2d 6286	. . . . . . . . . . 11 ; ;; ; ;;
163	79, 111, 157	addsub12d 9945	. . . . . . . . . . 11 ; ;; ;; ;
164	162, 163	eqtrd 2495	. . . . . . . . . 10 ; ;; ;; ;
165	59, 11, 35, 14, 37	divdiv1d 10347	. . . . . . . . . . . . . . . 16
166	138	oveq2i 6281	. . . . . . . . . . . . . . . 16 ;
167	165, 166	syl6eq 2511	. . . . . . . . . . . . . . 15 ;
168	167	oveq2d 6286	. . . . . . . . . . . . . 14 ;
169	60, 35, 37	divcan2d 10318	. . . . . . . . . . . . . 14
170	79	2timesd 10777	. . . . . . . . . . . . . 14 ; ; ;
171	168, 169, 170	3eqtr3d 2503	. . . . . . . . . . . . 13 ; ;
172	171	oveq1d 6285	. . . . . . . . . . . 12 ; ; ; ;
173	79, 79	pncand 9923	. . . . . . . . . . . 12 ; ; ; ;
174	172, 173	eqtrd 2495	. . . . . . . . . . 11 ; ;
175	174	oveq1d 6285	. . . . . . . . . 10 ; ;; ; ;;
176		quart1.p	. . . . . . . . . . . . 13
177	176	oveq1d 6285	. . . . . . . . . . . 12
178	80, 10, 13	divcli 10282	. . . . . . . . . . . . . 14
179		mulcl 9565	. . . . . . . . . . . . . 14 $/\$
180	178, 58, 179	sylancr 661	. . . . . . . . . . . . 13
181	20	sqcld 12293	. . . . . . . . . . . . 13
182	3, 180, 181	subdird 10009	. . . . . . . . . . . 12
183	2, 17, 19	sqdivd 12308	. . . . . . . . . . . . . . . 16
184	16	sqvali 12232	. . . . . . . . . . . . . . . . . 18
185	184, 125	eqtri 2483	. . . . . . . . . . . . . . . . 17 ;
186	185	oveq2i 6281	. . . . . . . . . . . . . . . 16 ;
187	183, 186	syl6eq 2511	. . . . . . . . . . . . . . 15 ;
188	187	oveq2d 6286	. . . . . . . . . . . . . 14 ;
189	3, 58, 76, 78	divassd 10351	. . . . . . . . . . . . . 14 ; ;
190	3, 58	mulcomd 9606	. . . . . . . . . . . . . . 15
191	190	oveq1d 6285	. . . . . . . . . . . . . 14 ; ;
192	188, 189, 191	3eqtr2d 2501	. . . . . . . . . . . . 13 ;
193	178	a1i 11	. . . . . . . . . . . . . . . . . 18
194	193, 58, 58	mulassd 9608	. . . . . . . . . . . . . . . . 17
195	103, 63, 11, 14	div23d 10353	. . . . . . . . . . . . . . . . . 18
196		2p2e4 10649	. . . . . . . . . . . . . . . . . . . . 21
197	196	oveq2i 6281	. . . . . . . . . . . . . . . . . . . 20
198	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
199	2, 198, 198	expaddd 12297	. . . . . . . . . . . . . . . . . . . 20
200	197, 199	syl5eqr 2509	. . . . . . . . . . . . . . . . . . 19
201	200	oveq2d 6286	. . . . . . . . . . . . . . . . . 18
202	195, 201	eqtrd 2495	. . . . . . . . . . . . . . . . 17
203	103, 63, 11, 14	divassd 10351	. . . . . . . . . . . . . . . . 17
204	194, 202, 203	3eqtr2d 2501	. . . . . . . . . . . . . . . 16
205	204	oveq1d 6285	. . . . . . . . . . . . . . 15
206	185, 76	syl5eqel 2546	. . . . . . . . . . . . . . . 16
207	185, 77	eqnetri 2750	. . . . . . . . . . . . . . . . 17
208	207	a1i 11	. . . . . . . . . . . . . . . 16
209	180, 58, 206, 208	divassd 10351	. . . . . . . . . . . . . . 15
210	103, 64, 206, 208	divassd 10351	. . . . . . . . . . . . . . 15
211	205, 209, 210	3eqtr3d 2503	. . . . . . . . . . . . . 14
212	183	oveq2d 6286	. . . . . . . . . . . . . 14
213	185	oveq2i 6281	. . . . . . . . . . . . . . . 16 ;
214	127, 213	syl6eqr 2513	. . . . . . . . . . . . . . 15
215	214	oveq2d 6286	. . . . . . . . . . . . . 14
216	211, 212, 215	3eqtr4d 2505	. . . . . . . . . . . . 13
217	192, 216	oveq12d 6288	. . . . . . . . . . . 12 ;
218	177, 182, 217	3eqtrd 2499	. . . . . . . . . . 11 ;
219	218	oveq2d 6286	. . . . . . . . . 10 ;; ;; ;
220	164, 175, 219	3eqtr4d 2505	. . . . . . . . 9 ; ;; ;;
221	101, 102, 220	3eqtrd 2499	. . . . . . . 8 ;; ; ;;
222	221	negeqd 9805	. . . . . . 7 ;; ; ;;
223	65, 79, 60, 89	addsub4d 9969	. . . . . . 7 ; ;; ; ;;
224	99, 222, 223	3eqtr3rd 2504	. . . . . 6 ; ;; ;;
225	224	oveq2d 6286	. . . . 5 ; ;; ;;
226	3, 180	subcld 9922	. . . . . . . . 9
227	176, 226	eqeltrd 2542	. . . . . . . 8
228	227, 181	mulcld 9605	. . . . . . 7
229	111, 228	addcld 9604	. . . . . 6 ;;
230	71, 229	negsubd 9928	. . . . 5 ;; ;;
231	96, 225, 230	3eqtrd 2499	. . . 4 ; ;; ;;
232	93, 95, 231	3eqtrd 2499	. . 3 ;;
233	232	oveq2d 6286	. 2 ;; ;; ;;
234	229, 71	pncan3d 9925	. 2 ;; ;;
235	233, 234	eqtr2d 2496	1 ;;

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1398

wcel 1823

wne 2649 (class class class)co 6270

cc 9479

cc0 9481

c1 9482

caddc 9484

cmul 9486

cmin 9796

cneg 9797

cdiv 10202

c2 10581

c3 10582

c4 10583

c5 10584

c6 10585

c8 10587

cn0 10791 ;cdc 10976

cexp 12151

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-2nd 6774 df-recs 7034 df-rdg 7068 df-er 7303 df-en 7510 df-dom 7511 df-sdom 7512 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-div 10203 df-nn 10532 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10977 df-uz 11083 df-seq 12093 df-exp 12152

This theorem is referenced by: quart1 23387

W3C validator