Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > coscld | Structured version Visualization version GIF version |
Description: Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
Ref | Expression |
---|---|
sincld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
coscld | ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sincld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | coscl 15927 | . 2 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ‘cfv 6473 ℂcc 10962 cosccos 15865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5226 ax-sep 5240 ax-nul 5247 ax-pow 5305 ax-pr 5369 ax-un 7642 ax-inf2 9490 ax-cnex 11020 ax-resscn 11021 ax-1cn 11022 ax-icn 11023 ax-addcl 11024 ax-addrcl 11025 ax-mulcl 11026 ax-mulrcl 11027 ax-mulcom 11028 ax-addass 11029 ax-mulass 11030 ax-distr 11031 ax-i2m1 11032 ax-1ne0 11033 ax-1rid 11034 ax-rnegex 11035 ax-rrecex 11036 ax-cnre 11037 ax-pre-lttri 11038 ax-pre-lttrn 11039 ax-pre-ltadd 11040 ax-pre-mulgt0 11041 ax-pre-sup 11042 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3727 df-csb 3843 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3916 df-nul 4269 df-if 4473 df-pw 4548 df-sn 4573 df-pr 4575 df-op 4579 df-uni 4852 df-int 4894 df-iun 4940 df-br 5090 df-opab 5152 df-mpt 5173 df-tr 5207 df-id 5512 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5569 df-se 5570 df-we 5571 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6232 df-ord 6299 df-on 6300 df-lim 6301 df-suc 6302 df-iota 6425 df-fun 6475 df-fn 6476 df-f 6477 df-f1 6478 df-fo 6479 df-f1o 6480 df-fv 6481 df-isom 6482 df-riota 7286 df-ov 7332 df-oprab 7333 df-mpo 7334 df-om 7773 df-1st 7891 df-2nd 7892 df-frecs 8159 df-wrecs 8190 df-recs 8264 df-rdg 8303 df-1o 8359 df-er 8561 df-pm 8681 df-en 8797 df-dom 8798 df-sdom 8799 df-fin 8800 df-sup 9291 df-inf 9292 df-oi 9359 df-card 9788 df-pnf 11104 df-mnf 11105 df-xr 11106 df-ltxr 11107 df-le 11108 df-sub 11300 df-neg 11301 df-div 11726 df-nn 12067 df-2 12129 df-3 12130 df-n0 12327 df-z 12413 df-uz 12676 df-rp 12824 df-ico 13178 df-fz 13333 df-fzo 13476 df-fl 13605 df-seq 13815 df-exp 13876 df-fac 14081 df-hash 14138 df-shft 14869 df-cj 14901 df-re 14902 df-im 14903 df-sqrt 15037 df-abs 15038 df-limsup 15271 df-clim 15288 df-rlim 15289 df-sum 15489 df-ef 15868 df-cos 15871 |
This theorem is referenced by: tanadd 15967 addsin 15970 sincossq 15976 pilem2 25709 ptolemy 25751 efif1olem4 25799 ssscongptld 26070 chordthmlem 26080 heron 26086 cos2h 35866 tan2h 35867 dvtan 35925 sinmulcos 43731 dvsinax 43779 dvasinbx 43786 itgsin0pilem1 43816 itgsinexplem1 43820 itgcoscmulx 43835 itgsincmulx 43840 dirkertrigeqlem1 43964 dirkertrigeqlem2 43965 dirkertrigeqlem3 43966 dirkeritg 43968 dirkercncflem2 43970 fourierdlem39 44012 fourierdlem56 44028 fourierdlem57 44029 fourierdlem58 44030 fourierdlem62 44034 fourierdlem68 44040 fourierdlem73 44045 fouriersw 44097 |
Copyright terms: Public domain | W3C validator |