MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sincld Structured version   Visualization version   Unicode version

Theorem sincld 14195
Description: Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
Hypothesis
Ref Expression
sincld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
sincld  |-  ( ph  ->  ( sin `  A
)  e.  CC )

Proof of Theorem sincld
StepHypRef Expression
1 sincld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 sincl 14191 . 2  |-  ( A  e.  CC  ->  ( sin `  A )  e.  CC )
31, 2syl 17 1  |-  ( ph  ->  ( sin `  A
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1891   ` cfv 5561   CCcc 9524   sincsin 14127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-inf2 8133  ax-cnex 9582  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602  ax-pre-mulgt0 9603  ax-pre-sup 9604  ax-addf 9605  ax-mulf 9606
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-fal 1454  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-int 4205  df-iun 4250  df-br 4375  df-opab 4434  df-mpt 4435  df-tr 4470  df-eprel 4723  df-id 4727  df-po 4733  df-so 4734  df-fr 4771  df-se 4772  df-we 4773  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-pred 5359  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-isom 5570  df-riota 6238  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-om 6681  df-1st 6781  df-2nd 6782  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-oadd 7173  df-er 7350  df-pm 7462  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-sup 7943  df-inf 7944  df-oi 8012  df-card 8360  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668  df-sub 9849  df-neg 9850  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-n0 10860  df-z 10928  df-uz 11150  df-rp 11293  df-ico 11631  df-fz 11776  df-fzo 11909  df-fl 12022  df-seq 12208  df-exp 12267  df-fac 12454  df-hash 12510  df-shft 13141  df-cj 13173  df-re 13174  df-im 13175  df-sqrt 13309  df-abs 13310  df-limsup 13537  df-clim 13563  df-rlim 13564  df-sum 13764  df-ef 14132  df-sin 14134
This theorem is referenced by:  retanhcl  14224  tanhlt1  14225  tanadd  14232  addsin  14235  sincossq  14241  sinkpi  23486  coseq1  23489  efif1olem4  23506  heron  23776  sin2h  31937  dvtan  31994  sineq0ALT  37331  sinmulcos  37782  dvcosre  37823  dvasinbx  37834  dvcosax  37840  itgsin0pilem1  37868  ibliccsinexp  37869  iblioosinexp  37871  itgsinexplem1  37872  itgsinexp  37873  itgcoscmulx  37888  itgsincmulx  37893  wallispilem2  37985  dirker2re  38011  dirkerdenne0  38012  dirkerper  38015  dirkertrigeqlem2  38018  dirkertrigeqlem3  38019  dirkeritg  38021  dirkercncflem2  38023  dirkercncflem4  38025  fourierdlem39  38066  fourierdlem43  38071  fourierdlem44  38072  fourierdlem56  38083  fourierdlem57  38084  fourierdlem58  38085  fourierdlem62  38089  fourierdlem68  38095  fourierdlem72  38099  fourierdlem73  38100  fourierdlem76  38103  fourierdlem80  38107  fourierdlem103  38130  fourierdlem104  38131  sqwvfoura  38149  sqwvfourb  38150  fouriersw  38152  sinh-conventional  40784
  Copyright terms: Public domain W3C validator