quartlem1 - Metamath Proof Explorer

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

Theorem quartlem1 23314

Description: Lemma for quart 23318. (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 10627	. . . . . . . . . 10
2		quartlem1.p	. . . . . . . . . 10
3		sqmul 12234	. . . . . . . . . 10 $/\$
4	1, 2, 3	sylancr 663	. . . . . . . . 9
5		sq2 12267	. . . . . . . . . 10
6	5	oveq1i 6306	. . . . . . . . 9
7	4, 6	syl6eq 2514	. . . . . . . 8
8	7	oveq1d 6311	. . . . . . 7
9		4cn 10634	. . . . . . . . 9
10	9	a1i 11	. . . . . . . 8
11		3cn 10631	. . . . . . . . 9
12	11	a1i 11	. . . . . . . 8
13	2	sqcld 12311	. . . . . . . 8
14	10, 12, 13	subdird 10034	. . . . . . 7
15	8, 14	eqtr4d 2501	. . . . . 6
16		ax-1cn 9567	. . . . . . . . . 10
17		3p1e4 10682	. . . . . . . . . 10
18	9, 11, 16, 17	subaddrii 9928	. . . . . . . . 9
19	18	oveq1i 6306	. . . . . . . 8
20		mulid2 9611	. . . . . . . 8
21	19, 20	syl5eq 2510	. . . . . . 7
22	13, 21	syl 16	. . . . . 6
23	15, 22	eqtr2d 2499	. . . . 5
24	23	oveq1d 6311	. . . 4 ; ;
25		mulcl 9593	. . . . . . 7 $/\$
26	1, 2, 25	sylancr 663	. . . . . 6
27	26	sqcld 12311	. . . . 5
28		mulcl 9593	. . . . . 6 $/\$
29	11, 13, 28	sylancr 663	. . . . 5
30		1nn0 10832	. . . . . . . 8
31		2nn 10714	. . . . . . . 8
32	30, 31	decnncl 11013	. . . . . . 7 ;
33	32	nncni 10566	. . . . . 6 ;
34		quartlem1.r	. . . . . 6
35		mulcl 9593	. . . . . 6 ; $/\$ ;
36	33, 34, 35	sylancr 663	. . . . 5 ;
37	27, 29, 36	subsubd 9978	. . . 4 ; ;
38	24, 37	eqtr4d 2501	. . 3 ; ;
39		quartlem1.u	. . 3 ;
40		mulcl 9593	. . . . . . 7 $/\$
41	9, 34, 40	sylancr 663	. . . . . 6
42	12, 13, 41	subdid 10033	. . . . 5
43		4t3e12 11072	. . . . . . . . 9 ;
44	9, 11, 43	mulcomli 9620	. . . . . . . 8 ;
45	44	oveq1i 6306	. . . . . . 7 ;
46	12, 10, 34	mulassd 9636	. . . . . . 7
47	45, 46	syl5eqr 2512	. . . . . 6 ;
48	47	oveq2d 6312	. . . . 5 ;
49	42, 48	eqtr4d 2501	. . . 4 ;
50	49	oveq2d 6312	. . 3 ;
51	38, 39, 50	3eqtr4d 2508	. 2
52	1	a1i 11	. . . . . . . . . 10
53		3nn0 10834	. . . . . . . . . . 11
54	53	a1i 11	. . . . . . . . . 10
55	52, 2, 54	mulexpd 12328	. . . . . . . . 9
56		cu2 12269	. . . . . . . . . 10
57	56	oveq1i 6306	. . . . . . . . 9
58	55, 57	syl6eq 2514	. . . . . . . 8
59	58	oveq2d 6312	. . . . . . 7
60		8cn 10642	. . . . . . . . 9
61	60	a1i 11	. . . . . . . 8
62		expcl 12187	. . . . . . . . 9 $/\$
63	2, 53, 62	sylancl 662	. . . . . . . 8
64	52, 61, 63	mul12d 9806	. . . . . . 7
65	59, 64	eqtrd 2498	. . . . . 6
66		9cn 10644	. . . . . . . . 9
67	66	a1i 11	. . . . . . . 8
68		mulcl 9593	. . . . . . . . 9 $/\$
69	1, 63, 68	sylancr 663	. . . . . . . 8
70	2, 34	mulcld 9633	. . . . . . . . 9
71		mulcl 9593	. . . . . . . . 9 $/\$
72	60, 70, 71	sylancr 663	. . . . . . . 8
73	67, 69, 72	subdid 10033	. . . . . . 7
74	26, 13, 41	subdid 10033	. . . . . . . . 9
75	52, 2, 13	mulassd 9636	. . . . . . . . . . 11
76	2, 13	mulcomd 9634	. . . . . . . . . . . . 13
77		df-3 10616	. . . . . . . . . . . . . . 15
78	77	oveq2i 6307	. . . . . . . . . . . . . 14
79		2nn0 10833	. . . . . . . . . . . . . . 15
80		expp1 12176	. . . . . . . . . . . . . . 15 $/\$
81	2, 79, 80	sylancl 662	. . . . . . . . . . . . . 14
82	78, 81	syl5eq 2510	. . . . . . . . . . . . 13
83	76, 82	eqtr4d 2501	. . . . . . . . . . . 12
84	83	oveq2d 6312	. . . . . . . . . . 11
85	75, 84	eqtrd 2498	. . . . . . . . . 10
86	52, 2, 10, 34	mul4d 9809	. . . . . . . . . . 11
87		4t2e8 10710	. . . . . . . . . . . . 13
88	9, 1, 87	mulcomli 9620	. . . . . . . . . . . 12
89	88	oveq1i 6306	. . . . . . . . . . 11
90	86, 89	syl6eq 2514	. . . . . . . . . 10
91	85, 90	oveq12d 6314	. . . . . . . . 9
92	74, 91	eqtrd 2498	. . . . . . . 8
93	92	oveq2d 6312	. . . . . . 7
94		9t8e72 11101	. . . . . . . . . 10 ;
95	94	oveq1i 6306	. . . . . . . . 9 ;
96	67, 61, 70	mulassd 9636	. . . . . . . . 9
97	95, 96	syl5eqr 2512	. . . . . . . 8 ;
98	97	oveq2d 6312	. . . . . . 7 ;
99	73, 93, 98	3eqtr4d 2508	. . . . . 6 ;
100	65, 99	oveq12d 6314	. . . . 5 ;
101		mulcl 9593	. . . . . . 7 $/\$
102	60, 69, 101	sylancr 663	. . . . . 6
103		mulcl 9593	. . . . . . 7 $/\$
104	66, 69, 103	sylancr 663	. . . . . 6
105		7nn0 10838	. . . . . . . . 9
106	105, 31	decnncl 11013	. . . . . . . 8 ;
107	106	nncni 10566	. . . . . . 7 ;
108		mulcl 9593	. . . . . . 7 ; $/\$ ;
109	107, 70, 108	sylancr 663	. . . . . 6 ;
110	102, 104, 109	subsubd 9978	. . . . 5 ; ;
111	104, 102	negsubdi2d 9966	. . . . . . 7
112	67, 61, 69	subdird 10034	. . . . . . . . 9
113		8p1e9 10687	. . . . . . . . . . . 12
114	66, 60, 16, 113	subaddrii 9928	. . . . . . . . . . 11
115	114	oveq1i 6306	. . . . . . . . . 10
116	69	mulid2d 9631	. . . . . . . . . 10
117	115, 116	syl5eq 2510	. . . . . . . . 9
118	112, 117	eqtr3d 2500	. . . . . . . 8
119	118	negeqd 9833	. . . . . . 7
120	111, 119	eqtr3d 2500	. . . . . 6
121	120	oveq1d 6311	. . . . 5 ; ;
122	100, 110, 121	3eqtrd 2502	. . . 4 ;
123		7nn 10719	. . . . . . 7
124	79, 123	decnncl 11013	. . . . . 6 ;
125	124	nncni 10566	. . . . 5 ;
126		quartlem1.q	. . . . . 6
127	126	sqcld 12311	. . . . 5
128		mulneg2 10015	. . . . 5 ; $/\$ ; ;
129	125, 127, 128	sylancr 663	. . . 4 ; ;
130	122, 129	oveq12d 6314	. . 3 ; ; ;
131	69	negcld 9937	. . . . 5
132		mulcl 9593	. . . . . 6 ; $/\$ ;
133	125, 127, 132	sylancr 663	. . . . 5 ;
134	131, 109, 133	addsubd 9971	. . . 4 ; ; ; ;
135	131, 109	addcld 9632	. . . . 5 ;
136	135, 133	negsubd 9956	. . . 4 ; ; ; ;
137		quartlem1.v	. . . 4 ; ;
138	134, 136, 137	3eqtr4d 2508	. . 3 ; ;
139	130, 138	eqtr2d 2499	. 2 ;
140	51, 139	jca 532	1 $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1395

wcel 1819 (class class class)co 6296

cc 9507

c1 9510

caddc 9512

cmul 9514

cmin 9824

cneg 9825

c2 10606

c3 10607

c4 10608

c7 10611

c8 10612

c9 10613

cn0 10816 ;cdc 11000

cexp 12169

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-2nd 6800 df-recs 7060 df-rdg 7094 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-seq 12111 df-exp 12170

This theorem is referenced by: quart 23318

W3C validator