Step | Hyp | Ref
| Expression |
1 | | df-tan 14641 |
. . . 4
⊢ tan =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) /
(cos‘𝑥))) |
2 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡cos “ (ℂ ∖ {0})) ⊆
dom cos |
3 | | cosf 14694 |
. . . . . . . . . 10
⊢
cos:ℂ⟶ℂ |
4 | 3 | fdmi 5965 |
. . . . . . . . 9
⊢ dom cos =
ℂ |
5 | 2, 4 | sseqtri 3600 |
. . . . . . . 8
⊢ (◡cos “ (ℂ ∖ {0})) ⊆
ℂ |
6 | 5 | sseli 3564 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
𝑥 ∈
ℂ) |
7 | 6 | sincld 14699 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(sin‘𝑥) ∈
ℂ) |
8 | 6 | coscld 14700 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(cos‘𝑥) ∈
ℂ) |
9 | | ffn 5958 |
. . . . . . . 8
⊢
(cos:ℂ⟶ℂ → cos Fn ℂ) |
10 | | elpreima 6245 |
. . . . . . . 8
⊢ (cos Fn
ℂ → (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↔ (𝑥 ∈ ℂ
∧ (cos‘𝑥) ∈
(ℂ ∖ {0})))) |
11 | 3, 9, 10 | mp2b 10 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↔
(𝑥 ∈ ℂ ∧
(cos‘𝑥) ∈
(ℂ ∖ {0}))) |
12 | | eldifsni 4261 |
. . . . . . . 8
⊢
((cos‘𝑥)
∈ (ℂ ∖ {0}) → (cos‘𝑥) ≠ 0) |
13 | 12 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧
(cos‘𝑥) ∈
(ℂ ∖ {0})) → (cos‘𝑥) ≠ 0) |
14 | 11, 13 | sylbi 206 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(cos‘𝑥) ≠
0) |
15 | 7, 8, 14 | divrecd 10683 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((sin‘𝑥) /
(cos‘𝑥)) =
((sin‘𝑥) · (1
/ (cos‘𝑥)))) |
16 | 15 | mpteq2ia 4668 |
. . . 4
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) /
(cos‘𝑥))) = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) · (1
/ (cos‘𝑥)))) |
17 | 1, 16 | eqtri 2632 |
. . 3
⊢ tan =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) · (1
/ (cos‘𝑥)))) |
18 | 17 | oveq2i 6560 |
. 2
⊢ (ℂ
D tan) = (ℂ D (𝑥
∈ (◡cos “ (ℂ ∖
{0})) ↦ ((sin‘𝑥) · (1 / (cos‘𝑥))))) |
19 | | cnelprrecn 9908 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
20 | 19 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
21 | | difss 3699 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ⊆ ℂ |
22 | | imass2 5420 |
. . . . . . . . 9
⊢ ((ℂ
∖ {0}) ⊆ ℂ → (◡cos “ (ℂ ∖ {0})) ⊆
(◡cos “
ℂ)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ (◡cos “ (ℂ ∖ {0})) ⊆
(◡cos “ ℂ) |
24 | | fimacnv 6255 |
. . . . . . . . 9
⊢
(cos:ℂ⟶ℂ → (◡cos “ ℂ) =
ℂ) |
25 | 3, 24 | ax-mp 5 |
. . . . . . . 8
⊢ (◡cos “ ℂ) =
ℂ |
26 | 23, 25 | sseqtri 3600 |
. . . . . . 7
⊢ (◡cos “ (ℂ ∖ {0})) ⊆
ℂ |
27 | 26 | sseli 3564 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
𝑥 ∈
ℂ) |
28 | 27 | sincld 14699 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(sin‘𝑥) ∈
ℂ) |
29 | 28 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (sin‘𝑥)
∈ ℂ) |
30 | 8 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (cos‘𝑥)
∈ ℂ) |
31 | | sincl 14695 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
32 | 31 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (sin‘𝑥) ∈ ℂ) |
33 | | coscl 14696 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
(cos‘𝑥) ∈
ℂ) |
34 | 33 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (cos‘𝑥) ∈ ℂ) |
35 | | dvsin 23549 |
. . . . . 6
⊢ (ℂ
D sin) = cos |
36 | | sinf 14693 |
. . . . . . . . 9
⊢
sin:ℂ⟶ℂ |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ sin:ℂ⟶ℂ) |
38 | 37 | feqmptd 6159 |
. . . . . . 7
⊢ (⊤
→ sin = (𝑥 ∈
ℂ ↦ (sin‘𝑥))) |
39 | 38 | oveq2d 6565 |
. . . . . 6
⊢ (⊤
→ (ℂ D sin) = (ℂ D (𝑥 ∈ ℂ ↦ (sin‘𝑥)))) |
40 | 3 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ cos:ℂ⟶ℂ) |
41 | 40 | feqmptd 6159 |
. . . . . 6
⊢ (⊤
→ cos = (𝑥 ∈
ℂ ↦ (cos‘𝑥))) |
42 | 35, 39, 41 | 3eqtr3a 2668 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (sin‘𝑥))) = (𝑥 ∈ ℂ ↦ (cos‘𝑥))) |
43 | 26 | a1i 11 |
. . . . 5
⊢ (⊤
→ (◡cos “ (ℂ ∖
{0})) ⊆ ℂ) |
44 | | eqid 2610 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
45 | 44 | cnfldtopon 22396 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
46 | 45 | toponunii 20547 |
. . . . . . . 8
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
47 | 46 | restid 15917 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
48 | 45, 47 | ax-mp 5 |
. . . . . 6
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
49 | 48 | eqcomi 2619 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
50 | | dvtanlem 32629 |
. . . . . 6
⊢ (◡cos “ (ℂ ∖ {0})) ∈
(TopOpen‘ℂfld) |
51 | 50 | a1i 11 |
. . . . 5
⊢ (⊤
→ (◡cos “ (ℂ ∖
{0})) ∈ (TopOpen‘ℂfld)) |
52 | 20, 32, 34, 42, 43, 49, 44, 51 | dvmptres 23532 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↦ (sin‘𝑥))) =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(cos‘𝑥))) |
53 | 8, 14 | reccld 10673 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) → (1
/ (cos‘𝑥)) ∈
ℂ) |
54 | 53 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (1 / (cos‘𝑥)) ∈ ℂ) |
55 | | ovex 6577 |
. . . . 5
⊢ (-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
∈ V |
56 | 55 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) ∈ V) |
57 | 11 | simprbi 479 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(cos‘𝑥) ∈
(ℂ ∖ {0})) |
58 | 57 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → (cos‘𝑥)
∈ (ℂ ∖ {0})) |
59 | 29 | negcld 10258 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (◡cos “ (ℂ ∖
{0}))) → -(sin‘𝑥) ∈ ℂ) |
60 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ∈
ℂ) |
61 | | eldifsni 4261 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ≠
0) |
62 | 60, 61 | reccld 10673 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ (1 / 𝑦) ∈
ℂ) |
63 | 62 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ {0})) → (1 / 𝑦) ∈ ℂ) |
64 | | negex 10158 |
. . . . . 6
⊢ -(1 /
(𝑦↑2)) ∈
V |
65 | 64 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ {0})) → -(1 / (𝑦↑2)) ∈ V) |
66 | 32 | negcld 10258 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℂ) → -(sin‘𝑥) ∈ ℂ) |
67 | | dvcos 23550 |
. . . . . . 7
⊢ (ℂ
D cos) = (𝑥 ∈ ℂ
↦ -(sin‘𝑥)) |
68 | 41 | oveq2d 6565 |
. . . . . . 7
⊢ (⊤
→ (ℂ D cos) = (ℂ D (𝑥 ∈ ℂ ↦ (cos‘𝑥)))) |
69 | 67, 68 | syl5reqr 2659 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (cos‘𝑥))) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥))) |
70 | 20, 34, 66, 69, 43, 49, 44, 51 | dvmptres 23532 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↦ (cos‘𝑥))) =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
-(sin‘𝑥))) |
71 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
72 | | dvrec 23524 |
. . . . . 6
⊢ (1 ∈
ℂ → (ℂ D (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 /
(𝑦↑2)))) |
73 | 71, 72 | mp1i 13 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 /
(𝑦↑2)))) |
74 | | oveq2 6557 |
. . . . 5
⊢ (𝑦 = (cos‘𝑥) → (1 / 𝑦) = (1 / (cos‘𝑥))) |
75 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = (cos‘𝑥) → (𝑦↑2) = ((cos‘𝑥)↑2)) |
76 | 75 | oveq2d 6565 |
. . . . . 6
⊢ (𝑦 = (cos‘𝑥) → (1 / (𝑦↑2)) = (1 / ((cos‘𝑥)↑2))) |
77 | 76 | negeqd 10154 |
. . . . 5
⊢ (𝑦 = (cos‘𝑥) → -(1 / (𝑦↑2)) = -(1 / ((cos‘𝑥)↑2))) |
78 | 20, 20, 58, 59, 63, 65, 70, 73, 74, 77 | dvmptco 23541 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↦ (1 / (cos‘𝑥)))) = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)))) |
79 | 20, 29, 30, 52, 54, 56, 78 | dvmptmul 23530 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
(◡cos “ (ℂ ∖ {0}))
↦ ((sin‘𝑥)
· (1 / (cos‘𝑥))))) = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥))))) |
80 | 79 | trud 1484 |
. 2
⊢ (ℂ
D (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) · (1
/ (cos‘𝑥))))) =
(𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥)))) |
81 | | ovex 6577 |
. . . . 5
⊢
((sin‘𝑥) /
(cos‘𝑥)) ∈
V |
82 | 81, 1 | dmmpti 5936 |
. . . 4
⊢ dom tan =
(◡cos “ (ℂ ∖
{0})) |
83 | 82 | eqcomi 2619 |
. . 3
⊢ (◡cos “ (ℂ ∖ {0})) = dom
tan |
84 | 8 | sqcld 12868 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥)↑2)
∈ ℂ) |
85 | 7 | sqcld 12868 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((sin‘𝑥)↑2)
∈ ℂ) |
86 | | sqne0 12792 |
. . . . . . . . 9
⊢
((cos‘𝑥)
∈ ℂ → (((cos‘𝑥)↑2) ≠ 0 ↔ (cos‘𝑥) ≠ 0)) |
87 | 8, 86 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥)↑2)
≠ 0 ↔ (cos‘𝑥)
≠ 0)) |
88 | 14, 87 | mpbird 246 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥)↑2) ≠
0) |
89 | 84, 85, 84, 88 | divdird 10718 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((((cos‘𝑥)↑2) +
((sin‘𝑥)↑2)) /
((cos‘𝑥)↑2)) =
((((cos‘𝑥)↑2) /
((cos‘𝑥)↑2)) +
(((sin‘𝑥)↑2) /
((cos‘𝑥)↑2)))) |
90 | 84, 85 | addcomd 10117 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥)↑2) +
((sin‘𝑥)↑2)) =
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2))) |
91 | | sincossq 14745 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ →
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2)) =
1) |
92 | 6, 91 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((sin‘𝑥)↑2) +
((cos‘𝑥)↑2)) =
1) |
93 | 90, 92 | eqtrd 2644 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥)↑2) +
((sin‘𝑥)↑2)) =
1) |
94 | 93 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((((cos‘𝑥)↑2) +
((sin‘𝑥)↑2)) /
((cos‘𝑥)↑2)) =
(1 / ((cos‘𝑥)↑2))) |
95 | 89, 94 | eqtr3d 2646 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((((cos‘𝑥)↑2) /
((cos‘𝑥)↑2)) +
(((sin‘𝑥)↑2) /
((cos‘𝑥)↑2))) =
(1 / ((cos‘𝑥)↑2))) |
96 | 8, 14 | recidd 10675 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥) · (1
/ (cos‘𝑥))) =
1) |
97 | 84, 88 | dividd 10678 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥)↑2) /
((cos‘𝑥)↑2)) =
1) |
98 | 96, 97 | eqtr4d 2647 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥) · (1
/ (cos‘𝑥))) =
(((cos‘𝑥)↑2) /
((cos‘𝑥)↑2))) |
99 | 7, 7, 84, 88 | div23d 10717 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((sin‘𝑥) ·
(sin‘𝑥)) /
((cos‘𝑥)↑2)) =
(((sin‘𝑥) /
((cos‘𝑥)↑2))
· (sin‘𝑥))) |
100 | 7 | sqvald 12867 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((sin‘𝑥)↑2) =
((sin‘𝑥) ·
(sin‘𝑥))) |
101 | 100 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((sin‘𝑥)↑2) /
((cos‘𝑥)↑2)) =
(((sin‘𝑥) ·
(sin‘𝑥)) /
((cos‘𝑥)↑2))) |
102 | 84, 88 | reccld 10673 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) → (1
/ ((cos‘𝑥)↑2))
∈ ℂ) |
103 | 102, 7 | mul2negd 10364 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) = ((1 / ((cos‘𝑥)↑2)) ·
(sin‘𝑥))) |
104 | 7, 84, 88 | divrec2d 10684 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((sin‘𝑥) /
((cos‘𝑥)↑2)) =
((1 / ((cos‘𝑥)↑2)) · (sin‘𝑥))) |
105 | 103, 104 | eqtr4d 2647 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) = ((sin‘𝑥) / ((cos‘𝑥)↑2))) |
106 | 105 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥)) = (((sin‘𝑥) / ((cos‘𝑥)↑2)) ·
(sin‘𝑥))) |
107 | 99, 101, 106 | 3eqtr4rd 2655 |
. . . . . 6
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥)) = (((sin‘𝑥)↑2) / ((cos‘𝑥)↑2))) |
108 | 98, 107 | oveq12d 6567 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥))) =
((((cos‘𝑥)↑2) /
((cos‘𝑥)↑2)) +
(((sin‘𝑥)↑2) /
((cos‘𝑥)↑2)))) |
109 | | 2nn0 11186 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
110 | | expneg 12730 |
. . . . . 6
⊢
(((cos‘𝑥)
∈ ℂ ∧ 2 ∈ ℕ0) → ((cos‘𝑥)↑-2) = (1 /
((cos‘𝑥)↑2))) |
111 | 8, 109, 110 | sylancl 693 |
. . . . 5
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
((cos‘𝑥)↑-2) =
(1 / ((cos‘𝑥)↑2))) |
112 | 95, 108, 111 | 3eqtr4d 2654 |
. . . 4
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) →
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥))) =
((cos‘𝑥)↑-2)) |
113 | 112 | rgen 2906 |
. . 3
⊢
∀𝑥 ∈
(◡cos “ (ℂ ∖
{0}))(((cos‘𝑥)
· (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥))) = ((cos‘𝑥)↑-2) |
114 | | mpteq12 4664 |
. . 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))) |
115 | 83, 113, 114 | mp2an 704 |
. 2
⊢ (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
(((cos‘𝑥) · (1
/ (cos‘𝑥))) + ((-(1 /
((cos‘𝑥)↑2))
· -(sin‘𝑥))
· (sin‘𝑥)))) =
(𝑥 ∈ dom tan ↦
((cos‘𝑥)↑-2)) |
116 | 18, 80, 115 | 3eqtri 2636 |
1
⊢ (ℂ
D tan) = (𝑥 ∈ dom tan
↦ ((cos‘𝑥)↑-2)) |