xnegdi - Metamath Proof Explorer

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

Theorem xnegdi 11469

Description: Extended real version of xnegdi 11469. (Contributed by Mario Carneiro, 20-Aug-2015.)

**Assertion**
Ref	Expression
xnegdi

**Proof of Theorem xnegdi**
Step	Hyp	Ref	Expression
1		elxr 11354	. 2
2		elxr 11354	. . . 4
3		recn 9603	. . . . . . . 8
4		recn 9603	. . . . . . . 8
5		negdi 9899	. . . . . . . 8
6	3, 4, 5	syl2an 477	. . . . . . 7
7		readdcl 9596	. . . . . . . 8
8		rexneg 11439	. . . . . . . 8
9	7, 8	syl 16	. . . . . . 7
10		renegcl 9905	. . . . . . . 8
11		renegcl 9905	. . . . . . . 8
12		rexadd 11460	. . . . . . . 8
13	10, 11, 12	syl2an 477	. . . . . . 7
14	6, 9, 13	3eqtr4d 2508	. . . . . 6
15		rexadd 11460	. . . . . . 7
16		xnegeq 11435	. . . . . . 7
17	15, 16	syl 16	. . . . . 6
18		rexneg 11439	. . . . . . 7
19		rexneg 11439	. . . . . . 7
20	18, 19	oveqan12d 6315	. . . . . 6
21	14, 17, 20	3eqtr4d 2508	. . . . 5
22		xnegpnf 11437	. . . . . 6
23		oveq2 6304	. . . . . . . 8
24		rexr 9660	. . . . . . . . 9
25		renemnf 9663	. . . . . . . . 9
26		xaddpnf1 11454	. . . . . . . . 9
27	24, 25, 26	syl2anc 661	. . . . . . . 8
28	23, 27	sylan9eqr 2520	. . . . . . 7
29		xnegeq 11435	. . . . . . 7
30	28, 29	syl 16	. . . . . 6
31		xnegeq 11435	. . . . . . . . 9
32	31, 22	syl6eq 2514	. . . . . . . 8
33	32	oveq2d 6312	. . . . . . 7
34	18, 10	eqeltrd 2545	. . . . . . . 8
35		rexr 9660	. . . . . . . . 9
36		renepnf 9662	. . . . . . . . 9
37		xaddmnf1 11456	. . . . . . . . 9
38	35, 36, 37	syl2anc 661	. . . . . . . 8
39	34, 38	syl 16	. . . . . . 7
40	33, 39	sylan9eqr 2520	. . . . . 6
41	22, 30, 40	3eqtr4a 2524	. . . . 5
42		xnegmnf 11438	. . . . . 6
43		oveq2 6304	. . . . . . . 8
44		renepnf 9662	. . . . . . . . 9
45		xaddmnf1 11456	. . . . . . . . 9
46	24, 44, 45	syl2anc 661	. . . . . . . 8
47	43, 46	sylan9eqr 2520	. . . . . . 7
48		xnegeq 11435	. . . . . . 7
49	47, 48	syl 16	. . . . . 6
50		xnegeq 11435	. . . . . . . . 9
51	50, 42	syl6eq 2514	. . . . . . . 8
52	51	oveq2d 6312	. . . . . . 7
53		renemnf 9663	. . . . . . . . 9
54		xaddpnf1 11454	. . . . . . . . 9
55	35, 53, 54	syl2anc 661	. . . . . . . 8
56	34, 55	syl 16	. . . . . . 7
57	52, 56	sylan9eqr 2520	. . . . . 6
58	42, 49, 57	3eqtr4a 2524	. . . . 5
59	21, 41, 58	3jaodan 1294	. . . 4
60	2, 59	sylan2b 475	. . 3
61		xneg0 11440	. . . . . . 7
62		simpr 461	. . . . . . . . . 10
63	62	oveq2d 6312	. . . . . . . . 9
64		pnfaddmnf 11458	. . . . . . . . 9
65	63, 64	syl6eq 2514	. . . . . . . 8
66		xnegeq 11435	. . . . . . . 8
67	65, 66	syl 16	. . . . . . 7
68	51	adantl 466	. . . . . . . . 9
69	68	oveq2d 6312	. . . . . . . 8
70		mnfaddpnf 11459	. . . . . . . 8
71	69, 70	syl6eq 2514	. . . . . . 7
72	61, 67, 71	3eqtr4a 2524	. . . . . 6
73		xaddpnf2 11455	. . . . . . . 8
74		xnegeq 11435	. . . . . . . 8
75	73, 74	syl 16	. . . . . . 7
76		xnegcl 11441	. . . . . . . . 9
77	76	adantr 465	. . . . . . . 8
78		xnegeq 11435	. . . . . . . . . . . 12
79	78, 22	syl6eq 2514	. . . . . . . . . . 11
80		xnegneg 11442	. . . . . . . . . . . 12
81	80	eqeq1d 2459	. . . . . . . . . . 11
82	79, 81	syl5ib 219	. . . . . . . . . 10
83	82	necon3d 2681	. . . . . . . . 9
84	83	imp 429	. . . . . . . 8
85		xaddmnf2 11457	. . . . . . . 8
86	77, 84, 85	syl2anc 661	. . . . . . 7
87	22, 75, 86	3eqtr4a 2524	. . . . . 6
88	72, 87	pm2.61dane 2775	. . . . 5
89	88	adantl 466	. . . 4
90		simpl 457	. . . . . 6
91	90	oveq1d 6311	. . . . 5
92		xnegeq 11435	. . . . 5
93	91, 92	syl 16	. . . 4
94		xnegeq 11435	. . . . . . 7
95	94	adantr 465	. . . . . 6
96	95, 22	syl6eq 2514	. . . . 5
97	96	oveq1d 6311	. . . 4
98	89, 93, 97	3eqtr4d 2508	. . 3
99		simpr 461	. . . . . . . . . 10
100	99	oveq2d 6312	. . . . . . . . 9
101	100, 70	syl6eq 2514	. . . . . . . 8
102		xnegeq 11435	. . . . . . . 8
103	101, 102	syl 16	. . . . . . 7
104	32	adantl 466	. . . . . . . . 9
105	104	oveq2d 6312	. . . . . . . 8
106	105, 64	syl6eq 2514	. . . . . . 7
107	61, 103, 106	3eqtr4a 2524	. . . . . 6
108		xaddmnf2 11457	. . . . . . . 8
109		xnegeq 11435	. . . . . . . 8
110	108, 109	syl 16	. . . . . . 7
111	76	adantr 465	. . . . . . . 8
112		xnegeq 11435	. . . . . . . . . . . 12
113	112, 42	syl6eq 2514	. . . . . . . . . . 11
114	80	eqeq1d 2459	. . . . . . . . . . 11
115	113, 114	syl5ib 219	. . . . . . . . . 10
116	115	necon3d 2681	. . . . . . . . 9
117	116	imp 429	. . . . . . . 8
118		xaddpnf2 11455	. . . . . . . 8
119	111, 117, 118	syl2anc 661	. . . . . . 7
120	42, 110, 119	3eqtr4a 2524	. . . . . 6
121	107, 120	pm2.61dane 2775	. . . . 5
122	121	adantl 466	. . . 4
123		simpl 457	. . . . . 6
124	123	oveq1d 6311	. . . . 5
125		xnegeq 11435	. . . . 5
126	124, 125	syl 16	. . . 4
127		xnegeq 11435	. . . . . . 7
128	127	adantr 465	. . . . . 6
129	128, 42	syl6eq 2514	. . . . 5
130	129	oveq1d 6311	. . . 4
131	122, 126, 130	3eqtr4d 2508	. . 3
132	60, 98, 131	3jaoian 1293	. 2
133	1, 132	sylanb 472	1

