Theorem m1m1sr 5222

Description: Minus one times minus one is plus one for signed reals.

Assertion

Ref	Expression
m1m1sr	|- (-1R .R -1R) = 1R

Proof of Theorem m1m1sr

Step	Hyp	Ref	Expression
1		1pr 5137	. . . . 5 |- 1P e. P.
2		addclpr 5140	. . . . . 6 |- ((1P e. P. /\ 1P e. P.) -> (1P +P. 1P) e. P.)
3	1, 1, 2	mp2an 701	. . . . 5 |- (1P +P. 1P) e. P.
4	1, 3	pm3.2i 285	. . . 4 |- (1P e. P. /\ (1P +P. 1P) e. P.)
5		mulsrpr 5205	. . . 4 |- (((1P e. P. /\ (1P +P. 1P) e. P.) /\ (1P e. P. /\ (1P +P. 1P) e. P.)) -> ([<.1P, (1P +P. 1P)>.] ~R .R [<.1P, (1P +P. 1P)>.] ~R ) = [<.((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))), ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))>.] ~R )
6	4, 4, 5	mp2an 701	. . 3 |- ([<.1P, (1P +P. 1P)>.] ~R .R [<.1P, (1P +P. 1P)>.] ~R ) = [<.((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))), ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))>.] ~R
7	1	elisseti 1825	. . . . . 6 |- 1P e. V
8		oprex 3999	. . . . . 6 |- ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P)) e. V
9	7, 8	addasspr 5144	. . . . 5 |- ((1P +P. 1P) +P. ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))) = (1P +P. (1P +P. ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))))
10		1idpr 5153	. . . . . . . 8 |- (1P e. P. -> (1P .P. 1P) = 1P)
11	1, 10	ax-mp 7	. . . . . . 7 |- (1P .P. 1P) = 1P
12	7, 7	distrpr 5152	. . . . . . . 8 |- ((1P +P. 1P) .P. (1P +P. 1P)) = (((1P +P. 1P) .P. 1P) +P. ((1P +P. 1P) .P. 1P))
13		oprex 3999	. . . . . . . . . 10 |- (1P +P. 1P) e. V
14	7, 13	mulcompr 5145	. . . . . . . . 9 |- (1P .P. (1P +P. 1P)) = ((1P +P. 1P) .P. 1P)
15	14	opreq1i 3987	. . . . . . . 8 |- ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P)) = (((1P +P. 1P) .P. 1P) +P. ((1P +P. 1P) .P. 1P))
16	12, 15	eqtr4i 1505	. . . . . . 7 |- ((1P +P. 1P) .P. (1P +P. 1P)) = ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))
17	11, 16	opreq12i 3989	. . . . . 6 |- ((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))) = (1P +P. ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P)))
18	17	opreq2i 3988	. . . . 5 |- (1P +P. ((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P)))) = (1P +P. (1P +P. ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))))
19	9, 18	eqtr4i 1505	. . . 4 |- ((1P +P. 1P) +P. ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))) = (1P +P. ((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))))
20	3, 1	pm3.2i 285	. . . . 5 |- ((1P +P. 1P) e. P. /\ 1P e. P.)
21		mulclpr 5142	. . . . . . . 8 |- ((1P e. P. /\ 1P e. P.) -> (1P .P. 1P) e. P.)
22	1, 1, 21	mp2an 701	. . . . . . 7 |- (1P .P. 1P) e. P.
23		mulclpr 5142	. . . . . . . 8 |- (((1P +P. 1P) e. P. /\ (1P +P. 1P) e. P.) -> ((1P +P. 1P) .P. (1P +P. 1P)) e. P.)
24	3, 3, 23	mp2an 701	. . . . . . 7 |- ((1P +P. 1P) .P. (1P +P. 1P)) e. P.
25		addclpr 5140	. . . . . . 7 |- (((1P .P. 1P) e. P. /\ ((1P +P. 1P) .P. (1P +P. 1P)) e. P.) -> ((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))) e. P.)
26	22, 24, 25	mp2an 701	. . . . . 6 |- ((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))) e. P.
27		mulclpr 5142	. . . . . . . 8 |- ((1P e. P. /\ (1P +P. 1P) e. P.) -> (1P .P. (1P +P. 1P)) e. P.)
28	1, 3, 27	mp2an 701	. . . . . . 7 |- (1P .P. (1P +P. 1P)) e. P.
29		mulclpr 5142	. . . . . . . 8 |- (((1P +P. 1P) e. P. /\ 1P e. P.) -> ((1P +P. 1P) .P. 1P) e. P.)
30	3, 1, 29	mp2an 701	. . . . . . 7 |- ((1P +P. 1P) .P. 1P) e. P.
31		addclpr 5140	. . . . . . 7 |- (((1P .P. (1P +P. 1P)) e. P. /\ ((1P +P. 1P) .P. 1P) e. P.) -> ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P)) e. P.)
32	28, 30, 31	mp2an 701	. . . . . 6 |- ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P)) e. P.
33	26, 32	pm3.2i 285	. . . . 5 |- (((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))) e. P. /\ ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P)) e. P.)
34		enreceq 5197	. . . . 5 |- ((((1P +P. 1P) e. P. /\ 1P e. P.) /\ (((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))) e. P. /\ ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P)) e. P.)) -> ([<.(1P +P. 1P), 1P>.] ~R = [<.((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))), ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))>.] ~R <-> ((1P +P. 1P) +P. ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))) = (1P +P. ((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))))))
35	20, 33, 34	mp2an 701	. . . 4 |- ([<.(1P +P. 1P), 1P>.] ~R = [<.((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))), ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))>.] ~R <-> ((1P +P. 1P) +P. ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))) = (1P +P. ((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P)))))
36	19, 35	mpbir 190	. . 3 |- [<.(1P +P. 1P), 1P>.] ~R = [<.((1P .P. 1P) +P. ((1P +P. 1P) .P. (1P +P. 1P))), ((1P .P. (1P +P. 1P)) +P. ((1P +P. 1P) .P. 1P))>.] ~R
37	6, 36	eqtr4i 1505	. 2 |- ([<.1P, (1P +P. 1P)>.] ~R .R [<.1P, (1P +P. 1P)>.] ~R ) = [<.(1P +P. 1P), 1P>.] ~R
38		df-m1r 5193	. . 3 |- -1R = [<.1P, (1P +P. 1P)>.] ~R
39	38, 38	opreq12i 3989	. 2 |- (-1R .R -1R) = ([<.1P, (1P +P. 1P)>.] ~R .R [<.1P, (1P +P. 1P)>.] ~R )
40		df-1r 5192	. 2 |- 1R = [<.(1P +P. 1P), 1P>.] ~R
41	37, 39, 40	3eqtr4i 1512	1 |- (-1R .R -1R) = 1R

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 960   e. wcel 962  <.cop 2423  (class class class)co 3979  [cec 4275  P.cnp 5005  1Pc1p 5006   +P. cpp 5007   .P. cmp 5008   ~R cer 5012  1Rc1r 5015  -1Rcm1r 5016   .R cmr 5018

This theorem is referenced by:  sqgt0sr 5235

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-rep 2708  ax-sep 2718  ax-nul 2725  ax-pow 2758  ax-pr 2795  ax-un 2882  ax-inf2 4642

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2012  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-pss 2066  df-nul 2292  df-if 2374  df-pw 2414  df-sn 2424  df-pr 2425  df-tp 2427  df-op 2428  df-uni 2518  df-int 2548  df-iun 2582  df-br 2635  df-opab 2682  df-tr 2696  df-eprel 2848  df-id 2851  df-po 2856  df-so 2866  df-fr 2933  df-we 2950  df-ord 2967  df-on 2968  df-lim 2969  df-suc 2970  df-om 3148  df-xp 3200  df-rel 3201  df-cnv 3202  df-co 3203  df-dm 3204  df-rn 3205  df-res 3206  df-ima 3207  df-fun 3208  df-fn 3209  df-f 3210  df-fv 3214  df-rdg 3948  df-opr 3981  df-oprab 3982  df-1st 4095  df-2nd 4096  df-1o 4149  df-oadd 4151  df-omul 4152  df-er 4277  df-ec 4279  df-qs 4282  df-ni 5020  df-pli 5021  df-mi 5022  df-lti 5023  df-plpq 5055  df-mpq 5056  df-enq 5057  df-nq 5058  df-plq 5059  df-mq 5060  df-rq 5061  df-ltq 5062  df-1q 5063  df-np 5106  df-1p 5107  df-plp 5108  df-mp 5109  df-ltp 5110  df-mpr 5185  df-enr 5186  df-nr 5187  df-mr 5189  df-1r 5192  df-m1r 5193

Copyright terms: Public domain