quartlem1 - Metamath Proof Explorer

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

Theorem quartlem1 23769

Description: Lemma for quart 23773. (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 10680	. . . . . . . . . 10
2		quartlem1.p	. . . . . . . . . 10
3		sqmul 12337	. . . . . . . . . 10 $/\$
4	1, 2, 3	sylancr 667	. . . . . . . . 9
5		sq2 12370	. . . . . . . . . 10
6	5	oveq1i 6311	. . . . . . . . 9
7	4, 6	syl6eq 2479	. . . . . . . 8
8	7	oveq1d 6316	. . . . . . 7
9		4cn 10687	. . . . . . . . 9
10	9	a1i 11	. . . . . . . 8
11		3cn 10684	. . . . . . . . 9
12	11	a1i 11	. . . . . . . 8
13	2	sqcld 12413	. . . . . . . 8
14	10, 12, 13	subdird 10075	. . . . . . 7
15	8, 14	eqtr4d 2466	. . . . . 6
16		ax-1cn 9597	. . . . . . . . . 10
17		3p1e4 10735	. . . . . . . . . 10
18	9, 11, 16, 17	subaddrii 9964	. . . . . . . . 9
19	18	oveq1i 6311	. . . . . . . 8
20		mulid2 9641	. . . . . . . 8
21	19, 20	syl5eq 2475	. . . . . . 7
22	13, 21	syl 17	. . . . . 6
23	15, 22	eqtr2d 2464	. . . . 5
24	23	oveq1d 6316	. . . 4 ; ;
25		mulcl 9623	. . . . . . 7 $/\$
26	1, 2, 25	sylancr 667	. . . . . 6
27	26	sqcld 12413	. . . . 5
28		mulcl 9623	. . . . . 6 $/\$
29	11, 13, 28	sylancr 667	. . . . 5
30		1nn0 10885	. . . . . . . 8
31		2nn 10767	. . . . . . . 8
32	30, 31	decnncl 11064	. . . . . . 7 ;
33	32	nncni 10619	. . . . . 6 ;
34		quartlem1.r	. . . . . 6
35		mulcl 9623	. . . . . 6 ; $/\$ ;
36	33, 34, 35	sylancr 667	. . . . 5 ;
37	27, 29, 36	subsubd 10014	. . . 4 ; ;
38	24, 37	eqtr4d 2466	. . 3 ; ;
39		quartlem1.u	. . 3 ;
40		mulcl 9623	. . . . . . 7 $/\$
41	9, 34, 40	sylancr 667	. . . . . 6
42	12, 13, 41	subdid 10074	. . . . 5
43		4t3e12 11123	. . . . . . . . 9 ;
44	9, 11, 43	mulcomli 9650	. . . . . . . 8 ;
45	44	oveq1i 6311	. . . . . . 7 ;
46	12, 10, 34	mulassd 9666	. . . . . . 7
47	45, 46	syl5eqr 2477	. . . . . 6 ;
48	47	oveq2d 6317	. . . . 5 ;
49	42, 48	eqtr4d 2466	. . . 4 ;
50	49	oveq2d 6317	. . 3 ;
51	38, 39, 50	3eqtr4d 2473	. 2
52	1	a1i 11	. . . . . . . . . 10
53		3nn0 10887	. . . . . . . . . . 11
54	53	a1i 11	. . . . . . . . . 10
55	52, 2, 54	mulexpd 12430	. . . . . . . . 9
56		cu2 12372	. . . . . . . . . 10
57	56	oveq1i 6311	. . . . . . . . 9
58	55, 57	syl6eq 2479	. . . . . . . 8
59	58	oveq2d 6317	. . . . . . 7
60		8cn 10695	. . . . . . . . 9
61	60	a1i 11	. . . . . . . 8
62		expcl 12289	. . . . . . . . 9 $/\$
63	2, 53, 62	sylancl 666	. . . . . . . 8
64	52, 61, 63	mul12d 9842	. . . . . . 7
65	59, 64	eqtrd 2463	. . . . . 6
66		9cn 10697	. . . . . . . . 9
67	66	a1i 11	. . . . . . . 8
68		mulcl 9623	. . . . . . . . 9 $/\$
69	1, 63, 68	sylancr 667	. . . . . . . 8
70	2, 34	mulcld 9663	. . . . . . . . 9
71		mulcl 9623	. . . . . . . . 9 $/\$
72	60, 70, 71	sylancr 667	. . . . . . . 8
73	67, 69, 72	subdid 10074	. . . . . . 7
74	26, 13, 41	subdid 10074	. . . . . . . . 9
75	52, 2, 13	mulassd 9666	. . . . . . . . . . 11
76	2, 13	mulcomd 9664	. . . . . . . . . . . . 13
77		df-3 10669	. . . . . . . . . . . . . . 15
78	77	oveq2i 6312	. . . . . . . . . . . . . 14
79		2nn0 10886	. . . . . . . . . . . . . . 15
80		expp1 12278	. . . . . . . . . . . . . . 15 $/\$
81	2, 79, 80	sylancl 666	. . . . . . . . . . . . . 14
82	78, 81	syl5eq 2475	. . . . . . . . . . . . 13
83	76, 82	eqtr4d 2466	. . . . . . . . . . . 12
84	83	oveq2d 6317	. . . . . . . . . . 11
85	75, 84	eqtrd 2463	. . . . . . . . . 10
86	52, 2, 10, 34	mul4d 9845	. . . . . . . . . . 11
87		4t2e8 10763	. . . . . . . . . . . . 13
88	9, 1, 87	mulcomli 9650	. . . . . . . . . . . 12
89	88	oveq1i 6311	. . . . . . . . . . 11
90	86, 89	syl6eq 2479	. . . . . . . . . 10
91	85, 90	oveq12d 6319	. . . . . . . . 9
92	74, 91	eqtrd 2463	. . . . . . . 8
93	92	oveq2d 6317	. . . . . . 7
94		9t8e72 11152	. . . . . . . . . 10 ;
95	94	oveq1i 6311	. . . . . . . . 9 ;
96	67, 61, 70	mulassd 9666	. . . . . . . . 9
97	95, 96	syl5eqr 2477	. . . . . . . 8 ;
98	97	oveq2d 6317	. . . . . . 7 ;
99	73, 93, 98	3eqtr4d 2473	. . . . . 6 ;
100	65, 99	oveq12d 6319	. . . . 5 ;
101		mulcl 9623	. . . . . . 7 $/\$
102	60, 69, 101	sylancr 667	. . . . . 6
103		mulcl 9623	. . . . . . 7 $/\$
104	66, 69, 103	sylancr 667	. . . . . 6
105		7nn0 10891	. . . . . . . . 9
106	105, 31	decnncl 11064	. . . . . . . 8 ;
107	106	nncni 10619	. . . . . . 7 ;
108		mulcl 9623	. . . . . . 7 ; $/\$ ;
109	107, 70, 108	sylancr 667	. . . . . 6 ;
110	102, 104, 109	subsubd 10014	. . . . 5 ; ;
111	104, 102	negsubdi2d 10002	. . . . . . 7
112	67, 61, 69	subdird 10075	. . . . . . . . 9
113		8p1e9 10740	. . . . . . . . . . . 12
114	66, 60, 16, 113	subaddrii 9964	. . . . . . . . . . 11
115	114	oveq1i 6311	. . . . . . . . . 10
116	69	mulid2d 9661	. . . . . . . . . 10
117	115, 116	syl5eq 2475	. . . . . . . . 9
118	112, 117	eqtr3d 2465	. . . . . . . 8
119	118	negeqd 9869	. . . . . . 7
120	111, 119	eqtr3d 2465	. . . . . 6
121	120	oveq1d 6316	. . . . 5 ; ;
122	100, 110, 121	3eqtrd 2467	. . . 4 ;
123		7nn 10772	. . . . . . 7
124	79, 123	decnncl 11064	. . . . . 6 ;
125	124	nncni 10619	. . . . 5 ;
126		quartlem1.q	. . . . . 6
127	126	sqcld 12413	. . . . 5
128		mulneg2 10056	. . . . 5 ; $/\$ ; ;
129	125, 127, 128	sylancr 667	. . . 4 ; ;
130	122, 129	oveq12d 6319	. . 3 ; ; ;
131	69	negcld 9973	. . . . 5
132		mulcl 9623	. . . . . 6 ; $/\$ ;
133	125, 127, 132	sylancr 667	. . . . 5 ;
134	131, 109, 133	addsubd 10007	. . . 4 ; ; ; ;
135	131, 109	addcld 9662	. . . . 5 ;
136	135, 133	negsubd 9992	. . . 4 ; ; ; ;
137		quartlem1.v	. . . 4 ; ;
138	134, 136, 137	3eqtr4d 2473	. . 3 ; ;
139	130, 138	eqtr2d 2464	. 2 ;
140	51, 139	jca 534	1 $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 370

wceq 1437

wcel 1868 (class class class)co 6301

cc 9537

c1 9540

caddc 9542

cmul 9544

cmin 9860

cneg 9861

c2 10659

c3 10660

c4 10661

c7 10664

c8 10665

c9 10666

cn0 10869 ;cdc 11051

cexp 12271

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 4551 ax-pow 4598 ax-pr 4656 ax-un 6593 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 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-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 4760 df-id 4764 df-po 4770 df-so 4771 df-fr 4808 df-we 4810 df-xp 4855 df-rel 4856 df-cnv 4857 df-co 4858 df-dm 4859 df-rn 4860 df-res 4861 df-ima 4862 df-pred 5395 df-ord 5441 df-on 5442 df-lim 5443 df-suc 5444 df-iota 5561 df-fun 5599 df-fn 5600 df-f 5601 df-f1 5602 df-fo 5603 df-f1o 5604 df-fv 5605 df-riota 6263 df-ov 6304 df-oprab 6305 df-mpt2 6306 df-om 6703 df-2nd 6804 df-wrecs 7032 df-recs 7094 df-rdg 7132 df-er 7367 df-en 7574 df-dom 7575 df-sdom 7576 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 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 12213 df-exp 12272

This theorem is referenced by: quart 23773

W3C validator