Theorem coscld 15480

Description: Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)

Hypothesis

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

Assertion

Ref	Expression
coscld	⊢ (𝜑 → (cos‘𝐴) ∈ ℂ)

Proof of Theorem coscld

Step	Hyp	Ref	Expression
1		sincld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		coscl 15476	. 2 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6352  ℂcc 10532  cosccos 15414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5327  ax-un 7458  ax-inf2 9101  ax-cnex 10590  ax-resscn 10591  ax-1cn 10592  ax-icn 10593  ax-addcl 10594  ax-addrcl 10595  ax-mulcl 10596  ax-mulrcl 10597  ax-mulcom 10598  ax-addass 10599  ax-mulass 10600  ax-distr 10601  ax-i2m1 10602  ax-1ne0 10603  ax-1rid 10604  ax-rnegex 10605  ax-rrecex 10606  ax-cnre 10607  ax-pre-lttri 10608  ax-pre-lttrn 10609  ax-pre-ltadd 10610  ax-pre-mulgt0 10611  ax-pre-sup 10612  ax-addf 10613  ax-mulf 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-fal 1549  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-nel 3123  df-ral 3142  df-rex 3143  df-reu 3144  df-rmo 3145  df-rab 3146  df-v 3495  df-sbc 3771  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4465  df-pw 4538  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4836  df-int 4874  df-iun 4918  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5457  df-eprel 5462  df-po 5471  df-so 5472  df-fr 5511  df-se 5512  df-we 5513  df-xp 5558  df-rel 5559  df-cnv 5560  df-co 5561  df-dm 5562  df-rn 5563  df-res 5564  df-ima 5565  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-isom 6361  df-riota 7111  df-ov 7156  df-oprab 7157  df-mpo 7158  df-om 7578  df-1st 7686  df-2nd 7687  df-wrecs 7944  df-recs 8005  df-rdg 8043  df-1o 8099  df-oadd 8103  df-er 8286  df-pm 8406  df-en 8507  df-dom 8508  df-sdom 8509  df-fin 8510  df-sup 8903  df-inf 8904  df-oi 8971  df-card 9365  df-pnf 10674  df-mnf 10675  df-xr 10676  df-ltxr 10677  df-le 10678  df-sub 10869  df-neg 10870  df-div 11295  df-nn 11636  df-2 11698  df-3 11699  df-n0 11896  df-z 11980  df-uz 12242  df-rp 12388  df-ico 12742  df-fz 12891  df-fzo 13032  df-fl 13160  df-seq 13368  df-exp 13428  df-fac 13632  df-hash 13689  df-shft 14422  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-limsup 14824  df-clim 14841  df-rlim 14842  df-sum 15039  df-ef 15417  df-cos 15420

This theorem is referenced by:  tanadd  15516  addsin  15519  sincossq  15525  pilem2  25038  ptolemy  25080  efif1olem4  25127  ssscongptld  25398  chordthmlem  25408  heron  25414  cos2h  34921  tan2h  34922  dvtan  34980  sinmulcos  42220  dvsinax  42271  dvasinbx  42279  itgsin0pilem1  42309  itgsinexplem1  42313  itgcoscmulx  42328  itgsincmulx  42333  dirkertrigeqlem1  42457  dirkertrigeqlem2  42458  dirkertrigeqlem3  42459  dirkeritg  42461  dirkercncflem2  42463  fourierdlem39  42505  fourierdlem56  42521  fourierdlem57  42522  fourierdlem58  42523  fourierdlem62  42527  fourierdlem68  42533  fourierdlem73  42538  fouriersw  42590