Theorem halfcld 12075

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 12055	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈ ℂ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2110  (class class class)co 7213  ℂcc 10727   / cdiv 11489  2c2 11885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-po 5468  df-so 5469  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-2 11893

This theorem is referenced by:  xp1d2m1eqxm1d2  12084  zeo  12263  zesq  13793  faclbnd2  13857  crre  14677  ef4p  15674  cosf  15686  efi4p  15698  sinhval  15715  addsin  15731  zob  15920  nn0ob  15945  flodddiv4t2lthalf  15977  4sqlem10  16500  lhop1lem  24910  chordthmlem  25715  chordthmlem2  25716  chordthmlem3  25717  chordthmlem4  25718  chordthmlem5  25719  dcubic2  25727  dcubic1  25728  dcubic  25729  mcubic  25730  cubic  25732  dquartlem1  25734  dquart  25736  quart1cl  25737  quart1lem  25738  quart1  25739  quartlem3  25742  quartlem4  25743  quart  25744  lgsquad2lem2  26266  lgsquad2  26267  logdivsum  26414  mulog2sumlem2  26416  mulog2sumlem3  26417  vmalogdivsum2  26419  selberg34r  26452  pntlemr  26483  lt2addrd  30794  logdivsqrle  32342  sin2h  35504  cos2h  35505  tan2h  35506  itg2addnclem  35565  lcmineqlem23  39793  aks4d1p1p2  39811  oddfl  42488  suplesup  42551  coseq0  43080  sinaover2ne0  43084  wallispilem4  43284  wallispi  43286  stirlinglem1  43290  stirlinglem4  43293  stirlinglem7  43296  stirlinglem15  43304  dirker2re  43308  dirkerdenne0  43309  dirkerper  43312  dirkertrigeqlem2  43315  dirkertrigeqlem3  43316  dirkeritg  43318  dirkercncflem1  43319  dirkercncflem2  43320  dirkercncflem4  43322  fourierdlem43  43366  fourierdlem44  43367  fourierdlem56  43378  fourierdlem58  43380  fourierdlem62  43384  fourierdlem68  43390  fourierdlem72  43394  fourierdlem76  43398  fourierdlem79  43401  fourierdlem80  43402  fourierdlem103  43425  fourierdlem104  43426  fourierdlem112  43434  dignn0flhalflem1  45634