Colors of variables: wff setvar class

Syntax hints: ->wi 4 /\wa 369 \/w3o 972 =wceq 1395 e.wcel 1818 =/=wne 2652 (class class class)co 6296 cc 9511 cr 9512 0cc0 9513 caddc 9516 cpnf 9646 cmnf 9647 cxr 9648 -ucneg 9829 cxne 11344 cxad 11345

This theorem is referenced by: xaddass2 11471 xposdif 11483 xadddi 11516 xrsxmet 21314

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-8 1820 ax-9 1822 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 ax-sep 4573 ax-nul 4581 ax-pow 4630 ax-pr 4691 ax-un 6592 ax-cnex 9569 ax-resscn 9570 ax-1cn 9571 ax-icn 9572 ax-addcl 9573 ax-addrcl 9574 ax-mulcl 9575 ax-mulrcl 9576 ax-mulcom 9577 ax-addass 9578 ax-mulass 9579 ax-distr 9580 ax-i2m1 9581 ax-1ne0 9582 ax-1rid 9583 ax-rnegex 9584 ax-rrecex 9585 ax-cnre 9586 ax-pre-lttri 9587 ax-pre-lttrn 9588 ax-pre-ltadd 9589

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 1613 df-nf 1617 df-sb 1740 df-eu 2286 df-mo 2287 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 3435 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-nul 3785 df-if 3942 df-pw 4014 df-sn 4030 df-pr 4032 df-op 4036 df-uni 4250 df-br 4453 df-opab 4511 df-mpt 4512 df-id 4800 df-po 4805 df-so 4806 df-xp 5010 df-rel 5011 df-cnv 5012 df-co 5013 df-dm 5014 df-rn 5015 df-res 5016 df-ima 5017 df-iota 5556 df-fun 5595 df-fn 5596 df-f 5597 df-f1 5598 df-fo 5599 df-f1o 5600 df-fv 5601 df-riota 6257 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-er 7330 df-en 7537 df-dom 7538 df-sdom 7539 df-pnf 9651 df-mnf 9652 df-xr 9653 df-ltxr 9654 df-sub 9830 df-neg 9831 df-xneg 11347 df-xadd 11348

W3C validator