sincn - Metamath Proof Explorer

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

Theorem sincn 26424

Description: Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)

**Assertion**
Ref	Expression
sincn	⊢ sin ∈ (ℂ–cn→ℂ)

Proof of Theorem sincn Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sin 16087	. 2 ⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
2		eqid 2734	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
3	2	subcn 24824	. . . . . . . . 9 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
4	3	a1i 11	. . . . . . . 8 ⊢ (⊤ → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
5		efcn 26423	. . . . . . . . . 10 ⊢ exp ∈ (ℂ–cn→ℂ)
6	5	a1i 11	. . . . . . . . 9 ⊢ (⊤ → exp ∈ (ℂ–cn→ℂ))
7		ax-icn 11196	. . . . . . . . . 10 ⊢ i ∈ ℂ
8		eqid 2734	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ ↦ (i · 𝑥)) = (𝑥 ∈ ℂ ↦ (i · 𝑥))
9	8	mulc1cncf 24867	. . . . . . . . . 10 ⊢ (i ∈ ℂ → (𝑥 ∈ ℂ ↦ (i · 𝑥)) ∈ (ℂ–cn→ℂ))
10	7, 9	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (i · 𝑥)) ∈ (ℂ–cn→ℂ))
11	6, 10	cncfmpt1f 24876	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (exp‘(i · 𝑥))) ∈ (ℂ–cn→ℂ))
12		negicn 11491	. . . . . . . . . 10 ⊢ -i ∈ ℂ
13		eqid 2734	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ ↦ (-i · 𝑥)) = (𝑥 ∈ ℂ ↦ (-i · 𝑥))
14	13	mulc1cncf 24867	. . . . . . . . . 10 ⊢ (-i ∈ ℂ → (𝑥 ∈ ℂ ↦ (-i · 𝑥)) ∈ (ℂ–cn→ℂ))
15	12, 14	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (-i · 𝑥)) ∈ (ℂ–cn→ℂ))
16	6, 15	cncfmpt1f 24876	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (exp‘(-i · 𝑥))) ∈ (ℂ–cn→ℂ))
17	2, 4, 11, 16	cncfmpt2f 24877	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥)))) ∈ (ℂ–cn→ℂ))
18		cncff 24855	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥)))) ∈ (ℂ–cn→ℂ) → (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥)))):ℂ⟶ℂ)
19	17, 18	syl 17	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥)))):ℂ⟶ℂ)
20		eqid 2734	. . . . . . 7 ⊢ (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))))
21	20	fmpt 7110	. . . . . 6 ⊢ (∀𝑥 ∈ ℂ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) ∈ ℂ ↔ (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥)))):ℂ⟶ℂ)
22	19, 21	sylibr 234	. . . . 5 ⊢ (⊤ → ∀𝑥 ∈ ℂ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) ∈ ℂ)
23		eqidd 2735	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥)))))
24		eqidd 2735	. . . . 5 ⊢ (⊤ → (𝑦 ∈ ℂ ↦ (𝑦 / (2 · i))) = (𝑦 ∈ ℂ ↦ (𝑦 / (2 · i))))
25		oveq1 7420	. . . . 5 ⊢ (𝑦 = ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) → (𝑦 / (2 · i)) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
26	22, 23, 24, 25	fmptcof 7130	. . . 4 ⊢ (⊤ → ((𝑦 ∈ ℂ ↦ (𝑦 / (2 · i))) ∘ (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))))) = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i))))
27		2mulicn 12473	. . . . . . 7 ⊢ (2 · i) ∈ ℂ
28		2muline0 12474	. . . . . . 7 ⊢ (2 · i) ≠ 0
29		eqid 2734	. . . . . . . 8 ⊢ (𝑦 ∈ ℂ ↦ (𝑦 / (2 · i))) = (𝑦 ∈ ℂ ↦ (𝑦 / (2 · i)))
30	29	divccncf 24868	. . . . . . 7 ⊢ (((2 · i) ∈ ℂ ∧ (2 · i) ≠ 0) → (𝑦 ∈ ℂ ↦ (𝑦 / (2 · i))) ∈ (ℂ–cn→ℂ))
31	27, 28, 30	mp2an 692	. . . . . 6 ⊢ (𝑦 ∈ ℂ ↦ (𝑦 / (2 · i))) ∈ (ℂ–cn→ℂ)
32	31	a1i 11	. . . . 5 ⊢ (⊤ → (𝑦 ∈ ℂ ↦ (𝑦 / (2 · i))) ∈ (ℂ–cn→ℂ))
33	17, 32	cncfco 24869	. . . 4 ⊢ (⊤ → ((𝑦 ∈ ℂ ↦ (𝑦 / (2 · i))) ∘ (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))))) ∈ (ℂ–cn→ℂ))
34	26, 33	eqeltrrd 2834	. . 3 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i))) ∈ (ℂ–cn→ℂ))
35	34	mptru 1546	. 2 ⊢ (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i))) ∈ (ℂ–cn→ℂ)
36	1, 35	eqeltri 2829	1 ⊢ sin ∈ (ℂ–cn→ℂ)

