quartlem1 - Metamath Proof Explorer

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

Theorem quartlem1 23776

Description: Lemma for quart 23780. (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 10677	. . . . . . . . . 10
2		quartlem1.p	. . . . . . . . . 10
3		sqmul 12335	. . . . . . . . . 10 $/\$
4	1, 2, 3	sylancr 668	. . . . . . . . 9
5		sq2 12368	. . . . . . . . . 10
6	5	oveq1i 6298	. . . . . . . . 9
7	4, 6	syl6eq 2500	. . . . . . . 8
8	7	oveq1d 6303	. . . . . . 7
9		4cn 10684	. . . . . . . . 9
10	9	a1i 11	. . . . . . . 8
11		3cn 10681	. . . . . . . . 9
12	11	a1i 11	. . . . . . . 8
13	2	sqcld 12411	. . . . . . . 8
14	10, 12, 13	subdird 10072	. . . . . . 7
15	8, 14	eqtr4d 2487	. . . . . 6
16		ax-1cn 9594	. . . . . . . . . 10
17		3p1e4 10732	. . . . . . . . . 10
18	9, 11, 16, 17	subaddrii 9961	. . . . . . . . 9
19	18	oveq1i 6298	. . . . . . . 8
20		mulid2 9638	. . . . . . . 8
21	19, 20	syl5eq 2496	. . . . . . 7
22	13, 21	syl 17	. . . . . 6
23	15, 22	eqtr2d 2485	. . . . 5
24	23	oveq1d 6303	. . . 4 ; ;
25		mulcl 9620	. . . . . . 7 $/\$
26	1, 2, 25	sylancr 668	. . . . . 6
27	26	sqcld 12411	. . . . 5
28		mulcl 9620	. . . . . 6 $/\$
29	11, 13, 28	sylancr 668	. . . . 5
30		1nn0 10882	. . . . . . . 8
31		2nn 10764	. . . . . . . 8
32	30, 31	decnncl 11061	. . . . . . 7 ;
33	32	nncni 10616	. . . . . 6 ;
34		quartlem1.r	. . . . . 6
35		mulcl 9620	. . . . . 6 ; $/\$ ;
36	33, 34, 35	sylancr 668	. . . . 5 ;
37	27, 29, 36	subsubd 10011	. . . 4 ; ;
38	24, 37	eqtr4d 2487	. . 3 ; ;
39		quartlem1.u	. . 3 ;
40		mulcl 9620	. . . . . . 7 $/\$
41	9, 34, 40	sylancr 668	. . . . . 6
42	12, 13, 41	subdid 10071	. . . . 5
43		4t3e12 11120	. . . . . . . . 9 ;
44	9, 11, 43	mulcomli 9647	. . . . . . . 8 ;
45	44	oveq1i 6298	. . . . . . 7 ;
46	12, 10, 34	mulassd 9663	. . . . . . 7
47	45, 46	syl5eqr 2498	. . . . . 6 ;
48	47	oveq2d 6304	. . . . 5 ;
49	42, 48	eqtr4d 2487	. . . 4 ;
50	49	oveq2d 6304	. . 3 ;
51	38, 39, 50	3eqtr4d 2494	. 2
52	1	a1i 11	. . . . . . . . . 10
53		3nn0 10884	. . . . . . . . . . 11
54	53	a1i 11	. . . . . . . . . 10
55	52, 2, 54	mulexpd 12428	. . . . . . . . 9
56		cu2 12370	. . . . . . . . . 10
57	56	oveq1i 6298	. . . . . . . . 9
58	55, 57	syl6eq 2500	. . . . . . . 8
59	58	oveq2d 6304	. . . . . . 7
60		8cn 10692	. . . . . . . . 9
61	60	a1i 11	. . . . . . . 8
62		expcl 12287	. . . . . . . . 9 $/\$
63	2, 53, 62	sylancl 667	. . . . . . . 8
64	52, 61, 63	mul12d 9839	. . . . . . 7
65	59, 64	eqtrd 2484	. . . . . 6
66		9cn 10694	. . . . . . . . 9
67	66	a1i 11	. . . . . . . 8
68		mulcl 9620	. . . . . . . . 9 $/\$
69	1, 63, 68	sylancr 668	. . . . . . . 8
70	2, 34	mulcld 9660	. . . . . . . . 9
71		mulcl 9620	. . . . . . . . 9 $/\$
72	60, 70, 71	sylancr 668	. . . . . . . 8
73	67, 69, 72	subdid 10071	. . . . . . 7
74	26, 13, 41	subdid 10071	. . . . . . . . 9
75	52, 2, 13	mulassd 9663	. . . . . . . . . . 11
76	2, 13	mulcomd 9661	. . . . . . . . . . . . 13
77		df-3 10666	. . . . . . . . . . . . . . 15
78	77	oveq2i 6299	. . . . . . . . . . . . . 14
79		2nn0 10883	. . . . . . . . . . . . . . 15
80		expp1 12276	. . . . . . . . . . . . . . 15 $/\$
81	2, 79, 80	sylancl 667	. . . . . . . . . . . . . 14
82	78, 81	syl5eq 2496	. . . . . . . . . . . . 13
83	76, 82	eqtr4d 2487	. . . . . . . . . . . 12
84	83	oveq2d 6304	. . . . . . . . . . 11
85	75, 84	eqtrd 2484	. . . . . . . . . 10
86	52, 2, 10, 34	mul4d 9842	. . . . . . . . . . 11
87		4t2e8 10760	. . . . . . . . . . . . 13
88	9, 1, 87	mulcomli 9647	. . . . . . . . . . . 12
89	88	oveq1i 6298	. . . . . . . . . . 11
90	86, 89	syl6eq 2500	. . . . . . . . . 10
91	85, 90	oveq12d 6306	. . . . . . . . 9
92	74, 91	eqtrd 2484	. . . . . . . 8
93	92	oveq2d 6304	. . . . . . 7
94		9t8e72 11149	. . . . . . . . . 10 ;
95	94	oveq1i 6298	. . . . . . . . 9 ;
96	67, 61, 70	mulassd 9663	. . . . . . . . 9
97	95, 96	syl5eqr 2498	. . . . . . . 8 ;
98	97	oveq2d 6304	. . . . . . 7 ;
99	73, 93, 98	3eqtr4d 2494	. . . . . 6 ;
100	65, 99	oveq12d 6306	. . . . 5 ;
101		mulcl 9620	. . . . . . 7 $/\$
102	60, 69, 101	sylancr 668	. . . . . 6
103		mulcl 9620	. . . . . . 7 $/\$
104	66, 69, 103	sylancr 668	. . . . . 6
105		7nn0 10888	. . . . . . . . 9
106	105, 31	decnncl 11061	. . . . . . . 8 ;
107	106	nncni 10616	. . . . . . 7 ;
108		mulcl 9620	. . . . . . 7 ; $/\$ ;
109	107, 70, 108	sylancr 668	. . . . . 6 ;
110	102, 104, 109	subsubd 10011	. . . . 5 ; ;
111	104, 102	negsubdi2d 9999	. . . . . . 7
112	67, 61, 69	subdird 10072	. . . . . . . . 9
113		8p1e9 10737	. . . . . . . . . . . 12
114	66, 60, 16, 113	subaddrii 9961	. . . . . . . . . . 11
115	114	oveq1i 6298	. . . . . . . . . 10
116	69	mulid2d 9658	. . . . . . . . . 10
117	115, 116	syl5eq 2496	. . . . . . . . 9
118	112, 117	eqtr3d 2486	. . . . . . . 8
119	118	negeqd 9866	. . . . . . 7
120	111, 119	eqtr3d 2486	. . . . . 6
121	120	oveq1d 6303	. . . . 5 ; ;
122	100, 110, 121	3eqtrd 2488	. . . 4 ;
123		7nn 10769	. . . . . . 7
124	79, 123	decnncl 11061	. . . . . 6 ;
125	124	nncni 10616	. . . . 5 ;
126		quartlem1.q	. . . . . 6
127	126	sqcld 12411	. . . . 5
128		mulneg2 10053	. . . . 5 ; $/\$ ; ;
129	125, 127, 128	sylancr 668	. . . 4 ; ;
130	122, 129	oveq12d 6306	. . 3 ; ; ;
131	69	negcld 9970	. . . . 5
132		mulcl 9620	. . . . . 6 ; $/\$ ;
133	125, 127, 132	sylancr 668	. . . . 5 ;
134	131, 109, 133	addsubd 10004	. . . 4 ; ; ; ;
135	131, 109	addcld 9659	. . . . 5 ;
136	135, 133	negsubd 9989	. . . 4 ; ; ; ;
137		quartlem1.v	. . . 4 ; ;
138	134, 136, 137	3eqtr4d 2494	. . 3 ; ;
139	130, 138	eqtr2d 2485	. 2 ;
140	51, 139	jca 535	1 $/\$ ;

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 371

wceq 1443

wcel 1886 (class class class)co 6288

cc 9534

c1 9537

caddc 9539

cmul 9541

cmin 9857

cneg 9858

c2 10656

c3 10657

c4 10658

c7 10661

c8 10662

c9 10663

cn0 10866 ;cdc 11048

cexp 12269

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-2 10665 df-3 10666 df-4 10667 df-5 10668 df-6 10669 df-7 10670 df-8 10671 df-9 10672 df-10 10673 df-n0 10867 df-z 10935 df-dec 11049 df-uz 11157 df-seq 12211 df-exp 12270

This theorem is referenced by: quart 23780

W3C validator