quart1lem - Metamath Proof Explorer

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

Theorem quart1lem 23781

Description: Lemma for quart1 23782. (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 9663	. . . . . . . . . 10
5	4	halfcld 10857	. . . . . . . . 9
6	1, 5	subcld 9986	. . . . . . . 8
7		3nn0 10887	. . . . . . . . . 10
8		expcl 12290	. . . . . . . . . 10 $/\$
9	2, 7, 8	sylancl 668	. . . . . . . . 9
10		8cn 10695	. . . . . . . . . 10
11	10	a1i 11	. . . . . . . . 9
12		8nn 10773	. . . . . . . . . . 11
13	12	nnne0i 10644	. . . . . . . . . 10
14	13	a1i 11	. . . . . . . . 9
15	9, 11, 14	divcld 10383	. . . . . . . 8
16		4cn 10687	. . . . . . . . . 10
17	16	a1i 11	. . . . . . . . 9
18		4ne0 10706	. . . . . . . . . 10
19	18	a1i 11	. . . . . . . . 9
20	2, 17, 19	divcld 10383	. . . . . . . 8
21	6, 15, 20	adddird 9668	. . . . . . 7
22		quart1.q	. . . . . . . 8
23	22	oveq1d 6305	. . . . . . 7
24	1, 2, 17, 19	divassd 10418	. . . . . . . . . 10
25	2	sqvald 12413	. . . . . . . . . . . . . . 15
26	25	oveq1d 6305	. . . . . . . . . . . . . 14
27	2, 2, 3	mul32d 9843	. . . . . . . . . . . . . 14
28	26, 27	eqtrd 2485	. . . . . . . . . . . . 13
29	28	oveq1d 6305	. . . . . . . . . . . 12
30		2cn 10680	. . . . . . . . . . . . . 14
31		4t2e8 10763	. . . . . . . . . . . . . 14
32	16, 30, 31	mulcomli 9650	. . . . . . . . . . . . 13
33	32	oveq2i 6301	. . . . . . . . . . . 12
34	29, 33	syl6eqr 2503	. . . . . . . . . . 11
35	30	a1i 11	. . . . . . . . . . . 12
36		2ne0 10702	. . . . . . . . . . . . 13
37	36	a1i 11	. . . . . . . . . . . 12
38	4, 35, 2, 17, 37, 19	divmuldivd 10424	. . . . . . . . . . 11
39	34, 38	eqtr4d 2488	. . . . . . . . . 10
40	24, 39	oveq12d 6308	. . . . . . . . 9
41	1, 5, 20	subdird 10075	. . . . . . . . 9
42	40, 41	eqtr4d 2488	. . . . . . . 8
43		df-4 10670	. . . . . . . . . . . . . 14
44	43	oveq2i 6301	. . . . . . . . . . . . 13
45		expp1 12279	. . . . . . . . . . . . . 14 $/\$
46	2, 7, 45	sylancl 668	. . . . . . . . . . . . 13
47	44, 46	syl5eq 2497	. . . . . . . . . . . 12
48	47	oveq1d 6305	. . . . . . . . . . 11
49	9, 2, 11, 14	div23d 10420	. . . . . . . . . . 11
50	48, 49	eqtrd 2485	. . . . . . . . . 10
51	50	oveq1d 6305	. . . . . . . . 9
52	15, 2, 17, 19	divassd 10418	. . . . . . . . 9
53	51, 52	eqtrd 2485	. . . . . . . 8
54	42, 53	oveq12d 6308	. . . . . . 7
55	21, 23, 54	3eqtr4d 2495	. . . . . 6
56	1, 2	mulcld 9663	. . . . . . . 8
57	56, 17, 19	divcld 10383	. . . . . . 7
58	2	sqcld 12414	. . . . . . . . 9
59	58, 3	mulcld 9663	. . . . . . . 8
60	59, 11, 14	divcld 10383	. . . . . . 7
61		4nn0 10888	. . . . . . . . . 10
62		expcl 12290	. . . . . . . . . 10 $/\$
63	2, 61, 62	sylancl 668	. . . . . . . . 9
64	63, 11, 14	divcld 10383	. . . . . . . 8
65	64, 17, 19	divcld 10383	. . . . . . 7
66	57, 60, 65	subadd23d 10008	. . . . . 6
67	65, 60	subcld 9986	. . . . . . 7
68	57, 67	addcomd 9835	. . . . . 6
69	55, 66, 68	3eqtrd 2489	. . . . 5
70		quart1.r	. . . . . 6 ; ;;
71		quart1.d	. . . . . . 7
72		1nn0 10885	. . . . . . . . . . . 12
73		6nn 10771	. . . . . . . . . . . 12
74	72, 73	decnncl 11064	. . . . . . . . . . 11 ;
75	74	nncni 10619	. . . . . . . . . 10 ;
76	75	a1i 11	. . . . . . . . 9 ;
77	74	nnne0i 10644	. . . . . . . . . 10 ;
78	77	a1i 11	. . . . . . . . 9 ;
79	59, 76, 78	divcld 10383	. . . . . . . 8 ;
80		3cn 10684	. . . . . . . . . 10
81		2nn0 10886	. . . . . . . . . . . . 13
82		5nn0 10889	. . . . . . . . . . . . 13
83	81, 82	deccl 11065	. . . . . . . . . . . 12 ;
84	83, 73	decnncl 11064	. . . . . . . . . . 11 ;;
85	84	nncni 10619	. . . . . . . . . 10 ;;
86	84	nnne0i 10644	. . . . . . . . . 10 ;;
87	80, 85, 86	divcli 10349	. . . . . . . . 9 ;;
88		mulcl 9623	. . . . . . . . 9 ;; $/\$ ;;
89	87, 63, 88	sylancr 669	. . . . . . . 8 ;;
90	79, 89	subcld 9986	. . . . . . 7 ; ;;
91	71, 90, 57	addsubd 10007	. . . . . 6 ; ;; ; ;;
92	70, 91	eqtr4d 2488	. . . . 5 ; ;;
93	69, 92	oveq12d 6308	. . . 4 ; ;;
94	71, 90	addcld 9662	. . . . 5 ; ;;
95	67, 57, 94	ppncand 10026	. . . 4 ; ;; ; ;;
96	67, 71, 90	add12d 9856	. . . . 5 ; ;; ; ;;
97	60, 89	addcld 9662	. . . . . . . 8 ;;
98	65, 79	addcld 9662	. . . . . . . 8 ;
99	97, 98	negsubdi2d 10002	. . . . . . 7 ;; ; ; ;;
100	65, 79	addcomd 9835	. . . . . . . . . 10 ; ;
101	100	oveq2d 6306	. . . . . . . . 9 ;; ; ;; ;
102	60, 89, 79, 65	addsub4d 10033	. . . . . . . . 9 ;; ; ; ;;
103	80	a1i 11	. . . . . . . . . . . . . . . 16
104	85	a1i 11	. . . . . . . . . . . . . . . 16 ;;
105	86	a1i 11	. . . . . . . . . . . . . . . 16 ;;
106	103, 63, 104, 105	divassd 10418	. . . . . . . . . . . . . . 15 ;; ;;
107	103, 63, 104, 105	div23d 10420	. . . . . . . . . . . . . . 15 ;; ;;
108		1p2e3 10734	. . . . . . . . . . . . . . . . . 18
109	108	oveq1i 6300	. . . . . . . . . . . . . . . . 17 ;; ;;
110		1cnd 9659	. . . . . . . . . . . . . . . . . 18
111	63, 104, 105	divcld 10383	. . . . . . . . . . . . . . . . . 18 ;;
112	110, 35, 111	adddird 9668	. . . . . . . . . . . . . . . . 17 ;; ;; ;;
113	109, 112	syl5eqr 2499	. . . . . . . . . . . . . . . 16 ;; ;; ;;
114	111	mulid2d 9661	. . . . . . . . . . . . . . . . 17 ;; ;;
115	114	oveq1d 6305	. . . . . . . . . . . . . . . 16 ;; ;; ;; ;;
116	113, 115	eqtrd 2485	. . . . . . . . . . . . . . 15 ;; ;; ;;
117	106, 107, 116	3eqtr3d 2493	. . . . . . . . . . . . . 14 ;; ;; ;;
118	43	oveq1i 6300	. . . . . . . . . . . . . . . 16
119	65, 17, 19	divcld 10383	. . . . . . . . . . . . . . . . 17
120	103, 110, 119	adddird 9668	. . . . . . . . . . . . . . . 16
121	118, 120	syl5eq 2497	. . . . . . . . . . . . . . 15
122	65, 17, 19	divcan2d 10385	. . . . . . . . . . . . . . 15
123	119	mulid2d 9661	. . . . . . . . . . . . . . . . 17
124	64, 17, 17, 19, 19	divdiv1d 10414	. . . . . . . . . . . . . . . . . 18
125		4t4e16 11124	. . . . . . . . . . . . . . . . . . 19 ;
126	125	oveq2i 6301	. . . . . . . . . . . . . . . . . 18 ;
127	124, 126	syl6eq 2501	. . . . . . . . . . . . . . . . 17 ;
128	63, 11, 76, 14, 78	divdiv1d 10414	. . . . . . . . . . . . . . . . . 18 ; ;
129	10, 75	mulcli 9648	. . . . . . . . . . . . . . . . . . . . 21 ;
130	129	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
131	10, 75, 13, 77	mulne0i 10255	. . . . . . . . . . . . . . . . . . . . 21 ;
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
133	63, 130, 132	divcld 10383	. . . . . . . . . . . . . . . . . . 19 ;
134	133, 35, 37	divcan2d 10385	. . . . . . . . . . . . . . . . . 18 ; ;
135	63, 130, 35, 132, 37	divdiv1d 10414	. . . . . . . . . . . . . . . . . . . 20 ; ;
136	10, 75, 30	mul32i 9829	. . . . . . . . . . . . . . . . . . . . . 22 ; ;
137		2exp4 15057	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
138		8t2e16 11139	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
139	137, 138	eqtr4i 2476	. . . . . . . . . . . . . . . . . . . . . . 23
140	139, 137	oveq12i 6302	. . . . . . . . . . . . . . . . . . . . . 22 ;
141		4p4e8 10746	. . . . . . . . . . . . . . . . . . . . . . . 24
142	141	oveq2i 6301	. . . . . . . . . . . . . . . . . . . . . . 23
143		expadd 12314	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
144	30, 61, 61, 143	mp3an 1364	. . . . . . . . . . . . . . . . . . . . . . 23
145		2exp8 15060	. . . . . . . . . . . . . . . . . . . . . . 23 ;;
146	142, 144, 145	3eqtr3i 2481	. . . . . . . . . . . . . . . . . . . . . 22 ;;
147	136, 140, 146	3eqtr2i 2479	. . . . . . . . . . . . . . . . . . . . 21 ; ;;
148	147	oveq2i 6301	. . . . . . . . . . . . . . . . . . . 20 ; ;;
149	135, 148	syl6eq 2501	. . . . . . . . . . . . . . . . . . 19 ; ;;
150	149	oveq2d 6306	. . . . . . . . . . . . . . . . . 18 ; ;;
151	128, 134, 150	3eqtr2d 2491	. . . . . . . . . . . . . . . . 17 ; ;;
152	123, 127, 151	3eqtrd 2489	. . . . . . . . . . . . . . . 16 ;;
153	152	oveq2d 6306	. . . . . . . . . . . . . . 15 ;;
154	121, 122, 153	3eqtr3d 2493	. . . . . . . . . . . . . 14 ;;
155	117, 154	oveq12d 6308	. . . . . . . . . . . . 13 ;; ;; ;; ;;
156		mulcl 9623	. . . . . . . . . . . . . . 15 $/\$
157	80, 119, 156	sylancr 669	. . . . . . . . . . . . . 14
158		mulcl 9623	. . . . . . . . . . . . . . 15 $/\$ ;; ;;
159	30, 111, 158	sylancr 669	. . . . . . . . . . . . . 14 ;;
160	111, 157, 159	pnpcan2d 10024	. . . . . . . . . . . . 13 ;; ;; ;; ;;
161	155, 160	eqtrd 2485	. . . . . . . . . . . 12 ;; ;;
162	161	oveq2d 6306	. . . . . . . . . . 11 ; ;; ; ;;
163	79, 111, 157	addsub12d 10009	. . . . . . . . . . 11 ; ;; ;; ;
164	162, 163	eqtrd 2485	. . . . . . . . . 10 ; ;; ;; ;
165	59, 11, 35, 14, 37	divdiv1d 10414	. . . . . . . . . . . . . . . 16
166	138	oveq2i 6301	. . . . . . . . . . . . . . . 16 ;
167	165, 166	syl6eq 2501	. . . . . . . . . . . . . . 15 ;
168	167	oveq2d 6306	. . . . . . . . . . . . . 14 ;
169	60, 35, 37	divcan2d 10385	. . . . . . . . . . . . . 14
170	79	2timesd 10855	. . . . . . . . . . . . . 14 ; ; ;
171	168, 169, 170	3eqtr3d 2493	. . . . . . . . . . . . 13 ; ;
172	171	oveq1d 6305	. . . . . . . . . . . 12 ; ; ; ;
173	79, 79	pncand 9987	. . . . . . . . . . . 12 ; ; ; ;
174	172, 173	eqtrd 2485	. . . . . . . . . . 11 ; ;
175	174	oveq1d 6305	. . . . . . . . . 10 ; ;; ; ;;
176		quart1.p	. . . . . . . . . . . . 13
177	176	oveq1d 6305	. . . . . . . . . . . 12
178	80, 10, 13	divcli 10349	. . . . . . . . . . . . . 14
179		mulcl 9623	. . . . . . . . . . . . . 14 $/\$
180	178, 58, 179	sylancr 669	. . . . . . . . . . . . 13
181	20	sqcld 12414	. . . . . . . . . . . . 13
182	3, 180, 181	subdird 10075	. . . . . . . . . . . 12
183	2, 17, 19	sqdivd 12429	. . . . . . . . . . . . . . . 16
184	16	sqvali 12354	. . . . . . . . . . . . . . . . . 18
185	184, 125	eqtri 2473	. . . . . . . . . . . . . . . . 17 ;
186	185	oveq2i 6301	. . . . . . . . . . . . . . . 16 ;
187	183, 186	syl6eq 2501	. . . . . . . . . . . . . . 15 ;
188	187	oveq2d 6306	. . . . . . . . . . . . . 14 ;
189	3, 58, 76, 78	divassd 10418	. . . . . . . . . . . . . 14 ; ;
190	3, 58	mulcomd 9664	. . . . . . . . . . . . . . 15
191	190	oveq1d 6305	. . . . . . . . . . . . . 14 ; ;
192	188, 189, 191	3eqtr2d 2491	. . . . . . . . . . . . 13 ;
193	178	a1i 11	. . . . . . . . . . . . . . . . . 18
194	193, 58, 58	mulassd 9666	. . . . . . . . . . . . . . . . 17
195	103, 63, 11, 14	div23d 10420	. . . . . . . . . . . . . . . . . 18
196		2p2e4 10727	. . . . . . . . . . . . . . . . . . . . 21
197	196	oveq2i 6301	. . . . . . . . . . . . . . . . . . . 20
198	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
199	2, 198, 198	expaddd 12418	. . . . . . . . . . . . . . . . . . . 20
200	197, 199	syl5eqr 2499	. . . . . . . . . . . . . . . . . . 19
201	200	oveq2d 6306	. . . . . . . . . . . . . . . . . 18
202	195, 201	eqtrd 2485	. . . . . . . . . . . . . . . . 17
203	103, 63, 11, 14	divassd 10418	. . . . . . . . . . . . . . . . 17
204	194, 202, 203	3eqtr2d 2491	. . . . . . . . . . . . . . . 16
205	204	oveq1d 6305	. . . . . . . . . . . . . . 15
206	185, 76	syl5eqel 2533	. . . . . . . . . . . . . . . 16
207	185, 77	eqnetri 2694	. . . . . . . . . . . . . . . . 17
208	207	a1i 11	. . . . . . . . . . . . . . . 16
209	180, 58, 206, 208	divassd 10418	. . . . . . . . . . . . . . 15
210	103, 64, 206, 208	divassd 10418	. . . . . . . . . . . . . . 15
211	205, 209, 210	3eqtr3d 2493	. . . . . . . . . . . . . 14
212	183	oveq2d 6306	. . . . . . . . . . . . . 14
213	185	oveq2i 6301	. . . . . . . . . . . . . . . 16 ;
214	127, 213	syl6eqr 2503	. . . . . . . . . . . . . . 15
215	214	oveq2d 6306	. . . . . . . . . . . . . 14
216	211, 212, 215	3eqtr4d 2495	. . . . . . . . . . . . 13
217	192, 216	oveq12d 6308	. . . . . . . . . . . 12 ;
218	177, 182, 217	3eqtrd 2489	. . . . . . . . . . 11 ;
219	218	oveq2d 6306	. . . . . . . . . 10 ;; ;; ;
220	164, 175, 219	3eqtr4d 2495	. . . . . . . . 9 ; ;; ;;
221	101, 102, 220	3eqtrd 2489	. . . . . . . 8 ;; ; ;;
222	221	negeqd 9869	. . . . . . 7 ;; ; ;;
223	65, 79, 60, 89	addsub4d 10033	. . . . . . 7 ; ;; ; ;;
224	99, 222, 223	3eqtr3rd 2494	. . . . . 6 ; ;; ;;
225	224	oveq2d 6306	. . . . 5 ; ;; ;;
226	3, 180	subcld 9986	. . . . . . . . 9
227	176, 226	eqeltrd 2529	. . . . . . . 8
228	227, 181	mulcld 9663	. . . . . . 7
229	111, 228	addcld 9662	. . . . . 6 ;;
230	71, 229	negsubd 9992	. . . . 5 ;; ;;
231	96, 225, 230	3eqtrd 2489	. . . 4 ; ;; ;;
232	93, 95, 231	3eqtrd 2489	. . 3 ;;
233	232	oveq2d 6306	. 2 ;; ;; ;;
234	229, 71	pncan3d 9989	. 2 ;; ;;
235	233, 234	eqtr2d 2486	1 ;;

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1444

wcel 1887

wne 2622 (class class class)co 6290

cc 9537

cc0 9539

c1 9540

caddc 9542

cmul 9544

cmin 9860

cneg 9861

cdiv 10269

c2 10659

c3 10660

c4 10661

c5 10662

c6 10663

c8 10665

cn0 10869 ;cdc 11051

cexp 12272

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-seq 12214 df-exp 12273

This theorem is referenced by: quart1 23782

W3C validator