xmulneg1 - Metamath Proof Explorer

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

Theorem xmulneg1 11382

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

**Assertion**
Ref	Expression
xmulneg1	$/\$

**Proof of Theorem xmulneg1**
Step	Hyp	Ref	Expression
1		xneg0 11332	. . . . . . . . 9
2	1	eqeq2i 2400	. . . . . . . 8
3		0xr 9551	. . . . . . . . 9
4		xneg11 11335	. . . . . . . . 9 $/\$
5	3, 4	mpan2 669	. . . . . . . 8
6	2, 5	syl5bbr 259	. . . . . . 7
7	6	adantr 463	. . . . . 6 $/\$
8	7	orbi1d 700	. . . . 5 $/\$ $\/$ $\/$
9	8	ifbid 3879	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
10		xnegpnf 11329	. . . . . . . . . . . . . 14
11	10	eqeq2i 2400	. . . . . . . . . . . . 13
12		simpll 751	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$
13		pnfxr 11242	. . . . . . . . . . . . . 14
14		xneg11 11335	. . . . . . . . . . . . . 14 $/\$
15	12, 13, 14	sylancl 660	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
16	11, 15	syl5bbr 259	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
17	16	anbi2d 701	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$
18		xnegmnf 11330	. . . . . . . . . . . . . 14
19	18	eqeq2i 2400	. . . . . . . . . . . . 13
20		mnfxr 11244	. . . . . . . . . . . . . 14
21		xneg11 11335	. . . . . . . . . . . . . 14 $/\$
22	12, 20, 21	sylancl 660	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
23	19, 22	syl5bbr 259	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
24	23	anbi2d 701	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$
25	17, 24	orbi12d 707	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
26		xlt0neg1 11339	. . . . . . . . . . . . . . 15
27	26	ad2antrr 723	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$
28	27	bicomd 201	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
29	28	anbi1d 702	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$
30		xlt0neg2 11340	. . . . . . . . . . . . . . 15
31	30	ad2antrr 723	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$
32	31	bicomd 201	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
33	32	anbi1d 702	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$
34	29, 33	orbi12d 707	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35		orcom 385	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	34, 35	syl6bb 261	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
37	25, 36	orbi12d 707	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
38	37	biimpar 483	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
39	38	iftrued 3865	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
40		xmullem2 11378	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
41	40	adantr 463	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
42	23	anbi2d 701	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$
43	16	anbi2d 701	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$
44	42, 43	orbi12d 707	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
45	28	anbi1d 702	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$
46	32	anbi1d 702	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$
47	45, 46	orbi12d 707	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
48		orcom 385	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
49	47, 48	syl6bb 261	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
50	44, 49	orbi12d 707	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
51	50	notbid 292	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
52	41, 51	sylibrd 234	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
53	52	imp 427	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
54	53	iffalsed 3868	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
55		iftrue 3863	. . . . . . . . . 10 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
56	55	adantl 464	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
57		xnegeq 11327	. . . . . . . . 9 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
58	56, 57	syl 16	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
59	58, 10	syl6eq 2439	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
60	39, 54, 59	3eqtr4d 2433	. . . . . 6 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
61	50	biimpar 483	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
62	61	iftrued 3865	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
63	41	con2d 115	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
64	63	imp 427	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
65	64	iffalsed 3868	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
66		iftrue 3863	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
67	66	adantl 464	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
68	65, 67	eqtrd 2423	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
69		xnegeq 11327	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
70	68, 69	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
71	70, 18	syl6eq 2439	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
72	62, 71	eqtr4d 2426	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
73	72	adantlr 712	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
74	37	notbid 292	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
75	74	biimpar 483	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
76	75	adantr 463	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
77	76	iffalsed 3868	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
78	51	biimpar 483	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
79	78	adantlr 712	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
80	79	iffalsed 3868	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
81		iffalse 3866	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
82	81	ad2antlr 724	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
83		iffalse 3866	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
84	83	adantl 464	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
85	82, 84	eqtrd 2423	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
86		xnegeq 11327	. . . . . . . . . 10 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
87	85, 86	syl 16	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
88		xmullem 11377	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
89	88	recnd 9533	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
90		ancom 448	. . . . . . . . . . . . . . 15 $/\$ $/\$
91		orcom 385	. . . . . . . . . . . . . . . 16 $\/$ $\/$
92	91	notbii 294	. . . . . . . . . . . . . . 15 $\/$ $\/$
93	90, 92	anbi12i 695	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
94		orcom 385	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
95	94	notbii 294	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
96	93, 95	anbi12i 695	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
97		orcom 385	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
98	97	notbii 294	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
99		xmullem 11377	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
100	96, 98, 99	syl2anb 477	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
101	100	recnd 9533	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
102	89, 101	mulneg1d 9927	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
103		rexneg 11331	. . . . . . . . . . . 12
104	88, 103	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
105	104	oveq1d 6211	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
106	88, 100	remulcld 9535	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
107		rexneg 11331	. . . . . . . . . . 11
108	106, 107	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
109	102, 105, 108	3eqtr4d 2433	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
110	87, 109	eqtr4d 2426	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
111	77, 80, 110	3eqtr4d 2433	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
112	73, 111	pm2.61dan 789	. . . . . 6 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
113	60, 112	pm2.61dan 789	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
114	113	ifeq2da 3888	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
115	9, 114	eqtrd 2423	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
116		xnegeq 11327	. . . . 5 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
117	116, 1	syl6eq 2439	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
118		xnegeq 11327	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
119	117, 118	ifsb 3870	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
120	115, 119	syl6eqr 2441	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
121		xnegcl 11333	. . 3
122		xmulval 11345	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
123	121, 122	sylan 469	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
124		xmulval 11345	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
125		xnegeq 11327	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
126	124, 125	syl 16	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
127	120, 123, 126	3eqtr4d 2433	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367

wceq 1399

wcel 1826

cif 3857 class class class wbr 4367 (class class class)co 6196

cr 9402

cc0 9403

cmul 9408

cpnf 9536

cmnf 9537

cxr 9538

clt 9539

cneg 9719

cxne 11236

cxmu 11238

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-op 3951 df-uni 4164 df-br 4368 df-opab 4426 df-mpt 4427 df-id 4709 df-po 4714 df-so 4715 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-er 7229 df-en 7436 df-dom 7437 df-sdom 7438 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-xneg 11239 df-xmul 11241

This theorem is referenced by: xmulneg2 11383 xmulpnf1n 11391 xmulm1 11394 xmulass 11400 xadddi 11408 xadddi2 11410 xrsmulgzz 27819

W3C validator