quart1lem - Metamath Proof Explorer

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

Theorem quart1lem 23768

Description: Lemma for quart1 23769. (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 9664	. . . . . . . . . 10
5	4	halfcld 10858	. . . . . . . . 9
6	1, 5	subcld 9987	. . . . . . . 8
7		3nn0 10888	. . . . . . . . . 10
8		expcl 12290	. . . . . . . . . 10 $/\$
9	2, 7, 8	sylancl 666	. . . . . . . . 9
10		8cn 10696	. . . . . . . . . 10
11	10	a1i 11	. . . . . . . . 9
12		8nn 10774	. . . . . . . . . . 11
13	12	nnne0i 10645	. . . . . . . . . 10
14	13	a1i 11	. . . . . . . . 9
15	9, 11, 14	divcld 10384	. . . . . . . 8
16		4cn 10688	. . . . . . . . . 10
17	16	a1i 11	. . . . . . . . 9
18		4ne0 10707	. . . . . . . . . 10
19	18	a1i 11	. . . . . . . . 9
20	2, 17, 19	divcld 10384	. . . . . . . 8
21	6, 15, 20	adddird 9669	. . . . . . 7
22		quart1.q	. . . . . . . 8
23	22	oveq1d 6317	. . . . . . 7
24	1, 2, 17, 19	divassd 10419	. . . . . . . . . 10
25	2	sqvald 12413	. . . . . . . . . . . . . . 15
26	25	oveq1d 6317	. . . . . . . . . . . . . 14
27	2, 2, 3	mul32d 9844	. . . . . . . . . . . . . 14
28	26, 27	eqtrd 2463	. . . . . . . . . . . . 13
29	28	oveq1d 6317	. . . . . . . . . . . 12
30		2cn 10681	. . . . . . . . . . . . . 14
31		4t2e8 10764	. . . . . . . . . . . . . 14
32	16, 30, 31	mulcomli 9651	. . . . . . . . . . . . 13
33	32	oveq2i 6313	. . . . . . . . . . . 12
34	29, 33	syl6eqr 2481	. . . . . . . . . . 11
35	30	a1i 11	. . . . . . . . . . . 12
36		2ne0 10703	. . . . . . . . . . . . 13
37	36	a1i 11	. . . . . . . . . . . 12
38	4, 35, 2, 17, 37, 19	divmuldivd 10425	. . . . . . . . . . 11
39	34, 38	eqtr4d 2466	. . . . . . . . . 10
40	24, 39	oveq12d 6320	. . . . . . . . 9
41	1, 5, 20	subdird 10076	. . . . . . . . 9
42	40, 41	eqtr4d 2466	. . . . . . . 8
43		df-4 10671	. . . . . . . . . . . . . 14
44	43	oveq2i 6313	. . . . . . . . . . . . 13
45		expp1 12279	. . . . . . . . . . . . . 14 $/\$
46	2, 7, 45	sylancl 666	. . . . . . . . . . . . 13
47	44, 46	syl5eq 2475	. . . . . . . . . . . 12
48	47	oveq1d 6317	. . . . . . . . . . 11
49	9, 2, 11, 14	div23d 10421	. . . . . . . . . . 11
50	48, 49	eqtrd 2463	. . . . . . . . . 10
51	50	oveq1d 6317	. . . . . . . . 9
52	15, 2, 17, 19	divassd 10419	. . . . . . . . 9
53	51, 52	eqtrd 2463	. . . . . . . 8
54	42, 53	oveq12d 6320	. . . . . . 7
55	21, 23, 54	3eqtr4d 2473	. . . . . 6
56	1, 2	mulcld 9664	. . . . . . . 8
57	56, 17, 19	divcld 10384	. . . . . . 7
58	2	sqcld 12414	. . . . . . . . 9
59	58, 3	mulcld 9664	. . . . . . . 8
60	59, 11, 14	divcld 10384	. . . . . . 7
61		4nn0 10889	. . . . . . . . . 10
62		expcl 12290	. . . . . . . . . 10 $/\$
63	2, 61, 62	sylancl 666	. . . . . . . . 9
64	63, 11, 14	divcld 10384	. . . . . . . 8
65	64, 17, 19	divcld 10384	. . . . . . 7
66	57, 60, 65	subadd23d 10009	. . . . . 6
67	65, 60	subcld 9987	. . . . . . 7
68	57, 67	addcomd 9836	. . . . . 6
69	55, 66, 68	3eqtrd 2467	. . . . 5
70		quart1.r	. . . . . 6 ; ;;
71		quart1.d	. . . . . . 7
72		1nn0 10886	. . . . . . . . . . . 12
73		6nn 10772	. . . . . . . . . . . 12
74	72, 73	decnncl 11065	. . . . . . . . . . 11 ;
75	74	nncni 10620	. . . . . . . . . 10 ;
76	75	a1i 11	. . . . . . . . 9 ;
77	74	nnne0i 10645	. . . . . . . . . 10 ;
78	77	a1i 11	. . . . . . . . 9 ;
79	59, 76, 78	divcld 10384	. . . . . . . 8 ;
80		3cn 10685	. . . . . . . . . 10
81		2nn0 10887	. . . . . . . . . . . . 13
82		5nn0 10890	. . . . . . . . . . . . 13
83	81, 82	deccl 11066	. . . . . . . . . . . 12 ;
84	83, 73	decnncl 11065	. . . . . . . . . . 11 ;;
85	84	nncni 10620	. . . . . . . . . 10 ;;
86	84	nnne0i 10645	. . . . . . . . . 10 ;;
87	80, 85, 86	divcli 10350	. . . . . . . . 9 ;;
88		mulcl 9624	. . . . . . . . 9 ;; $/\$ ;;
89	87, 63, 88	sylancr 667	. . . . . . . 8 ;;
90	79, 89	subcld 9987	. . . . . . 7 ; ;;
91	71, 90, 57	addsubd 10008	. . . . . 6 ; ;; ; ;;
92	70, 91	eqtr4d 2466	. . . . 5 ; ;;
93	69, 92	oveq12d 6320	. . . 4 ; ;;
94	71, 90	addcld 9663	. . . . 5 ; ;;
95	67, 57, 94	ppncand 10027	. . . 4 ; ;; ; ;;
96	67, 71, 90	add12d 9857	. . . . 5 ; ;; ; ;;
97	60, 89	addcld 9663	. . . . . . . 8 ;;
98	65, 79	addcld 9663	. . . . . . . 8 ;
99	97, 98	negsubdi2d 10003	. . . . . . 7 ;; ; ; ;;
100	65, 79	addcomd 9836	. . . . . . . . . 10 ; ;
101	100	oveq2d 6318	. . . . . . . . 9 ;; ; ;; ;
102	60, 89, 79, 65	addsub4d 10034	. . . . . . . . 9 ;; ; ; ;;
103	80	a1i 11	. . . . . . . . . . . . . . . 16
104	85	a1i 11	. . . . . . . . . . . . . . . 16 ;;
105	86	a1i 11	. . . . . . . . . . . . . . . 16 ;;
106	103, 63, 104, 105	divassd 10419	. . . . . . . . . . . . . . 15 ;; ;;
107	103, 63, 104, 105	div23d 10421	. . . . . . . . . . . . . . 15 ;; ;;
108		1p2e3 10735	. . . . . . . . . . . . . . . . . 18
109	108	oveq1i 6312	. . . . . . . . . . . . . . . . 17 ;; ;;
110		1cnd 9660	. . . . . . . . . . . . . . . . . 18
111	63, 104, 105	divcld 10384	. . . . . . . . . . . . . . . . . 18 ;;
112	110, 35, 111	adddird 9669	. . . . . . . . . . . . . . . . 17 ;; ;; ;;
113	109, 112	syl5eqr 2477	. . . . . . . . . . . . . . . 16 ;; ;; ;;
114	111	mulid2d 9662	. . . . . . . . . . . . . . . . 17 ;; ;;
115	114	oveq1d 6317	. . . . . . . . . . . . . . . 16 ;; ;; ;; ;;
116	113, 115	eqtrd 2463	. . . . . . . . . . . . . . 15 ;; ;; ;;
117	106, 107, 116	3eqtr3d 2471	. . . . . . . . . . . . . 14 ;; ;; ;;
118	43	oveq1i 6312	. . . . . . . . . . . . . . . 16
119	65, 17, 19	divcld 10384	. . . . . . . . . . . . . . . . 17
120	103, 110, 119	adddird 9669	. . . . . . . . . . . . . . . 16
121	118, 120	syl5eq 2475	. . . . . . . . . . . . . . 15
122	65, 17, 19	divcan2d 10386	. . . . . . . . . . . . . . 15
123	119	mulid2d 9662	. . . . . . . . . . . . . . . . 17
124	64, 17, 17, 19, 19	divdiv1d 10415	. . . . . . . . . . . . . . . . . 18
125		4t4e16 11125	. . . . . . . . . . . . . . . . . . 19 ;
126	125	oveq2i 6313	. . . . . . . . . . . . . . . . . 18 ;
127	124, 126	syl6eq 2479	. . . . . . . . . . . . . . . . 17 ;
128	63, 11, 76, 14, 78	divdiv1d 10415	. . . . . . . . . . . . . . . . . 18 ; ;
129	10, 75	mulcli 9649	. . . . . . . . . . . . . . . . . . . . 21 ;
130	129	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
131	10, 75, 13, 77	mulne0i 10256	. . . . . . . . . . . . . . . . . . . . 21 ;
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ;
133	63, 130, 132	divcld 10384	. . . . . . . . . . . . . . . . . . 19 ;
134	133, 35, 37	divcan2d 10386	. . . . . . . . . . . . . . . . . 18 ; ;
135	63, 130, 35, 132, 37	divdiv1d 10415	. . . . . . . . . . . . . . . . . . . 20 ; ;
136	10, 75, 30	mul32i 9830	. . . . . . . . . . . . . . . . . . . . . 22 ; ;
137		2exp4 15045	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
138		8t2e16 11140	. . . . . . . . . . . . . . . . . . . . . . . 24 ;
139	137, 138	eqtr4i 2454	. . . . . . . . . . . . . . . . . . . . . . 23
140	139, 137	oveq12i 6314	. . . . . . . . . . . . . . . . . . . . . 22 ;
141		4p4e8 10747	. . . . . . . . . . . . . . . . . . . . . . . 24
142	141	oveq2i 6313	. . . . . . . . . . . . . . . . . . . . . . 23
143		expadd 12314	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
144	30, 61, 61, 143	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . 23
145		2exp8 15048	. . . . . . . . . . . . . . . . . . . . . . 23 ;;
146	142, 144, 145	3eqtr3i 2459	. . . . . . . . . . . . . . . . . . . . . 22 ;;
147	136, 140, 146	3eqtr2i 2457	. . . . . . . . . . . . . . . . . . . . 21 ; ;;
148	147	oveq2i 6313	. . . . . . . . . . . . . . . . . . . 20 ; ;;
149	135, 148	syl6eq 2479	. . . . . . . . . . . . . . . . . . 19 ; ;;
150	149	oveq2d 6318	. . . . . . . . . . . . . . . . . 18 ; ;;
151	128, 134, 150	3eqtr2d 2469	. . . . . . . . . . . . . . . . 17 ; ;;
152	123, 127, 151	3eqtrd 2467	. . . . . . . . . . . . . . . 16 ;;
153	152	oveq2d 6318	. . . . . . . . . . . . . . 15 ;;
154	121, 122, 153	3eqtr3d 2471	. . . . . . . . . . . . . 14 ;;
155	117, 154	oveq12d 6320	. . . . . . . . . . . . 13 ;; ;; ;; ;;
156		mulcl 9624	. . . . . . . . . . . . . . 15 $/\$
157	80, 119, 156	sylancr 667	. . . . . . . . . . . . . 14
158		mulcl 9624	. . . . . . . . . . . . . . 15 $/\$ ;; ;;
159	30, 111, 158	sylancr 667	. . . . . . . . . . . . . 14 ;;
160	111, 157, 159	pnpcan2d 10025	. . . . . . . . . . . . 13 ;; ;; ;; ;;
161	155, 160	eqtrd 2463	. . . . . . . . . . . 12 ;; ;;
162	161	oveq2d 6318	. . . . . . . . . . 11 ; ;; ; ;;
163	79, 111, 157	addsub12d 10010	. . . . . . . . . . 11 ; ;; ;; ;
164	162, 163	eqtrd 2463	. . . . . . . . . 10 ; ;; ;; ;
165	59, 11, 35, 14, 37	divdiv1d 10415	. . . . . . . . . . . . . . . 16
166	138	oveq2i 6313	. . . . . . . . . . . . . . . 16 ;
167	165, 166	syl6eq 2479	. . . . . . . . . . . . . . 15 ;
168	167	oveq2d 6318	. . . . . . . . . . . . . 14 ;
169	60, 35, 37	divcan2d 10386	. . . . . . . . . . . . . 14
170	79	2timesd 10856	. . . . . . . . . . . . . 14 ; ; ;
171	168, 169, 170	3eqtr3d 2471	. . . . . . . . . . . . 13 ; ;
172	171	oveq1d 6317	. . . . . . . . . . . 12 ; ; ; ;
173	79, 79	pncand 9988	. . . . . . . . . . . 12 ; ; ; ;
174	172, 173	eqtrd 2463	. . . . . . . . . . 11 ; ;
175	174	oveq1d 6317	. . . . . . . . . 10 ; ;; ; ;;
176		quart1.p	. . . . . . . . . . . . 13
177	176	oveq1d 6317	. . . . . . . . . . . 12
178	80, 10, 13	divcli 10350	. . . . . . . . . . . . . 14
179		mulcl 9624	. . . . . . . . . . . . . 14 $/\$
180	178, 58, 179	sylancr 667	. . . . . . . . . . . . 13
181	20	sqcld 12414	. . . . . . . . . . . . 13
182	3, 180, 181	subdird 10076	. . . . . . . . . . . 12
183	2, 17, 19	sqdivd 12429	. . . . . . . . . . . . . . . 16
184	16	sqvali 12354	. . . . . . . . . . . . . . . . . 18
185	184, 125	eqtri 2451	. . . . . . . . . . . . . . . . 17 ;
186	185	oveq2i 6313	. . . . . . . . . . . . . . . 16 ;
187	183, 186	syl6eq 2479	. . . . . . . . . . . . . . 15 ;
188	187	oveq2d 6318	. . . . . . . . . . . . . 14 ;
189	3, 58, 76, 78	divassd 10419	. . . . . . . . . . . . . 14 ; ;
190	3, 58	mulcomd 9665	. . . . . . . . . . . . . . 15
191	190	oveq1d 6317	. . . . . . . . . . . . . 14 ; ;
192	188, 189, 191	3eqtr2d 2469	. . . . . . . . . . . . 13 ;
193	178	a1i 11	. . . . . . . . . . . . . . . . . 18
194	193, 58, 58	mulassd 9667	. . . . . . . . . . . . . . . . 17
195	103, 63, 11, 14	div23d 10421	. . . . . . . . . . . . . . . . . 18
196		2p2e4 10728	. . . . . . . . . . . . . . . . . . . . 21
197	196	oveq2i 6313	. . . . . . . . . . . . . . . . . . . 20
198	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
199	2, 198, 198	expaddd 12418	. . . . . . . . . . . . . . . . . . . 20
200	197, 199	syl5eqr 2477	. . . . . . . . . . . . . . . . . . 19
201	200	oveq2d 6318	. . . . . . . . . . . . . . . . . 18
202	195, 201	eqtrd 2463	. . . . . . . . . . . . . . . . 17
203	103, 63, 11, 14	divassd 10419	. . . . . . . . . . . . . . . . 17
204	194, 202, 203	3eqtr2d 2469	. . . . . . . . . . . . . . . 16
205	204	oveq1d 6317	. . . . . . . . . . . . . . 15
206	185, 76	syl5eqel 2514	. . . . . . . . . . . . . . . 16
207	185, 77	eqnetri 2720	. . . . . . . . . . . . . . . . 17
208	207	a1i 11	. . . . . . . . . . . . . . . 16
209	180, 58, 206, 208	divassd 10419	. . . . . . . . . . . . . . 15
210	103, 64, 206, 208	divassd 10419	. . . . . . . . . . . . . . 15
211	205, 209, 210	3eqtr3d 2471	. . . . . . . . . . . . . 14
212	183	oveq2d 6318	. . . . . . . . . . . . . 14
213	185	oveq2i 6313	. . . . . . . . . . . . . . . 16 ;
214	127, 213	syl6eqr 2481	. . . . . . . . . . . . . . 15
215	214	oveq2d 6318	. . . . . . . . . . . . . 14
216	211, 212, 215	3eqtr4d 2473	. . . . . . . . . . . . 13
217	192, 216	oveq12d 6320	. . . . . . . . . . . 12 ;
218	177, 182, 217	3eqtrd 2467	. . . . . . . . . . 11 ;
219	218	oveq2d 6318	. . . . . . . . . 10 ;; ;; ;
220	164, 175, 219	3eqtr4d 2473	. . . . . . . . 9 ; ;; ;;
221	101, 102, 220	3eqtrd 2467	. . . . . . . 8 ;; ; ;;
222	221	negeqd 9870	. . . . . . 7 ;; ; ;;
223	65, 79, 60, 89	addsub4d 10034	. . . . . . 7 ; ;; ; ;;
224	99, 222, 223	3eqtr3rd 2472	. . . . . 6 ; ;; ;;
225	224	oveq2d 6318	. . . . 5 ; ;; ;;
226	3, 180	subcld 9987	. . . . . . . . 9
227	176, 226	eqeltrd 2510	. . . . . . . 8
228	227, 181	mulcld 9664	. . . . . . 7
229	111, 228	addcld 9663	. . . . . 6 ;;
230	71, 229	negsubd 9993	. . . . 5 ;; ;;
231	96, 225, 230	3eqtrd 2467	. . . 4 ; ;; ;;
232	93, 95, 231	3eqtrd 2467	. . 3 ;;
233	232	oveq2d 6318	. 2 ;; ;; ;;
234	229, 71	pncan3d 9990	. 2 ;; ;;
235	233, 234	eqtr2d 2464	1 ;;

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1437

wcel 1868

wne 2618 (class class class)co 6302

cc 9538

cc0 9540

c1 9541

caddc 9543

cmul 9545

cmin 9861

cneg 9862

cdiv 10270

c2 10660

c3 10661

c4 10662

c5 10663

c6 10664

c8 10666

cn0 10870 ;cdc 11052

cexp 12272

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-sep 4543 ax-nul 4552 ax-pow 4599 ax-pr 4657 ax-un 6594 ax-cnex 9596 ax-resscn 9597 ax-1cn 9598 ax-icn 9599 ax-addcl 9600 ax-addrcl 9601 ax-mulcl 9602 ax-mulrcl 9603 ax-mulcom 9604 ax-addass 9605 ax-mulass 9606 ax-distr 9607 ax-i2m1 9608 ax-1ne0 9609 ax-1rid 9610 ax-rnegex 9611 ax-rrecex 9612 ax-cnre 9613 ax-pre-lttri 9614 ax-pre-lttrn 9615 ax-pre-ltadd 9616 ax-pre-mulgt0 9617

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4761 df-id 4765 df-po 4771 df-so 4772 df-fr 4809 df-we 4811 df-xp 4856 df-rel 4857 df-cnv 4858 df-co 4859 df-dm 4860 df-rn 4861 df-res 4862 df-ima 4863 df-pred 5396 df-ord 5442 df-on 5443 df-lim 5444 df-suc 5445 df-iota 5562 df-fun 5600 df-fn 5601 df-f 5602 df-f1 5603 df-fo 5604 df-f1o 5605 df-fv 5606 df-riota 6264 df-ov 6305 df-oprab 6306 df-mpt2 6307 df-om 6704 df-2nd 6805 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-pnf 9678 df-mnf 9679 df-xr 9680 df-ltxr 9681 df-le 9682 df-sub 9863 df-neg 9864 df-div 10271 df-nn 10611 df-2 10669 df-3 10670 df-4 10671 df-5 10672 df-6 10673 df-7 10674 df-8 10675 df-9 10676 df-10 10677 df-n0 10871 df-z 10939 df-dec 11053 df-uz 11161 df-seq 12214 df-exp 12273

This theorem is referenced by: quart1 23769

W3C validator