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

Theorem reccld 11144
Description: Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
div1d.1 (𝜑𝐴 ∈ ℂ)
reccld.2 (𝜑𝐴 ≠ 0)
Assertion
Ref Expression
reccld (𝜑 → (1 / 𝐴) ∈ ℂ)

Proof of Theorem reccld
StepHypRef Expression
1 div1d.1 . 2 (𝜑𝐴 ∈ ℂ)
2 reccld.2 . 2 (𝜑𝐴 ≠ 0)
3 reccl 11040 . 2 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℂ)
41, 2, 3syl2anc 579 1 (𝜑 → (1 / 𝐴) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 2969  (class class class)co 6922  cc 10270  0cc0 10272  1c1 10273   / cdiv 11032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033
This theorem is referenced by:  recgt0  11221  expmulz  13224  rlimdiv  14784  rlimno1  14792  isumdivc  14900  fsumdivc  14922  geolim  15005  georeclim  15007  clim2div  15024  prodfdiv  15031  dvmptdivc  24165  dvmptdiv  24174  dvexp3  24178  logtayl  24843  dvcncxp1  24924  cxpeq  24938  logbrec  24960  ang180lem1  24987  ang180lem2  24988  ang180lem3  24989  isosctrlem2  24997  dvatan  25113  efrlim  25148  amgm  25169  lgamgulmlem2  25208  lgamgulmlem3  25209  igamf  25229  igamcl  25230  lgam1  25242  dchrinvcl  25430  dchrabs  25437  2lgslem3c  25575  dchrmusumlem  25663  vmalogdivsum2  25679  pntrlog2bndlem2  25719  pntrlog2bndlem6  25724  nmlno0lem  28220  nmlnop0iALT  29426  branmfn  29536  leopmul  29565  logdivsqrle  31330  dvtan  34087  dvasin  34123  areacirclem1  34127  areacirclem4  34130  exp11d  38171  pell14qrdich  38397  mpaaeu  38683  areaquad  38764  hashnzfzclim  39481  binomcxplemnotnn0  39515  oddfl  40403  climrec  40747  climdivf  40756  reclimc  40797  divlimc  40800  ioodvbdlimc1lem2  41079  ioodvbdlimc2lem  41081  stoweidlem7  41155  stoweidlem37  41185  wallispilem4  41216  wallispi  41218  wallispi2lem1  41219  stirlinglem1  41222  stirlinglem3  41224  stirlinglem4  41225  stirlinglem5  41226  stirlinglem7  41228  stirlinglem10  41231  stirlinglem11  41232  stirlinglem12  41233  stirlinglem15  41236  dirkertrigeq  41249  fourierdlem30  41285  fourierdlem83  41337  fourierdlem95  41349  eenglngeehlnmlem1  43477  eenglngeehlnmlem2  43478  seccl  43603  csccl  43604  young2d  43661
  Copyright terms: Public domain W3C validator