| Step | Hyp | Ref
| Expression |
| 1 | | df-tan 16107 |
. . . 4
⊢ tan =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) /
(cos‘𝑥))) |
| 2 | | cnvimass 6100 |
. . . . . . . . 9
⊢ (◡cos “ (ℂ ∖ {0})) ⊆
dom cos |
| 3 | | cosf 16161 |
. . . . . . . . . 10
⊢
cos:ℂ⟶ℂ |
| 4 | 3 | fdmi 6747 |
. . . . . . . . 9
⊢ dom cos =
ℂ |
| 5 | 2, 4 | sseqtri 4032 |
. . . . . . . 8
⊢ (◡cos “ (ℂ ∖ {0})) ⊆
ℂ |
| 6 | 5 | sseli 3979 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
𝑥 ∈
ℂ) |
| 7 | 6 | sincld 16166 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(sin‘𝑥) ∈
ℂ) |
| 8 | 6 | coscld 16167 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(cos‘𝑥) ∈
ℂ) |
| 9 | | ffn 6736 |
. . . . . . . 8
⊢
(cos:ℂ⟶ℂ → cos Fn ℂ) |
| 10 | | elpreima 7078 |
. . . . . . . 8
⊢ (cos Fn
ℂ → (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↔ (𝑥 ∈ ℂ
∧ (cos‘𝑥) ∈
(ℂ ∖ {0})))) |
| 11 | 3, 9, 10 | mp2b 10 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↔
(𝑥 ∈ ℂ ∧
(cos‘𝑥) ∈
(ℂ ∖ {0}))) |
| 12 | | eldifsni 4790 |
. . . . . . . 8
⊢
((cos‘𝑥)
∈ (ℂ ∖ {0}) → (cos‘𝑥) ≠ 0) |
| 13 | 12 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧
(cos‘𝑥) ∈
(ℂ ∖ {0})) → (cos‘𝑥) ≠ 0) |
| 14 | 11, 13 | sylbi 217 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(cos‘𝑥) ≠
0) |
| 15 | 7, 8, 14 | divrecd 12046 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((sin‘𝑥) /
(cos‘𝑥)) =
((sin‘𝑥) · (1
/ (cos‘𝑥)))) |
| 16 | 15 | mpteq2ia 5245 |
. . . 4
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) /
(cos‘𝑥))) = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) · (1
/ (cos‘𝑥)))) |
| 17 | 1, 16 | eqtri 2765 |
. . 3
⊢ tan =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) · (1
/ (cos‘𝑥)))) |
| 18 | 17 | oveq2i 7442 |
. 2
⊢ (ℂ
D tan) = (ℂ D (𝑥
∈ (◡cos “ (ℂ ∖
{0})) ↦ ((sin‘𝑥) · (1 / (cos‘𝑥))))) |
| 19 | | cnelprrecn 11248 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
| 20 | 19 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 21 | | difss 4136 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ⊆ ℂ |
| 22 | | imass2 6120 |
. . . . . . . . 9
⊢ ((ℂ
∖ {0}) ⊆ ℂ → (◡cos “ (ℂ ∖ {0})) ⊆
(◡cos “
ℂ)) |
| 23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ (◡cos “ (ℂ ∖ {0})) ⊆
(◡cos “ ℂ) |
| 24 | | fimacnv 6758 |
. . . . . . . . 9
⊢
(cos:ℂ⟶ℂ → (◡cos “ ℂ) =
ℂ) |
| 25 | 3, 24 | ax-mp 5 |
. . . . . . . 8
⊢ (◡cos “ ℂ) =
ℂ |
| 26 | 23, 25 | sseqtri 4032 |
. . . . . . 7
⊢ (◡cos “ (ℂ ∖ {0})) ⊆
ℂ |
| 27 | 26 | sseli 3979 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
𝑥 ∈
ℂ) |
| 28 | 27 | sincld 16166 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(sin‘𝑥) ∈
ℂ) |
| 29 | 28 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (sin‘𝑥)
∈ ℂ) |
| 30 | 8 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (cos‘𝑥)
∈ ℂ) |
| 31 | | sincl 16162 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
| 32 | 31 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (sin‘𝑥) ∈ ℂ) |
| 33 | | coscl 16163 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
(cos‘𝑥) ∈
ℂ) |
| 34 | 33 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (cos‘𝑥) ∈ ℂ) |
| 35 | | dvsin 26020 |
. . . . . 6
⊢ (ℂ
D sin) = cos |
| 36 | | sinf 16160 |
. . . . . . . . 9
⊢
sin:ℂ⟶ℂ |
| 37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ sin:ℂ⟶ℂ) |
| 38 | 37 | feqmptd 6977 |
. . . . . . 7
⊢ (⊤
→ sin = (𝑥 ∈
ℂ ↦ (sin‘𝑥))) |
| 39 | 38 | oveq2d 7447 |
. . . . . 6
⊢ (⊤
→ (ℂ D sin) = (ℂ D (𝑥 ∈ ℂ ↦ (sin‘𝑥)))) |
| 40 | 3 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ cos:ℂ⟶ℂ) |
| 41 | 40 | feqmptd 6977 |
. . . . . 6
⊢ (⊤
→ cos = (𝑥 ∈
ℂ ↦ (cos‘𝑥))) |
| 42 | 35, 39, 41 | 3eqtr3a 2801 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (sin‘𝑥))) = (𝑥 ∈ ℂ ↦ (cos‘𝑥))) |
| 43 | 26 | a1i 11 |
. . . . 5
⊢ (⊤
→ (◡cos “ (ℂ ∖
{0})) ⊆ ℂ) |
| 44 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 45 | 44 | cnfldtopon 24803 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 46 | 45 | toponrestid 22927 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 47 | | dvtanlem 37676 |
. . . . . 6
⊢ (◡cos “ (ℂ ∖ {0})) ∈
(TopOpen‘ℂfld) |
| 48 | 47 | a1i 11 |
. . . . 5
⊢ (⊤
→ (◡cos “ (ℂ ∖
{0})) ∈ (TopOpen‘ℂfld)) |
| 49 | 20, 32, 34, 42, 43, 46, 44, 48 | dvmptres 26001 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↦ (sin‘𝑥))) =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(cos‘𝑥))) |
| 50 | 8, 14 | reccld 12036 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) → (1
/ (cos‘𝑥)) ∈
ℂ) |
| 51 | 50 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (1 / (cos‘𝑥)) ∈ ℂ) |
| 52 | | ovexd 7466 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) ∈ V) |
| 53 | 11 | simprbi 496 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(cos‘𝑥) ∈
(ℂ ∖ {0})) |
| 54 | 53 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (cos‘𝑥)
∈ (ℂ ∖ {0})) |
| 55 | 29 | negcld 11607 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → -(sin‘𝑥) ∈ ℂ) |
| 56 | | eldifi 4131 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ∈
ℂ) |
| 57 | | eldifsni 4790 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ≠
0) |
| 58 | 56, 57 | reccld 12036 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ (1 / 𝑦) ∈
ℂ) |
| 59 | 58 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ {0})) → (1 / 𝑦) ∈ ℂ) |
| 60 | | negex 11506 |
. . . . . 6
⊢ -(1 /
(𝑦↑2)) ∈
V |
| 61 | 60 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ {0})) → -(1 / (𝑦↑2)) ∈ V) |
| 62 | 32 | negcld 11607 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℂ) → -(sin‘𝑥) ∈ ℂ) |
| 63 | 41 | oveq2d 7447 |
. . . . . . 7
⊢ (⊤
→ (ℂ D cos) = (ℂ D (𝑥 ∈ ℂ ↦ (cos‘𝑥)))) |
| 64 | | dvcos 26021 |
. . . . . . 7
⊢ (ℂ
D cos) = (𝑥 ∈ ℂ
↦ -(sin‘𝑥)) |
| 65 | 63, 64 | eqtr3di 2792 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (cos‘𝑥))) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥))) |
| 66 | 20, 34, 62, 65, 43, 46, 44, 48 | dvmptres 26001 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↦ (cos‘𝑥))) =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
-(sin‘𝑥))) |
| 67 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 68 | | dvrec 25993 |
. . . . . 6
⊢ (1 ∈
ℂ → (ℂ D (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 /
(𝑦↑2)))) |
| 69 | 67, 68 | mp1i 13 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 /
(𝑦↑2)))) |
| 70 | | oveq2 7439 |
. . . . 5
⊢ (𝑦 = (cos‘𝑥) → (1 / 𝑦) = (1 / (cos‘𝑥))) |
| 71 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑦 = (cos‘𝑥) → (𝑦↑2) = ((cos‘𝑥)↑2)) |
| 72 | 71 | oveq2d 7447 |
. . . . . 6
⊢ (𝑦 = (cos‘𝑥) → (1 / (𝑦↑2)) = (1 / ((cos‘𝑥)↑2))) |
| 73 | 72 | negeqd 11502 |
. . . . 5
⊢ (𝑦 = (cos‘𝑥) → -(1 / (𝑦↑2)) = -(1 / ((cos‘𝑥)↑2))) |
| 74 | 20, 20, 54, 55, 59, 61, 66, 69, 70, 73 | dvmptco 26010 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↦ (1 / (cos‘𝑥)))) = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)))) |
| 75 | 20, 29, 30, 49, 51, 52, 74 | dvmptmul 25999 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↦ ((sin‘𝑥)
· (1 / (cos‘𝑥))))) = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥))))) |
| 76 | 75 | mptru 1547 |
. 2
⊢ (ℂ
D (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) · (1
/ (cos‘𝑥))))) =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥)))) |
| 77 | | ovex 7464 |
. . . . 5
⊢
((sin‘𝑥) /
(cos‘𝑥)) ∈
V |
| 78 | 77, 1 | dmmpti 6712 |
. . . 4
⊢ dom tan =
(◡cos “ (ℂ ∖
{0})) |
| 79 | 78 | eqcomi 2746 |
. . 3
⊢ (◡cos “ (ℂ ∖ {0})) = dom
tan |
| 80 | 8 | sqcld 14184 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥)↑2)
∈ ℂ) |
| 81 | 7 | sqcld 14184 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((sin‘𝑥)↑2)
∈ ℂ) |
| 82 | | sqne0 14163 |
. . . . . . . . 9
⊢
((cos‘𝑥)
∈ ℂ → (((cos‘𝑥)↑2) ≠ 0 ↔ (cos‘𝑥) ≠ 0)) |
| 83 | 8, 82 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥)↑2)
≠ 0 ↔ (cos‘𝑥)
≠ 0)) |
| 84 | 14, 83 | mpbird 257 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥)↑2) ≠
0) |
| 85 | 80, 81, 80, 84 | divdird 12081 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((((cos‘𝑥)↑2) +
((sin‘𝑥)↑2)) /
((cos‘𝑥)↑2)) =
((((cos‘𝑥)↑2) /
((cos‘𝑥)↑2)) +
(((sin‘𝑥)↑2) /
((cos‘𝑥)↑2)))) |
| 86 | 80, 81 | addcomd 11463 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥)↑2) +
((sin‘𝑥)↑2)) =
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2))) |
| 87 | | sincossq 16212 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ →
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2)) =
1) |
| 88 | 6, 87 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2)) =
1) |
| 89 | 86, 88 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥)↑2) +
((sin‘𝑥)↑2)) =
1) |
| 90 | 89 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((((cos‘𝑥)↑2) +
((sin‘𝑥)↑2)) /
((cos‘𝑥)↑2)) =
(1 / ((cos‘𝑥)↑2))) |
| 91 | 85, 90 | eqtr3d 2779 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((((cos‘𝑥)↑2) /
((cos‘𝑥)↑2)) +
(((sin‘𝑥)↑2) /
((cos‘𝑥)↑2))) =
(1 / ((cos‘𝑥)↑2))) |
| 92 | 8, 14 | recidd 12038 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥) · (1
/ (cos‘𝑥))) =
1) |
| 93 | 80, 84 | dividd 12041 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥)↑2) /
((cos‘𝑥)↑2)) =
1) |
| 94 | 92, 93 | eqtr4d 2780 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥) · (1
/ (cos‘𝑥))) =
(((cos‘𝑥)↑2) /
((cos‘𝑥)↑2))) |
| 95 | 7, 7, 80, 84 | div23d 12080 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((sin‘𝑥) ·
(sin‘𝑥)) /
((cos‘𝑥)↑2)) =
(((sin‘𝑥) /
((cos‘𝑥)↑2))
· (sin‘𝑥))) |
| 96 | 7 | sqvald 14183 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((sin‘𝑥)↑2) =
((sin‘𝑥) ·
(sin‘𝑥))) |
| 97 | 96 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((sin‘𝑥)↑2) /
((cos‘𝑥)↑2)) =
(((sin‘𝑥) ·
(sin‘𝑥)) /
((cos‘𝑥)↑2))) |
| 98 | 80, 84 | reccld 12036 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) → (1
/ ((cos‘𝑥)↑2))
∈ ℂ) |
| 99 | 98, 7 | mul2negd 11718 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) = ((1 / ((cos‘𝑥)↑2)) ·
(sin‘𝑥))) |
| 100 | 7, 80, 84 | divrec2d 12047 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((sin‘𝑥) /
((cos‘𝑥)↑2)) =
((1 / ((cos‘𝑥)↑2)) · (sin‘𝑥))) |
| 101 | 99, 100 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) = ((sin‘𝑥) / ((cos‘𝑥)↑2))) |
| 102 | 101 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥)) = (((sin‘𝑥) / ((cos‘𝑥)↑2)) ·
(sin‘𝑥))) |
| 103 | 95, 97, 102 | 3eqtr4rd 2788 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥)) = (((sin‘𝑥)↑2) / ((cos‘𝑥)↑2))) |
| 104 | 94, 103 | oveq12d 7449 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥))) =
((((cos‘𝑥)↑2) /
((cos‘𝑥)↑2)) +
(((sin‘𝑥)↑2) /
((cos‘𝑥)↑2)))) |
| 105 | | 2nn0 12543 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
| 106 | | expneg 14110 |
. . . . . 6
⊢
(((cos‘𝑥)
∈ ℂ ∧ 2 ∈ ℕ0) → ((cos‘𝑥)↑-2) = (1 /
((cos‘𝑥)↑2))) |
| 107 | 8, 105, 106 | sylancl 586 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥)↑-2) =
(1 / ((cos‘𝑥)↑2))) |
| 108 | 91, 104, 107 | 3eqtr4d 2787 |
. . . 4
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥))) =
((cos‘𝑥)↑-2)) |
| 109 | 108 | rgen 3063 |
. . 3
⊢
∀𝑥 ∈
(◡cos “ (ℂ ∖
{0}))(((cos‘𝑥)
· (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥))) = ((cos‘𝑥)↑-2) |
| 110 | | mpteq12 5234 |
. . 3
⊢ (((◡cos “ (ℂ ∖ {0})) = dom tan
∧ ∀𝑥 ∈
(◡cos “ (ℂ ∖
{0}))(((cos‘𝑥)
· (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥))) = ((cos‘𝑥)↑-2)) → (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥)))) =
(𝑥 ∈ dom tan ↦
((cos‘𝑥)↑-2))) |
| 111 | 79, 109, 110 | mp2an 692 |
. 2
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥)))) =
(𝑥 ∈ dom tan ↦
((cos‘𝑥)↑-2)) |
| 112 | 18, 76, 111 | 3eqtri 2769 |
1
⊢ (ℂ
D tan) = (𝑥 ∈ dom tan
↦ ((cos‘𝑥)↑-2)) |