xmulneg1 - Metamath Proof Explorer

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

Theorem xmulneg1 11473

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

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

**Proof of Theorem xmulneg1**
Step	Hyp	Ref	Expression
1		xneg0 11423	. . . . . . . . 9
2	1	eqeq2i 2485	. . . . . . . 8
3		0xr 9652	. . . . . . . . 9
4		xneg11 11426	. . . . . . . . 9 $/\$
5	3, 4	mpan2 671	. . . . . . . 8
6	2, 5	syl5bbr 259	. . . . . . 7
7	6	adantr 465	. . . . . 6 $/\$
8	7	orbi1d 702	. . . . 5 $/\$ $\/$ $\/$
9	8	ifbid 3967	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
10		xnegpnf 11420	. . . . . . . . . . . . . 14
11	10	eqeq2i 2485	. . . . . . . . . . . . 13
12		simpll 753	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$
13		pnfxr 11333	. . . . . . . . . . . . . 14
14		xneg11 11426	. . . . . . . . . . . . . 14 $/\$
15	12, 13, 14	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
16	11, 15	syl5bbr 259	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
17	16	anbi2d 703	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$
18		xnegmnf 11421	. . . . . . . . . . . . . 14
19	18	eqeq2i 2485	. . . . . . . . . . . . 13
20		mnfxr 11335	. . . . . . . . . . . . . 14
21		xneg11 11426	. . . . . . . . . . . . . 14 $/\$
22	12, 20, 21	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
23	19, 22	syl5bbr 259	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
24	23	anbi2d 703	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$
25	17, 24	orbi12d 709	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
26		xlt0neg1 11430	. . . . . . . . . . . . . . 15
27	26	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$
28	27	bicomd 201	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
29	28	anbi1d 704	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$
30		xlt0neg2 11431	. . . . . . . . . . . . . . 15
31	30	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$
32	31	bicomd 201	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
33	32	anbi1d 704	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$
34	29, 33	orbi12d 709	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35		orcom 387	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	34, 35	syl6bb 261	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
37	25, 36	orbi12d 709	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
38	37	biimpar 485	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
39		iftrue 3951	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
40	38, 39	syl 16	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
41		xmullem2 11469	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
42	41	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
43	23	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$
44	16	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$
45	43, 44	orbi12d 709	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	28	anbi1d 704	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$
47	32	anbi1d 704	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$
48	46, 47	orbi12d 709	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
49		orcom 387	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
50	48, 49	syl6bb 261	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
51	45, 50	orbi12d 709	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
52	51	notbid 294	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
53	42, 52	sylibrd 234	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
54	53	imp 429	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
55		iffalse 3954	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
56	54, 55	syl 16	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
57		iftrue 3951	. . . . . . . . . 10 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
58	57	adantl 466	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
59		xnegeq 11418	. . . . . . . . 9 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
60	58, 59	syl 16	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
61	60, 10	syl6eq 2524	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
62	40, 56, 61	3eqtr4d 2518	. . . . . 6 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
63	51	biimpar 485	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
64		iftrue 3951	. . . . . . . . . 10 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
65	63, 64	syl 16	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
66	42	con2d 115	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
67	66	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
68		iffalse 3954	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
69	67, 68	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
70		iftrue 3951	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
71	70	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
72	69, 71	eqtrd 2508	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
73		xnegeq 11418	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
74	72, 73	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
75	74, 18	syl6eq 2524	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
76	65, 75	eqtr4d 2511	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
77	76	adantlr 714	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
78	37	notbid 294	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
79	78	biimpar 485	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
80	79	adantr 465	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
81		iffalse 3954	. . . . . . . . 9 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
82	80, 81	syl 16	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
83	52	biimpar 485	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
84	83	adantlr 714	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
85	84, 55	syl 16	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
86	68	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
87		iffalse 3954	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
88	87	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
89	86, 88	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
90		xnegeq 11418	. . . . . . . . . 10 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
91	89, 90	syl 16	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
92		xmullem 11468	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
93	92	recnd 9634	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
94		ancom 450	. . . . . . . . . . . . . . 15 $/\$ $/\$
95		orcom 387	. . . . . . . . . . . . . . . 16 $\/$ $\/$
96	95	notbii 296	. . . . . . . . . . . . . . 15 $\/$ $\/$
97	94, 96	anbi12i 697	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
98		orcom 387	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
99	98	notbii 296	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
100	97, 99	anbi12i 697	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
101		orcom 387	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
102	101	notbii 296	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
103		xmullem 11468	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
104	100, 102, 103	syl2anb 479	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
105	104	recnd 9634	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
106	93, 105	mulneg1d 10021	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
107		rexneg 11422	. . . . . . . . . . . 12
108	92, 107	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
109	108	oveq1d 6310	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
110	92, 104	remulcld 9636	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
111		rexneg 11422	. . . . . . . . . . 11
112	110, 111	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
113	106, 109, 112	3eqtr4d 2518	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
114	91, 113	eqtr4d 2511	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
115	82, 85, 114	3eqtr4d 2518	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
116	77, 115	pm2.61dan 789	. . . . . 6 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
117	62, 116	pm2.61dan 789	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
118	117	ifeq2da 3976	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
119	9, 118	eqtrd 2508	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
120		xnegeq 11418	. . . . 5 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
121	120, 1	syl6eq 2524	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
122		xnegeq 11418	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
123	121, 122	ifsb 3958	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
124	119, 123	syl6eqr 2526	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
125		xnegcl 11424	. . 3
126		xmulval 11436	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
127	125, 126	sylan 471	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
128		xmulval 11436	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
129		xnegeq 11418	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
130	128, 129	syl 16	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
131	124, 127, 130	3eqtr4d 2518	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1379

wcel 1767

cif 3945 class class class wbr 4453 (class class class)co 6295

cr 9503

cc0 9504

cmul 9509

cpnf 9637

cmnf 9638

cxr 9639

clt 9640

cneg 9818

cxne 11327

cxmu 11329

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-cnex 9560 ax-resscn 9561 ax-1cn 9562 ax-icn 9563 ax-addcl 9564 ax-addrcl 9565 ax-mulcl 9566 ax-mulrcl 9567 ax-mulcom 9568 ax-addass 9569 ax-mulass 9570 ax-distr 9571 ax-i2m1 9572 ax-1ne0 9573 ax-1rid 9574 ax-rnegex 9575 ax-rrecex 9576 ax-cnre 9577 ax-pre-lttri 9578 ax-pre-lttrn 9579 ax-pre-ltadd 9580

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2822 df-rex 2823 df-reu 2824 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-op 4040 df-uni 4252 df-br 4454 df-opab 4512 df-mpt 4513 df-id 4801 df-po 4806 df-so 4807 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 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 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-er 7323 df-en 7529 df-dom 7530 df-sdom 7531 df-pnf 9642 df-mnf 9643 df-xr 9644 df-ltxr 9645 df-le 9646 df-sub 9819 df-neg 9820 df-xneg 11330 df-xmul 11332

This theorem is referenced by: xmulneg2 11474 xmulpnf1n 11482 xmulm1 11485 xmulass 11491 xadddi 11499 xadddi2 11501 xrsmulgzz 27490

W3C validator