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

Theorem renegcli 10941
Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 10943 is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Hypothesis
Ref Expression
renegcl.1 𝐴 ∈ ℝ
Assertion
Ref Expression
renegcli -𝐴 ∈ ℝ

Proof of Theorem renegcli
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 renegcl.1 . 2 𝐴 ∈ ℝ
2 ax-rnegex 10602 . 2 (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3 recn 10621 . . . . 5 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4 df-neg 10867 . . . . . . 7 -𝐴 = (0 − 𝐴)
54eqeq1i 2831 . . . . . 6 (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6 0cn 10627 . . . . . . 7 0 ∈ ℂ
71recni 10649 . . . . . . 7 𝐴 ∈ ℂ
8 subadd 10883 . . . . . . 7 ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
96, 7, 8mp3an12 1444 . . . . . 6 (𝑥 ∈ ℂ → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
105, 9syl5bb 284 . . . . 5 (𝑥 ∈ ℂ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
113, 10syl 17 . . . 4 (𝑥 ∈ ℝ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
12 eleq1a 2913 . . . 4 (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ))
1311, 12sylbird 261 . . 3 (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
1413rexlimiv 3285 . 2 (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
151, 2, 14mp2b 10 1 -𝐴 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1530  wcel 2107  wrex 3144  (class class class)co 7150  cc 10529  cr 10530  0cc0 10531   + caddc 10534  cmin 10864  -cneg 10865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-po 5473  df-so 5474  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8284  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-ltxr 10674  df-sub 10866  df-neg 10867
This theorem is referenced by:  resubcli  10942  renegcl  10943  recgt0ii  11540  inelr  11622  cju  11628  neg1rr  11746  sincos2sgn  15542  dvdslelem  15654  divalglem1  15740  divalglem6  15744  modsubi  16403  neghalfpire  24985  coseq0negpitopi  25023  pige3ALT  25039  negpitopissre  25056  eff1o  25065  ellogrn  25075  logimclad  25088  logneg  25103  logcj  25121  argregt0  25125  argrege0  25126  argimgt0  25127  argimlt0  25128  logimul  25129  logneg2  25130  logcnlem3  25159  dvloglem  25163  logf1o2  25165  efopnlem2  25172  cxpsqrtlem  25217  abscxpbnd  25266  logreclem  25272  ang180lem2  25320  asinneg  25396  asinsin  25402  asin1  25404  asinrecl  25412  atanlogaddlem  25423  atanlogsublem  25425  atanlogsub  25426  atantan  25433  atanbndlem  25435  birthday  25465  ppiub  25713  lgsdir2lem1  25834  ex-fl  28159  ex-ceil  28160  normlem2  28821  logdivsqrle  31826  logi  32869  bj-pinftyccb  34401  bj-minftyccb  34405  bj-pinftynminfty  34407  cos2h  34769  tan2h  34770  renegclALT  35985  fourierdlem5  42282  fourierdlem9  42286  fourierdlem18  42295  fourierdlem24  42301  fourierdlem38  42315  fourierdlem40  42317  fourierdlem43  42320  fourierdlem44  42321  fourierdlem46  42322  fourierdlem50  42326  fourierdlem62  42338  fourierdlem66  42342  fourierdlem74  42350  fourierdlem75  42351  fourierdlem76  42352  fourierdlem77  42353  fourierdlem78  42354  fourierdlem83  42359  fourierdlem85  42361  fourierdlem87  42363  fourierdlem88  42364  fourierdlem93  42369  fourierdlem94  42370  fourierdlem95  42371  fourierdlem101  42377  fourierdlem102  42378  fourierdlem103  42379  fourierdlem104  42380  fourierdlem111  42387  fourierdlem112  42388  fourierdlem113  42389  fourierdlem114  42390  sqwvfoura  42398  sqwvfourb  42399  fouriersw  42401  fouriercn  42402
  Copyright terms: Public domain W3C validator