Colors of variables: wff setvar class

Syntax hints: ⊤wtru 1540 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 ↦ cmpt 5205 ∘ ccom 5669 ⟶wf 6537 ‘cfv 6541 (class class class)co 7413 ℂcc 11135 0cc0 11137 ici 11139 · cmul 11142 − cmin 11474 -cneg 11475 / cdiv 11902 2c2 12303 expce 16079 sincsin 16081 TopOpenctopn 17437 ℂ_fldccnfld 21326 Cn ccn 23178 ×_t ctx 23514 –cn→ccncf 24838

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-inf2 9663 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215 ax-addf 11216

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-om 7870 df-1st 7996 df-2nd 7997 df-supp 8168 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-er 8727 df-map 8850 df-pm 8851 df-ixp 8920 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-fsupp 9384 df-fi 9433 df-sup 9464 df-inf 9465 df-oi 9532 df-card 9961 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-z 12597 df-dec 12717 df-uz 12861 df-q 12973 df-rp 13017 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-ico 13375 df-icc 13376 df-fz 13530 df-fzo 13677 df-fl 13814 df-seq 14025 df-exp 14085 df-fac 14295 df-bc 14324 df-hash 14352 df-shft 15088 df-cj 15120 df-re 15121 df-im 15122 df-sqrt 15256 df-abs 15257 df-limsup 15489 df-clim 15506 df-rlim 15507 df-sum 15705 df-ef 16085 df-sin 16087 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17230 df-ress 17253 df-plusg 17286 df-mulr 17287 df-starv 17288 df-sca 17289 df-vsca 17290 df-ip 17291 df-tset 17292 df-ple 17293 df-ds 17295 df-unif 17296 df-hom 17297 df-cco 17298 df-rest 17438 df-topn 17439 df-0g 17457 df-gsum 17458 df-topgen 17459 df-pt 17460 df-prds 17463 df-xrs 17518 df-qtop 17523 df-imas 17524 df-xps 17526 df-mre 17600 df-mrc 17601 df-acs 17603 df-mgm 18622 df-sgrp 18701 df-mnd 18717 df-submnd 18766 df-mulg 19055 df-cntz 19304 df-cmn 19768 df-psmet 21318 df-xmet 21319 df-met 21320 df-bl 21321 df-mopn 21322 df-fbas 21323 df-fg 21324 df-cnfld 21327 df-top 22848 df-topon 22865 df-topsp 22887 df-bases 22900 df-cld 22973 df-ntr 22974 df-cls 22975 df-nei 23052 df-lp 23090 df-perf 23091 df-cn 23181 df-cnp 23182 df-haus 23269 df-tx 23516 df-hmeo 23709 df-fil 23800 df-fm 23892 df-flim 23893 df-flf 23894 df-xms 24275 df-ms 24276 df-tms 24277 df-cncf 24840 df-limc 25837 df-dv 25838

This theorem is referenced by: pilem3 26433 resuppsinopn 42356 resincncf 45847 itgsin0pilem1 45922 ibliccsinexp 45923 itgsinexplem1 45926 itgsinexp 45927 itgcoscmulx 45941 itgsincmulx 45946 dirkeritg 46074 dirkercncflem2 46076 dirkercncflem4 46078 fourierdlem21 46100 fourierdlem22 46101 fourierdlem39 46118 fourierdlem62 46140 fourierdlem68 46146 fourierdlem73 46151 fourierdlem76 46154 fourierdlem78 46156 fourierdlem83 46161 sqwvfourb 46201

W3C validator