Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > resincld | Structured version Visualization version GIF version |
Description: Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
Ref | Expression |
---|---|
resincld.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
Ref | Expression |
---|---|
resincld | ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resincld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | resincl 15830 | . 2 ⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2109 ‘cfv 6430 ℝcr 10854 sincsin 15754 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-rep 5213 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7579 ax-inf2 9360 ax-cnex 10911 ax-resscn 10912 ax-1cn 10913 ax-icn 10914 ax-addcl 10915 ax-addrcl 10916 ax-mulcl 10917 ax-mulrcl 10918 ax-mulcom 10919 ax-addass 10920 ax-mulass 10921 ax-distr 10922 ax-i2m1 10923 ax-1ne0 10924 ax-1rid 10925 ax-rnegex 10926 ax-rrecex 10927 ax-cnre 10928 ax-pre-lttri 10929 ax-pre-lttrn 10930 ax-pre-ltadd 10931 ax-pre-mulgt0 10932 ax-pre-sup 10933 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3072 df-rmo 3073 df-rab 3074 df-v 3432 df-sbc 3720 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4845 df-int 4885 df-iun 4931 df-br 5079 df-opab 5141 df-mpt 5162 df-tr 5196 df-id 5488 df-eprel 5494 df-po 5502 df-so 5503 df-fr 5543 df-se 5544 df-we 5545 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-res 5600 df-ima 5601 df-pred 6199 df-ord 6266 df-on 6267 df-lim 6268 df-suc 6269 df-iota 6388 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435 df-fo 6436 df-f1o 6437 df-fv 6438 df-isom 6439 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-om 7701 df-1st 7817 df-2nd 7818 df-frecs 8081 df-wrecs 8112 df-recs 8186 df-rdg 8225 df-1o 8281 df-er 8472 df-pm 8592 df-en 8708 df-dom 8709 df-sdom 8710 df-fin 8711 df-sup 9162 df-inf 9163 df-oi 9230 df-card 9681 df-pnf 10995 df-mnf 10996 df-xr 10997 df-ltxr 10998 df-le 10999 df-sub 11190 df-neg 11191 df-div 11616 df-nn 11957 df-2 12019 df-3 12020 df-n0 12217 df-z 12303 df-uz 12565 df-rp 12713 df-ico 13067 df-fz 13222 df-fzo 13365 df-fl 13493 df-seq 13703 df-exp 13764 df-fac 13969 df-hash 14026 df-shft 14759 df-cj 14791 df-re 14792 df-im 14793 df-sqrt 14927 df-abs 14928 df-limsup 15161 df-clim 15178 df-rlim 15179 df-sum 15379 df-ef 15758 df-sin 15760 |
This theorem is referenced by: sin01bnd 15875 sinltx 15879 sin01gt0 15880 pilem3 25593 sincosq2sgn 25637 sincosq3sgn 25638 sincosq4sgn 25639 tanrpcl 25642 tangtx 25643 sinq12ge0 25646 sinq34lt0t 25647 sineq0 25661 cosordlem 25667 tanord1 25674 argimgt0 25748 logf1o2 25786 cxpsqrtlem 25838 heron 25969 asinsinlem 26022 basellem3 26213 basellem4 26214 basellem8 26218 sinccvglem 33609 circum 33611 sin2h 35746 wallispilem1 43560 dirker2re 43587 dirkercncflem2 43599 dirkercncflem4 43601 fourierdlem5 43607 fourierdlem21 43623 fourierdlem22 43624 fourierdlem39 43641 fourierdlem43 43645 fourierdlem56 43657 fourierdlem57 43658 fourierdlem58 43659 fourierdlem62 43663 fourierdlem66 43667 fourierdlem68 43669 fourierdlem72 43673 fourierdlem76 43677 fourierdlem78 43679 fourierdlem83 43684 fourierdlem87 43688 fourierdlem103 43704 fourierdlem104 43705 fourierdlem112 43713 sqwvfourb 43724 |
Copyright terms: Public domain | W3C validator |