ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  resubcl GIF version

Theorem resubcl 7254
Description: Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
Assertion
Ref Expression
resubcl ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)

Proof of Theorem resubcl
StepHypRef Expression
1 recn 6995 . . 3 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2 recn 6995 . . 3 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3 negsub 7238 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴𝐵))
41, 2, 3syl2an 273 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴𝐵))
5 renegcl 7251 . . 3 (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6 readdcl 6988 . . 3 ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
75, 6sylan2 270 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
84, 7eqeltrrd 2115 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97   = wceq 1243  wcel 1393  (class class class)co 5499  cc 6868  cr 6869   + caddc 6873  cmin 7162  -cneg 7163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3872  ax-pow 3924  ax-pr 3941  ax-setind 4256  ax-resscn 6957  ax-1cn 6958  ax-icn 6960  ax-addcl 6961  ax-addrcl 6962  ax-mulcl 6963  ax-addcom 6965  ax-addass 6967  ax-distr 6969  ax-i2m1 6970  ax-0id 6973  ax-rnegex 6974  ax-cnre 6976
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2308  df-rex 2309  df-reu 2310  df-rab 2312  df-v 2556  df-sbc 2762  df-dif 2917  df-un 2919  df-in 2921  df-ss 2928  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-br 3762  df-opab 3816  df-id 4027  df-xp 4338  df-rel 4339  df-cnv 4340  df-co 4341  df-dm 4342  df-iota 4854  df-fun 4891  df-fv 4897  df-riota 5455  df-ov 5502  df-oprab 5503  df-mpt2 5504  df-sub 7164  df-neg 7165
This theorem is referenced by:  peano2rem  7257  resubcld  7358  posdif  7428  lt2sub  7433  le2sub  7434  cju  7889  elz2  8284  difrp  8590  iooshf  8788  iccshftl  8831  lincmb01cmp  8838  uzsubsubfz  8878  difelfzle  8959  fzonmapblen  9010  eluzgtdifelfzo  9020  expubnd  9189  absdiflt  9566  absdifle  9567  elicc4abs  9568  abssubge0  9576  abs2difabs  9582
  Copyright terms: Public domain W3C validator