Theorem renegcli 11432

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11434 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.

Step	Hyp	Ref	Expression
1		renegcl.1	. 2 ⊢ 𝐴 ∈ ℝ
2		ax-rnegex 11087	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3		recn 11106	. . . . 5 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4		df-neg 11357	. . . . . . 7 ⊢ -𝐴 = (0 − 𝐴)
5	4	eqeq1i 2738	. . . . . 6 ⊢ (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6		0cn 11114	. . . . . . 7 ⊢ 0 ∈ ℂ
7	1	recni 11136	. . . . . . 7 ⊢ 𝐴 ∈ ℂ
8		subadd 11373	. . . . . . 7 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
9	6, 7, 8	mp3an12 1453	. . . . . 6 ⊢ (𝑥 ∈ ℂ → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
10	5, 9	bitrid 283	. . . . 5 ⊢ (𝑥 ∈ ℂ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
11	3, 10	syl 17	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
12		eleq1a 2828	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ))
13	11, 12	sylbird 260	. . 3 ⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
14	13	rexlimiv 3128	. 2 ⊢ (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
15	1, 2, 14	mp2b 10	1 ⊢ -𝐴 ∈ ℝ

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3058  (class class class)co 7355  ℂcc 11014  ℝcr 11015  0cc0 11016   + caddc 11019   − cmin 11354  -cneg 11355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11073  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-addrcl 11077  ax-mulcl 11078  ax-mulrcl 11079  ax-mulcom 11080  ax-addass 11081  ax-mulass 11082  ax-distr 11083  ax-i2m1 11084  ax-1ne0 11085  ax-1rid 11086  ax-rnegex 11087  ax-rrecex 11088  ax-cnre 11089  ax-pre-lttri 11090  ax-pre-lttrn 11091  ax-pre-ltadd 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-er 8631  df-en 8879  df-dom 8880  df-sdom 8881  df-pnf 11158  df-mnf 11159  df-ltxr 11161  df-sub 11356  df-neg 11357

This theorem is referenced by:  resubcli  11433  renegcl  11434  recgt0ii  12038  neg1rr  12121  cju  12131  sincos2sgn  16113  dvdslelem  16230  divalglem1  16315  divalglem6  16319  modsubi  16994  neghalfpire  26411  coseq0negpitopi  26449  pige3ALT  26466  negpitopissre  26486  eff1o  26495  ellogrn  26505  logimclad  26518  logi  26533  logneg  26534  logcj  26552  argregt0  26556  argrege0  26557  argimgt0  26558  argimlt0  26559  logimul  26560  logneg2  26561  logcnlem3  26590  dvloglem  26594  logf1o2  26596  efopnlem2  26603  cxpsqrtlem  26648  abscxpbnd  26700  logreclem  26709  ang180lem2  26757  asinneg  26833  asinsin  26839  asin1  26841  asinrecl  26849  atanlogaddlem  26860  atanlogsublem  26862  atanlogsub  26863  atantan  26870  atanbndlem  26872  birthday  26901  ppiub  27152  lgsdir2lem1  27273  ex-fl  30438  ex-ceil  30439  normlem2  31102  logdivsqrle  34674  bj-pinftyccb  37276  bj-minftyccb  37280  bj-pinftynminfty  37282  cos2h  37661  tan2h  37662  renegclALT  39072  fourierdlem5  46224  fourierdlem9  46228  fourierdlem18  46237  fourierdlem24  46243  fourierdlem38  46257  fourierdlem40  46259  fourierdlem43  46262  fourierdlem44  46263  fourierdlem46  46264  fourierdlem50  46268  fourierdlem62  46280  fourierdlem66  46284  fourierdlem74  46292  fourierdlem75  46293  fourierdlem76  46294  fourierdlem77  46295  fourierdlem78  46296  fourierdlem83  46301  fourierdlem85  46303  fourierdlem87  46305  fourierdlem88  46306  fourierdlem93  46311  fourierdlem94  46312  fourierdlem95  46313  fourierdlem101  46319  fourierdlem102  46320  fourierdlem103  46321  fourierdlem104  46322  fourierdlem111  46329  fourierdlem112  46330  fourierdlem113  46331  fourierdlem114  46332  sqwvfoura  46340  sqwvfourb  46341  fouriersw  46343  fouriercn  46344  nthrucw  46998