Theorem halfcld 12323

Description: Closure of half of a number (frequently used special case). (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
2timesd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
halfcld	⊢ (𝜑 → (𝐴 / 2) ∈ ℂ)

Proof of Theorem halfcld

Step	Hyp	Ref	Expression
1		2timesd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		halfcl 12303	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈ ℂ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7341  ℂcc 10974   / cdiv 11737  2c2 12133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-resscn 11033  ax-1cn 11034  ax-icn 11035  ax-addcl 11036  ax-addrcl 11037  ax-mulcl 11038  ax-mulrcl 11039  ax-mulcom 11040  ax-addass 11041  ax-mulass 11042  ax-distr 11043  ax-i2m1 11044  ax-1ne0 11045  ax-1rid 11046  ax-rnegex 11047  ax-rrecex 11048  ax-cnre 11049  ax-pre-lttri 11050  ax-pre-lttrn 11051  ax-pre-ltadd 11052  ax-pre-mulgt0 11053

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  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 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-opab 5159  df-mpt 5180  df-id 5522  df-po 5536  df-so 5537  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-riota 7297  df-ov 7344  df-oprab 7345  df-mpo 7346  df-er 8573  df-en 8809  df-dom 8810  df-sdom 8811  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120  df-sub 11312  df-neg 11313  df-div 11738  df-2 12141

This theorem is referenced by:  xp1d2m1eqxm1d2  12332  zeo  12511  zesq  14046  faclbnd2  14110  crre  14924  ef4p  15921  cosf  15933  efi4p  15945  sinhval  15962  addsin  15978  zob  16167  nn0ob  16192  flodddiv4t2lthalf  16224  4sqlem10  16745  lhop1lem  25282  chordthmlem  26087  chordthmlem2  26088  chordthmlem3  26089  chordthmlem4  26090  chordthmlem5  26091  dcubic2  26099  dcubic1  26100  dcubic  26101  mcubic  26102  cubic  26104  dquartlem1  26106  dquart  26108  quart1cl  26109  quart1lem  26110  quart1  26111  quartlem3  26114  quartlem4  26115  quart  26116  lgsquad2lem2  26638  lgsquad2  26639  logdivsum  26786  mulog2sumlem2  26788  mulog2sumlem3  26789  vmalogdivsum2  26791  selberg34r  26824  pntlemr  26855  lt2addrd  31359  logdivsqrle  32928  sin2h  35923  cos2h  35924  tan2h  35925  itg2addnclem  35984  lcmineqlem23  40364  aks4d1p1p2  40383  oddfl  43203  suplesup  43265  coseq0  43793  sinaover2ne0  43797  wallispilem4  43997  wallispi  43999  stirlinglem1  44003  stirlinglem4  44006  stirlinglem7  44009  stirlinglem15  44017  dirker2re  44021  dirkerdenne0  44022  dirkerper  44025  dirkertrigeqlem2  44028  dirkertrigeqlem3  44029  dirkeritg  44031  dirkercncflem1  44032  dirkercncflem2  44033  dirkercncflem4  44035  fourierdlem43  44079  fourierdlem44  44080  fourierdlem56  44091  fourierdlem58  44093  fourierdlem62  44097  fourierdlem68  44103  fourierdlem72  44107  fourierdlem76  44111  fourierdlem79  44114  fourierdlem80  44115  fourierdlem103  44138  fourierdlem104  44139  fourierdlem112  44147  dignn0flhalflem1  46379