quartlem1 - Metamath Proof Explorer

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

Theorem quartlem1 22395

Description: Lemma for quart 22399. (Contributed by Mario Carneiro, 6-May-2015.)

**Hypotheses**
Ref	Expression
quartlem1.p
quartlem1.q
quartlem1.r
quartlem1.u	;
quartlem1.v	; ;

**Assertion**
Ref	Expression
quartlem1	$/\$ ;

**Proof of Theorem quartlem1**
Step	Hyp	Ref	Expression
1		2cn 10507	. . . . . . . . . 10
2		quartlem1.p	. . . . . . . . . 10
3		sqmul 12050	. . . . . . . . . 10 $/\$
4	1, 2, 3	sylancr 663	. . . . . . . . 9
5		sq2 12083	. . . . . . . . . 10
6	5	oveq1i 6213	. . . . . . . . 9
7	4, 6	syl6eq 2511	. . . . . . . 8
8	7	oveq1d 6218	. . . . . . 7
9		4cn 10514	. . . . . . . . 9
10	9	a1i 11	. . . . . . . 8
11		3cn 10511	. . . . . . . . 9
12	11	a1i 11	. . . . . . . 8
13	2	sqcld 12127	. . . . . . . 8
14	10, 12, 13	subdird 9916	. . . . . . 7
15	8, 14	eqtr4d 2498	. . . . . 6
16		ax-1cn 9455	. . . . . . . . . 10
17		3p1e4 10562	. . . . . . . . . 10
18	9, 11, 16, 17	subaddrii 9812	. . . . . . . . 9
19	18	oveq1i 6213	. . . . . . . 8
20		mulid2 9499	. . . . . . . 8
21	19, 20	syl5eq 2507	. . . . . . 7
22	13, 21	syl 16	. . . . . 6
23	15, 22	eqtr2d 2496	. . . . 5
24	23	oveq1d 6218	. . . 4 ; ;
25		mulcl 9481	. . . . . . 7 $/\$
26	1, 2, 25	sylancr 663	. . . . . 6
27	26	sqcld 12127	. . . . 5
28		mulcl 9481	. . . . . 6 $/\$
29	11, 13, 28	sylancr 663	. . . . 5
30		1nn0 10710	. . . . . . . 8
31		2nn 10594	. . . . . . . 8
32	30, 31	decnncl 10883	. . . . . . 7 ;
33	32	nncni 10447	. . . . . 6 ;
34		quartlem1.r	. . . . . 6
35		mulcl 9481	. . . . . 6 ; $/\$ ;
36	33, 34, 35	sylancr 663	. . . . 5 ;
37	27, 29, 36	subsubd 9862	. . . 4 ; ;
38	24, 37	eqtr4d 2498	. . 3 ; ;
39		quartlem1.u	. . 3 ;
40		mulcl 9481	. . . . . . 7 $/\$
41	9, 34, 40	sylancr 663	. . . . . 6
42	12, 13, 41	subdid 9915	. . . . 5
43		4t3e12 10942	. . . . . . . . 9 ;
44	9, 11, 43	mulcomli 9508	. . . . . . . 8 ;
45	44	oveq1i 6213	. . . . . . 7 ;
46	12, 10, 34	mulassd 9524	. . . . . . 7
47	45, 46	syl5eqr 2509	. . . . . 6 ;
48	47	oveq2d 6219	. . . . 5 ;
49	42, 48	eqtr4d 2498	. . . 4 ;
50	49	oveq2d 6219	. . 3 ;
51	38, 39, 50	3eqtr4d 2505	. 2
52	1	a1i 11	. . . . . . . . . 10
53		3nn0 10712	. . . . . . . . . . 11
54	53	a1i 11	. . . . . . . . . 10
55	52, 2, 54	mulexpd 12144	. . . . . . . . 9
56		cu2 12085	. . . . . . . . . 10
57	56	oveq1i 6213	. . . . . . . . 9
58	55, 57	syl6eq 2511	. . . . . . . 8
59	58	oveq2d 6219	. . . . . . 7
60		8cn 10522	. . . . . . . . 9
61	60	a1i 11	. . . . . . . 8
62		expcl 12004	. . . . . . . . 9 $/\$
63	2, 53, 62	sylancl 662	. . . . . . . 8
64	52, 61, 63	mul12d 9693	. . . . . . 7
65	59, 64	eqtrd 2495	. . . . . 6
66		9cn 10524	. . . . . . . . 9
67	66	a1i 11	. . . . . . . 8
68		mulcl 9481	. . . . . . . . 9 $/\$
69	1, 63, 68	sylancr 663	. . . . . . . 8
70	2, 34	mulcld 9521	. . . . . . . . 9
71		mulcl 9481	. . . . . . . . 9 $/\$
72	60, 70, 71	sylancr 663	. . . . . . . 8
73	67, 69, 72	subdid 9915	. . . . . . 7
74	26, 13, 41	subdid 9915	. . . . . . . . 9
75	52, 2, 13	mulassd 9524	. . . . . . . . . . 11
76	2, 13	mulcomd 9522	. . . . . . . . . . . . 13
77		df-3 10496	. . . . . . . . . . . . . . 15
78	77	oveq2i 6214	. . . . . . . . . . . . . 14
79		2nn0 10711	. . . . . . . . . . . . . . 15
80		expp1 11993	. . . . . . . . . . . . . . 15 $/\$
81	2, 79, 80	sylancl 662	. . . . . . . . . . . . . 14
82	78, 81	syl5eq 2507	. . . . . . . . . . . . 13
83	76, 82	eqtr4d 2498	. . . . . . . . . . . 12
84	83	oveq2d 6219	. . . . . . . . . . 11
85	75, 84	eqtrd 2495	. . . . . . . . . 10
86	52, 2, 10, 34	mul4d 9696	. . . . . . . . . . 11
87		4t2e8 10590	. . . . . . . . . . . . 13
88	9, 1, 87	mulcomli 9508	. . . . . . . . . . . 12
89	88	oveq1i 6213	. . . . . . . . . . 11
90	86, 89	syl6eq 2511	. . . . . . . . . 10
91	85, 90	oveq12d 6221	. . . . . . . . 9
92	74, 91	eqtrd 2495	. . . . . . . 8
93	92	oveq2d 6219	. . . . . . 7
94		9t8e72 10971	. . . . . . . . . 10 ;
95	94	oveq1i 6213	. . . . . . . . 9 ;
96	67, 61, 70	mulassd 9524	. . . . . . . . 9
97	95, 96	syl5eqr 2509	. . . . . . . 8 ;
98	97	oveq2d 6219	. . . . . . 7 ;
99	73, 93, 98	3eqtr4d 2505	. . . . . 6 ;
100	65, 99	oveq12d 6221	. . . . 5 ;
101		mulcl 9481	. . . . . . 7 $/\$
102	60, 69, 101	sylancr 663	. . . . . 6
103		mulcl 9481	. . . . . . 7 $/\$
104	66, 69, 103	sylancr 663	. . . . . 6
105		7nn0 10716	. . . . . . . . 9
106	105, 31	decnncl 10883	. . . . . . . 8 ;
107	106	nncni 10447	. . . . . . 7 ;
108		mulcl 9481	. . . . . . 7 ; $/\$ ;
109	107, 70, 108	sylancr 663	. . . . . 6 ;
110	102, 104, 109	subsubd 9862	. . . . 5 ; ;
111	104, 102	negsubdi2d 9850	. . . . . . 7
112	67, 61, 69	subdird 9916	. . . . . . . . 9
113		8p1e9 10567	. . . . . . . . . . . 12
114	66, 60, 16, 113	subaddrii 9812	. . . . . . . . . . 11
115	114	oveq1i 6213	. . . . . . . . . 10
116	69	mulid2d 9519	. . . . . . . . . 10
117	115, 116	syl5eq 2507	. . . . . . . . 9
118	112, 117	eqtr3d 2497	. . . . . . . 8
119	118	negeqd 9719	. . . . . . 7
120	111, 119	eqtr3d 2497	. . . . . 6
121	120	oveq1d 6218	. . . . 5 ; ;
122	100, 110, 121	3eqtrd 2499	. . . 4 ;
123		7nn 10599	. . . . . . 7
124	79, 123	decnncl 10883	. . . . . 6 ;
125	124	nncni 10447	. . . . 5 ;
126		quartlem1.q	. . . . . 6
127	126	sqcld 12127	. . . . 5
128		mulneg2 9897	. . . . 5 ; $/\$ ; ;
129	125, 127, 128	sylancr 663	. . . 4 ; ;
130	122, 129	oveq12d 6221	. . 3 ; ; ;
131	69	negcld 9821	. . . . 5
132		mulcl 9481	. . . . . 6 ; $/\$ ;
133	125, 127, 132	sylancr 663	. . . . 5 ;
134	131, 109, 133	addsubd 9855	. . . 4 ; ; ; ;
135	131, 109	addcld 9520	. . . . 5 ;
136	135, 133	negsubd 9840	. . . 4 ; ; ; ;
137		quartlem1.v	. . . 4 ; ;
138	134, 136, 137	3eqtr4d 2505	. . 3 ; ;
139	130, 138	eqtr2d 2496	. 2 ;
140	51, 139	jca 532	1 $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1370

