MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  m1m1sr Structured version   Visualization version   GIF version

Theorem m1m1sr 10987
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
StepHypRef Expression
1 df-m1r 10956 . . 3 -1R = [⟨1P, (1P +P 1P)⟩] ~R
21, 1oveq12i 7363 . 2 (-1R ·R -1R) = ([⟨1P, (1P +P 1P)⟩] ~R ·R [⟨1P, (1P +P 1P)⟩] ~R )
3 df-1r 10955 . . 3 1R = [⟨(1P +P 1P), 1P⟩] ~R
4 1pr 10909 . . . . 5 1PP
5 addclpr 10912 . . . . . 6 ((1PP ∧ 1PP) → (1P +P 1P) ∈ P)
64, 4, 5mp2an 690 . . . . 5 (1P +P 1P) ∈ P
7 mulsrpr 10970 . . . . 5 (((1PP ∧ (1P +P 1P) ∈ P) ∧ (1PP ∧ (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 )
84, 6, 4, 6, 7mp4an 691 . . . 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 10916 . . . . . 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 10923 . . . . . . . . 9 (1PP → (1P ·P 1P) = 1P)
114, 10ax-mp 5 . . . . . . . 8 (1P ·P 1P) = 1P
12 distrpr 10922 . . . . . . . . 9 ((1P +P 1P) ·P (1P +P 1P)) = (((1P +P 1P) ·P 1P) +P ((1P +P 1P) ·P 1P))
13 mulcompr 10917 . . . . . . . . . 10 (1P ·P (1P +P 1P)) = ((1P +P 1P) ·P 1P)
1413oveq1i 7361 . . . . . . . . 9 ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P)) = (((1P +P 1P) ·P 1P) +P ((1P +P 1P) ·P 1P))
1512, 14eqtr4i 2767 . . . . . . . 8 ((1P +P 1P) ·P (1P +P 1P)) = ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P))
1611, 15oveq12i 7363 . . . . . . 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)))
1716oveq2i 7362 . . . . . 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))))
189, 17eqtr4i 2767 . . . . 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 10914 . . . . . . . 8 ((1PP ∧ 1PP) → (1P ·P 1P) ∈ P)
204, 4, 19mp2an 690 . . . . . . 7 (1P ·P 1P) ∈ P
21 mulclpr 10914 . . . . . . . 8 (((1P +P 1P) ∈ P ∧ (1P +P 1P) ∈ P) → ((1P +P 1P) ·P (1P +P 1P)) ∈ P)
226, 6, 21mp2an 690 . . . . . . 7 ((1P +P 1P) ·P (1P +P 1P)) ∈ P
23 addclpr 10912 . . . . . . 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)
2420, 22, 23mp2an 690 . . . . . 6 ((1P ·P 1P) +P ((1P +P 1P) ·P (1P +P 1P))) ∈ P
25 mulclpr 10914 . . . . . . . 8 ((1PP ∧ (1P +P 1P) ∈ P) → (1P ·P (1P +P 1P)) ∈ P)
264, 6, 25mp2an 690 . . . . . . 7 (1P ·P (1P +P 1P)) ∈ P
27 mulclpr 10914 . . . . . . . 8 (((1P +P 1P) ∈ P ∧ 1PP) → ((1P +P 1P) ·P 1P) ∈ P)
286, 4, 27mp2an 690 . . . . . . 7 ((1P +P 1P) ·P 1P) ∈ P
29 addclpr 10912 . . . . . . 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)
3026, 28, 29mp2an 690 . . . . . 6 ((1P ·P (1P +P 1P)) +P ((1P +P 1P) ·P 1P)) ∈ P
31 enreceq 10960 . . . . . 6 ((((1P +P 1P) ∈ P ∧ 1PP) ∧ (((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))))))
326, 4, 24, 30, 31mp4an 691 . . . . 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)))))
3318, 32mpbir 230 . . . 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
348, 33eqtr4i 2767 . . 3 ([⟨1P, (1P +P 1P)⟩] ~R ·R [⟨1P, (1P +P 1P)⟩] ~R ) = [⟨(1P +P 1P), 1P⟩] ~R
353, 34eqtr4i 2767 . 2 1R = ([⟨1P, (1P +P 1P)⟩] ~R ·R [⟨1P, (1P +P 1P)⟩] ~R )
362, 35eqtr4i 2767 1 (-1R ·R -1R) = 1R
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541  wcel 2106  cop 4590  (class class class)co 7351  [cec 8604  Pcnp 10753  1Pc1p 10754   +P cpp 10755   ·P cmp 10756   ~R cer 10758  1Rc1r 10761  -1Rcm1r 10762   ·R cmr 10764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-inf2 9535
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7354  df-oprab 7355  df-mpo 7356  df-om 7795  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-oadd 8408  df-omul 8409  df-er 8606  df-ec 8608  df-qs 8612  df-ni 10766  df-pli 10767  df-mi 10768  df-lti 10769  df-plpq 10802  df-mpq 10803  df-ltpq 10804  df-enq 10805  df-nq 10806  df-erq 10807  df-plq 10808  df-mq 10809  df-1nq 10810  df-rq 10811  df-ltnq 10812  df-np 10875  df-1p 10876  df-plp 10877  df-mp 10878  df-ltp 10879  df-enr 10949  df-nr 10950  df-mr 10952  df-1r 10955  df-m1r 10956
This theorem is referenced by:  sqgt0sr  11000
  Copyright terms: Public domain W3C validator