Theorem reccld 11690

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 11586	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℂ)
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (1 / 𝐴) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941  (class class class)co 7260  ℂcc 10816  0cc0 10818  1c1 10819   / cdiv 11578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-resscn 10875  ax-1cn 10876  ax-icn 10877  ax-addcl 10878  ax-addrcl 10879  ax-mulcl 10880  ax-mulrcl 10881  ax-mulcom 10882  ax-addass 10883  ax-mulass 10884  ax-distr 10885  ax-i2m1 10886  ax-1ne0 10887  ax-1rid 10888  ax-rnegex 10889  ax-rrecex 10890  ax-cnre 10891  ax-pre-lttri 10892  ax-pre-lttrn 10893  ax-pre-ltadd 10894  ax-pre-mulgt0 10895

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-po 5499  df-so 5500  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-riota 7217  df-ov 7263  df-oprab 7264  df-mpo 7265  df-er 8461  df-en 8697  df-dom 8698  df-sdom 8699  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962  df-sub 11153  df-neg 11154  df-div 11579

This theorem is referenced by:  recgt0  11767  expmulz  13773  rlimdiv  15301  rlimno1  15309  isumdivc  15420  fsumdivc  15442  geolim  15526  georeclim  15528  clim2div  15545  prodfdiv  15552  dvmptdivc  25072  dvmptdiv  25081  dvexp3  25085  logtayl  25758  dvcncxp1  25839  cxpeq  25853  logbrec  25875  ang180lem1  25902  ang180lem2  25903  ang180lem3  25904  isosctrlem2  25912  dvatan  26028  efrlim  26062  amgm  26083  lgamgulmlem2  26122  lgamgulmlem3  26123  igamf  26143  igamcl  26144  lgam1  26156  dchrinvcl  26344  dchrabs  26351  2lgslem3c  26489  dchrmusumlem  26613  vmalogdivsum2  26629  pntrlog2bndlem2  26669  pntrlog2bndlem6  26674  nmlno0lem  29096  nmlnop0iALT  30298  branmfn  30408  leopmul  30437  logdivsqrle  32572  dvtan  35796  dvasin  35830  areacirclem1  35834  areacirclem4  35837  lcmineqlem5  40011  lcmineqlem6  40012  lcmineqlem12  40018  aks4d1p1p7  40052  pell14qrdich  40649  mpaaeu  40933  areaquad  41005  hashnzfzclim  41871  binomcxplemnotnn0  41905  oddfl  42747  climrec  43076  climdivf  43085  reclimc  43126  divlimc  43129  ioodvbdlimc1lem2  43405  ioodvbdlimc2lem  43407  stoweidlem7  43480  stoweidlem37  43510  wallispilem4  43541  wallispi  43543  wallispi2lem1  43544  stirlinglem1  43547  stirlinglem3  43549  stirlinglem4  43550  stirlinglem5  43551  stirlinglem7  43553  stirlinglem10  43556  stirlinglem11  43557  stirlinglem12  43558  stirlinglem15  43561  dirkertrigeq  43574  fourierdlem30  43610  fourierdlem83  43662  fourierdlem95  43674  eenglngeehlnmlem1  46013  eenglngeehlnmlem2  46014  seccl  46382  csccl  46383  young2d  46439