Step |
Hyp |
Ref |
Expression |
1 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
2 |
|
cosf |
⊢ cos : ℂ ⟶ ℂ |
3 |
|
ssid |
⊢ ℂ ⊆ ℂ |
4 |
|
nfcv |
⊢ Ⅎ 𝑥 ℝ |
5 |
|
nfrab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } |
6 |
4 5
|
dfss2f |
⊢ ( ℝ ⊆ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } ↔ ∀ 𝑥 ( 𝑥 ∈ ℝ → 𝑥 ∈ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } ) ) |
7 |
|
recn |
⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ ) |
8 |
7
|
sincld |
⊢ ( 𝑥 ∈ ℝ → ( sin ‘ 𝑥 ) ∈ ℂ ) |
9 |
8
|
negcld |
⊢ ( 𝑥 ∈ ℝ → - ( sin ‘ 𝑥 ) ∈ ℂ ) |
10 |
|
elex |
⊢ ( - ( sin ‘ 𝑥 ) ∈ ℂ → - ( sin ‘ 𝑥 ) ∈ V ) |
11 |
9 10
|
syl |
⊢ ( 𝑥 ∈ ℝ → - ( sin ‘ 𝑥 ) ∈ V ) |
12 |
|
rabid |
⊢ ( 𝑥 ∈ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } ↔ ( 𝑥 ∈ ℂ ∧ - ( sin ‘ 𝑥 ) ∈ V ) ) |
13 |
7 11 12
|
sylanbrc |
⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } ) |
14 |
6 13
|
mpgbir |
⊢ ℝ ⊆ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } |
15 |
|
dvcos |
⊢ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) |
16 |
15
|
dmmpt |
⊢ dom ( ℂ D cos ) = { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } |
17 |
14 16
|
sseqtrri |
⊢ ℝ ⊆ dom ( ℂ D cos ) |
18 |
|
dvres3 |
⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ cos : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D cos ) ) ) → ( ℝ D ( cos ↾ ℝ ) ) = ( ( ℂ D cos ) ↾ ℝ ) ) |
19 |
1 2 3 17 18
|
mp4an |
⊢ ( ℝ D ( cos ↾ ℝ ) ) = ( ( ℂ D cos ) ↾ ℝ ) |
20 |
|
ffn |
⊢ ( cos : ℂ ⟶ ℂ → cos Fn ℂ ) |
21 |
2 20
|
ax-mp |
⊢ cos Fn ℂ |
22 |
|
dffn5 |
⊢ ( cos Fn ℂ ↔ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ) |
23 |
21 22
|
mpbi |
⊢ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) |
24 |
23
|
reseq1i |
⊢ ( cos ↾ ℝ ) = ( ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ↾ ℝ ) |
25 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
26 |
|
resmpt |
⊢ ( ℝ ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) ) |
27 |
25 26
|
ax-mp |
⊢ ( ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) |
28 |
24 27
|
eqtri |
⊢ ( cos ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) |
29 |
28
|
oveq2i |
⊢ ( ℝ D ( cos ↾ ℝ ) ) = ( ℝ D ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) ) |
30 |
15
|
reseq1i |
⊢ ( ( ℂ D cos ) ↾ ℝ ) = ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ↾ ℝ ) |
31 |
|
resmpt |
⊢ ( ℝ ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) ) ) |
32 |
25 31
|
ax-mp |
⊢ ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) ) |
33 |
30 32
|
eqtri |
⊢ ( ( ℂ D cos ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) ) |
34 |
19 29 33
|
3eqtr3i |
⊢ ( ℝ D ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) ) |