Theorem reccld 11980

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

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		reccld.2	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
3		reccl 11875	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℂ)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (1 / 𝐴) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964  (class class class)co 7408  ℂcc 11094  0cc0 11096  1c1 11097   / cdiv 11867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-div 11868

This theorem is referenced by:  recgt0  12057  expmulz  14140  rlimdiv  15693  rlimno1  15701  isumdivc  15811  fsumdivc  15833  geolim  15920  georeclim  15922  clim2div  15939  prodfdiv  15946  divcn  24992  dvmptdivc  26089  dvmptdiv  26098  dvexp3  26102  logtayl  26787  dvcncxp1  26870  cxpeq  26884  logbrec  26909  ang180lem1  26936  ang180lem2  26937  ang180lem3  26938  isosctrlem2  26946  dvatan  27062  efrlim  27096  amgm  27117  lgamgulmlem2  27156  lgamgulmlem3  27157  igamf  27177  igamcl  27178  lgam1  27190  dchrinvcl  27379  dchrabs  27386  2lgslem3c  27524  dchrmusumlem  27648  vmalogdivsum2  27664  pntrlog2bndlem2  27704  pntrlog2bndlem6  27709  nmlno0lem  31082  nmlnop0iALT  32284  branmfn  32394  leopmul  32423  arginv  33029  constrinvcl  34104  cos9thpiminplylem2  34114  cos9thpiminply  34119  cos9thpinconstrlem2  34121  cos9thpinconstr  34122  logdivsqrle  34978  dvtan  38204  dvasin  38238  areacirclem1  38242  areacirclem4  38245  lcmineqlem5  42685  lcmineqlem6  42686  lcmineqlem12  42692  aks4d1p1p7  42726  readvrec2  43005  readvrec  43006  pell14qrdich  43481  mpaaeu  43762  areaquad  43828  hashnzfzclim  44917  binomcxplemnotnn0  44951  oddfl  45882  climrec  46204  climdivf  46213  reclimc  46252  divlimc  46255  ioodvbdlimc1lem2  46531  ioodvbdlimc2lem  46533  stoweidlem7  46606  stoweidlem37  46636  wallispilem4  46667  wallispi  46669  wallispi2lem1  46670  stirlinglem1  46673  stirlinglem3  46675  stirlinglem4  46676  stirlinglem5  46677  stirlinglem7  46679  stirlinglem10  46682  stirlinglem11  46683  stirlinglem12  46684  stirlinglem15  46687  dirkertrigeq  46700  fourierdlem30  46736  fourierdlem83  46788  fourierdlem95  46800  ppivalnnnprmge6  48260  eenglngeehlnmlem1  49395  eenglngeehlnmlem2  49396  seccl  50406  csccl  50407  young2d  50461