wcel 1758 (class class class)co 6203

cc 9395

c1 9398

caddc 9400

cmul 9402

cmin 9710

cneg 9711

c2 10486

c3 10487

c4 10488

c7 10491

c8 10492

c9 10493

cn0 10694 ;cdc 10870

cexp 11986

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485 ax-cnex 9453 ax-resscn 9454 ax-1cn 9455 ax-icn 9456 ax-addcl 9457 ax-addrcl 9458 ax-mulcl 9459 ax-mulrcl 9460 ax-mulcom 9461 ax-addass 9462 ax-mulass 9463 ax-distr 9464 ax-i2m1 9465 ax-1ne0 9466 ax-1rid 9467 ax-rnegex 9468 ax-rrecex 9469 ax-cnre 9470 ax-pre-lttri 9471 ax-pre-lttrn 9472 ax-pre-ltadd 9473 ax-pre-mulgt0 9474

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-nel 2651 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-pss 3455 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-tp 3993 df-op 3995 df-uni 4203 df-iun 4284 df-br 4404 df-opab 4462 df-mpt 4463 df-tr 4497 df-eprel 4743 df-id 4747 df-po 4752 df-so 4753 df-fr 4790 df-we 4792 df-ord 4833 df-on 4834 df-lim 4835 df-suc 4836 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-riota 6164 df-ov 6206 df-oprab 6207 df-mpt2 6208 df-om 6590 df-2nd 6691 df-recs 6945 df-rdg 6979 df-er 7214 df-en 7424 df-dom 7425 df-sdom 7426 df-pnf 9535 df-mnf 9536 df-xr 9537 df-ltxr 9538 df-le 9539 df-sub 9712 df-neg 9713 df-nn 10438 df-2 10495 df-3 10496 df-4 10497 df-5 10498 df-6 10499 df-7 10500 df-8 10501 df-9 10502 df-10 10503 df-n0 10695 df-z 10762 df-dec 10871 df-uz 10977 df-seq 11928 df-exp 11987

This theorem is referenced by: quart 22399

W3C validator