Theorem m1m1sr 11080

Description: Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)

Assertion

Ref	Expression
m1m1sr	⊢ (-1R ·R -1R) = 1R

Proof of Theorem m1m1sr

Step	Hyp	Ref	Expression
1		df-m1r 11049	. . 3 ⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
2	1, 1	oveq12i 7425	. 2 ⊢ (-1R ·R -1R) = ([⟨1P, (1P +P 1P)⟩] ~R ·R [⟨1P, (1P +P 1P)⟩] ~R )
3		df-1r 11048	. . 3 ⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
4		1pr 11002	. . . . 5 ⊢ 1P ∈ P
5		addclpr 11005	. . . . . 6 ⊢ ((1P ∈ P ∧ 1P ∈ P) → (1P +P 1P) ∈ P)
6	4, 4, 5	mp2an 704	. . . . 5 ⊢ (1P +P 1P) ∈ P
7		mulsrpr 11063	. . . . 5 ⊢ (((1P ∈ P ∧ (1P +P 1P) ∈ P) ∧ (1P ∈ P ∧ (1P +P 1P) ∈ 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 )
8	4, 6, 4, 6, 7	mp4an 705	. . . 4 ⊢ ([⟨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
9		addasspr 11009	. . . . . 6 ⊢ ((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 11016	. . . . . . . . 9 ⊢ (1P ∈ P → (1P ·P 1P) = 1P)
11	4, 10	ax-mp 5	. . . . . . . 8 ⊢ (1P ·P 1P) = 1P
12		distrpr 11015	. . . . . . . . 9 ⊢ ((1P +P 1P) ·P (1P +P 1P)) = (((1P +P 1P) ·P 1P) +P ((1P +P 1P) ·P 1P))
13		mulcompr 11010	. . . . . . . . . 10 ⊢ (1P ·P (1P +P 1P)) = ((1P +P 1P) ·P 1P)
14	13	oveq1i 7423	. . . . . . . . 9 ⊢ ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P)) = (((1P +P 1P) ·P 1P) +P ((1P +P 1P) ·P 1P))
15	12, 14	eqtr4i 2795	. . . . . . . 8 ⊢ ((1P +P 1P) ·P (1P +P 1P)) = ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P))
16	11, 15	oveq12i 7425	. . . . . . 7 ⊢ ((1P ·P 1P) +P ((1P +P 1P) ·P (1P +P 1P))) = (1P +P ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P)))
17	16	oveq2i 7424	. . . . . 6 ⊢ (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))))
18	9, 17	eqtr4i 2795	. . . . 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))))
19		mulclpr 11007	. . . . . . . 8 ⊢ ((1P ∈ P ∧ 1P ∈ P) → (1P ·P 1P) ∈ P)
20	4, 4, 19	mp2an 704	. . . . . . 7 ⊢ (1P ·P 1P) ∈ P
21		mulclpr 11007	. . . . . . . 8 ⊢ (((1P +P 1P) ∈ P ∧ (1P +P 1P) ∈ P) → ((1P +P 1P) ·P (1P +P 1P)) ∈ P)
22	6, 6, 21	mp2an 704	. . . . . . 7 ⊢ ((1P +P 1P) ·P (1P +P 1P)) ∈ P
23		addclpr 11005	. . . . . . 7 ⊢ (((1P ·P 1P) ∈ P ∧ ((1P +P 1P) ·P (1P +P 1P)) ∈ P) → ((1P ·P 1P) +P ((1P +P 1P) ·P (1P +P 1P))) ∈ P)
24	20, 22, 23	mp2an 704	. . . . . 6 ⊢ ((1P ·P 1P) +P ((1P +P 1P) ·P (1P +P 1P))) ∈ P
25		mulclpr 11007	. . . . . . . 8 ⊢ ((1P ∈ P ∧ (1P +P 1P) ∈ P) → (1P ·P (1P +P 1P)) ∈ P)
26	4, 6, 25	mp2an 704	. . . . . . 7 ⊢ (1P ·P (1P +P 1P)) ∈ P
27		mulclpr 11007	. . . . . . . 8 ⊢ (((1P +P 1P) ∈ P ∧ 1P ∈ P) → ((1P +P 1P) ·P 1P) ∈ P)
28	6, 4, 27	mp2an 704	. . . . . . 7 ⊢ ((1P +P 1P) ·P 1P) ∈ P
29		addclpr 11005	. . . . . . 7 ⊢ (((1P ·P (1P +P 1P)) ∈ P ∧ ((1P +P 1P) ·P 1P) ∈ P) → ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P)) ∈ P)
30	26, 28, 29	mp2an 704	. . . . . 6 ⊢ ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P)) ∈ P
31		enreceq 11053	. . . . . 6 ⊢ ((((1P +P 1P) ∈ P ∧ 1P ∈ P) ∧ (((1P ·P 1P) +P ((1P +P 1P) ·P (1P +P 1P))) ∈ P ∧ ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P)) ∈ 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))))))
32	6, 4, 24, 30, 31	mp4an 705	. . . . 5 ⊢ ([⟨(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)))))
33	18, 32	mpbir 234	. . . 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
34	8, 33	eqtr4i 2795	. . 3 ⊢ ([⟨1P, (1P +P 1P)⟩] ~R ·R [⟨1P, (1P +P 1P)⟩] ~R ) = [⟨(1P +P 1P), 1P⟩] ~R
35	3, 34	eqtr4i 2795	. 2 ⊢ 1R = ([⟨1P, (1P +P 1P)⟩] ~R ·R [⟨1P, (1P +P 1P)⟩] ~R )
36	2, 35	eqtr4i 2795	1 ⊢ (-1R ·R -1R) = 1R

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ⟨cop 4600  (class class class)co 7413  [cec 8694  Pcnp 10846  1_Pc1p 10847   +_P cpp 10848   ·_P cmp 10849   ~_R cer 10851  1_Rc1r 10854  -1_Rcm1r 10855   ·_R cmr 10857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5273  ax-pow 5339  ax-pr 5407  ax-un 7735  ax-inf2 9612

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-oadd 8459  df-omul 8460  df-er 8696  df-ec 8698  df-qs 8702  df-ni 10859  df-pli 10860  df-mi 10861  df-lti 10862  df-plpq 10895  df-mpq 10896  df-ltpq 10897  df-enq 10898  df-nq 10899  df-erq 10900  df-plq 10901  df-mq 10902  df-1nq 10903  df-rq 10904  df-ltnq 10905  df-np 10968  df-1p 10969  df-plp 10970  df-mp 10971  df-ltp 10972  df-enr 11042  df-nr 11043  df-mr 11045  df-1r 11048  df-m1r 11049

This theorem is referenced by:  sqgt0sr  11093