dvtan - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvtan		Structured version Visualization version GIF version

Theorem dvtan 38427

Description: Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.)

**Assertion**
Ref	Expression
dvtan	⊢ (ℂ D tan) = (𝑥 ∈ dom tan ↦ ((cos‘𝑥)↑-2))

Proof of Theorem dvtan Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-tan 16163	. . . 4 ⊢ tan = (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
2		cnvimass 6082	. . . . . . . . 9 ⊢ (^◡cos “ (ℂ ∖ {0})) ⊆ dom cos
3		cosf 16219	. . . . . . . . . 10 ⊢ cos:ℂ⟶ℂ
4	3	fdmi 6718	. . . . . . . . 9 ⊢ dom cos = ℂ
5	2, 4	sseqtri 3982	. . . . . . . 8 ⊢ (^◡cos “ (ℂ ∖ {0})) ⊆ ℂ
6	5	sseli 3930	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
7	6	sincld 16224	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (sin‘𝑥) ∈ ℂ)
8	6	coscld 16225	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (cos‘𝑥) ∈ ℂ)
9		ffn 6706	. . . . . . . 8 ⊢ (cos:ℂ⟶ℂ → cos Fn ℂ)
10		elpreima 7054	. . . . . . . 8 ⊢ (cos Fn ℂ → (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↔ (𝑥 ∈ ℂ ∧ (cos‘𝑥) ∈ (ℂ ∖ {0}))))
11	3, 9, 10	mp2b 10	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↔ (𝑥 ∈ ℂ ∧ (cos‘𝑥) ∈ (ℂ ∖ {0})))
12		eldifsni 4756	. . . . . . . 8 ⊢ ((cos‘𝑥) ∈ (ℂ ∖ {0}) → (cos‘𝑥) ≠ 0)
13	12	adantl 487	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ (cos‘𝑥) ∈ (ℂ ∖ {0})) → (cos‘𝑥) ≠ 0)
14	11, 13	sylbi 220	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (cos‘𝑥) ≠ 0)
15	7, 8, 14	divrecd 12022	. . . . 5 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((sin‘𝑥) / (cos‘𝑥)) = ((sin‘𝑥) · (1 / (cos‘𝑥))))
16	15	mpteq2ia 5204	. . . 4 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥))) = (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) · (1 / (cos‘𝑥))))
17	1, 16	eqtri 2785	. . 3 ⊢ tan = (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) · (1 / (cos‘𝑥))))
18	17	oveq2i 7428	. 2 ⊢ (ℂ D tan) = (ℂ D (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) · (1 / (cos‘𝑥)))))
19		cnelprrecn 11221	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
20	19	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
21		difss 4086	. . . . . . . . 9 ⊢ (ℂ ∖ {0}) ⊆ ℂ
22		imass2 6102	. . . . . . . . 9 ⊢ ((ℂ ∖ {0}) ⊆ ℂ → (^◡cos “ (ℂ ∖ {0})) ⊆ (^◡cos “ ℂ))
23	21, 22	ax-mp 5	. . . . . . . 8 ⊢ (^◡cos “ (ℂ ∖ {0})) ⊆ (^◡cos “ ℂ)
24		fimacnv 6729	. . . . . . . . 9 ⊢ (cos:ℂ⟶ℂ → (^◡cos “ ℂ) = ℂ)
25	3, 24	ax-mp 5	. . . . . . . 8 ⊢ (^◡cos “ ℂ) = ℂ
26	23, 25	sseqtri 3982	. . . . . . 7 ⊢ (^◡cos “ (ℂ ∖ {0})) ⊆ ℂ
27	26	sseli 3930	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
28	27	sincld 16224	. . . . 5 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (sin‘𝑥) ∈ ℂ)
29	28	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (^◡cos “ (ℂ ∖ {0}))) → (sin‘𝑥) ∈ ℂ)
30	8	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (^◡cos “ (ℂ ∖ {0}))) → (cos‘𝑥) ∈ ℂ)
31		sincl 16220	. . . . . 6 ⊢ (𝑥 ∈ ℂ → (sin‘𝑥) ∈ ℂ)
32	31	adantl 487	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (sin‘𝑥) ∈ ℂ)
33		coscl 16221	. . . . . 6 ⊢ (𝑥 ∈ ℂ → (cos‘𝑥) ∈ ℂ)
34	33	adantl 487	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (cos‘𝑥) ∈ ℂ)
35		dvsin 26216	. . . . . 6 ⊢ (ℂ D sin) = cos
36		sinf 16218	. . . . . . . . 9 ⊢ sin:ℂ⟶ℂ
37	36	a1i 11	. . . . . . . 8 ⊢ (⊤ → sin:ℂ⟶ℂ)
38	37	feqmptd 6950	. . . . . . 7 ⊢ (⊤ → sin = (𝑥 ∈ ℂ ↦ (sin‘𝑥)))
39	38	oveq2d 7433	. . . . . 6 ⊢ (⊤ → (ℂ D sin) = (ℂ D (𝑥 ∈ ℂ ↦ (sin‘𝑥))))
40	3	a1i 11	. . . . . . 7 ⊢ (⊤ → cos:ℂ⟶ℂ)
41	40	feqmptd 6950	. . . . . 6 ⊢ (⊤ → cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥)))
42	35, 39, 41	3eqtr3a 2821	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (sin‘𝑥))) = (𝑥 ∈ ℂ ↦ (cos‘𝑥)))
43	26	a1i 11	. . . . 5 ⊢ (⊤ → (^◡cos “ (ℂ ∖ {0})) ⊆ ℂ)
44		eqid 2762	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
45	44	cnfldtopon 25014	. . . . . 6 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
46	45	toponrestid 23152	. . . . 5 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
47		dvtanlem 38426	. . . . . 6 ⊢ (^◡cos “ (ℂ ∖ {0})) ∈ (TopOpen‘ℂ_fld)
48	47	a1i 11	. . . . 5 ⊢ (⊤ → (^◡cos “ (ℂ ∖ {0})) ∈ (TopOpen‘ℂ_fld))
49	20, 32, 34, 42, 43, 46, 44, 48	dvmptres 26197	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ (sin‘𝑥))) = (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ (cos‘𝑥)))
50	8, 14	reccld 12012	. . . . 5 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (1 / (cos‘𝑥)) ∈ ℂ)
51	50	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (^◡cos “ (ℂ ∖ {0}))) → (1 / (cos‘𝑥)) ∈ ℂ)
52		ovexd 7452	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (^◡cos “ (ℂ ∖ {0}))) → (-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) ∈ V)
53	11	simprbi 503	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (cos‘𝑥) ∈ (ℂ ∖ {0}))
54	53	adantl 487	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (^◡cos “ (ℂ ∖ {0}))) → (cos‘𝑥) ∈ (ℂ ∖ {0}))
55	29	negcld 11584	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (^◡cos “ (ℂ ∖ {0}))) → -(sin‘𝑥) ∈ ℂ)
56		eldifi 4081	. . . . . . 7 ⊢ (𝑦 ∈ (ℂ ∖ {0}) → 𝑦 ∈ ℂ)
57		eldifsni 4756	. . . . . . 7 ⊢ (𝑦 ∈ (ℂ ∖ {0}) → 𝑦 ≠ 0)
58	56, 57	reccld 12012	. . . . . 6 ⊢ (𝑦 ∈ (ℂ ∖ {0}) → (1 / 𝑦) ∈ ℂ)
59	58	adantl 487	. . . . 5 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ {0})) → (1 / 𝑦) ∈ ℂ)
60		negex 11483	. . . . . 6 ⊢ -(1 / (𝑦↑2)) ∈ V
61	60	a1i 11	. . . . 5 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ {0})) → -(1 / (𝑦↑2)) ∈ V)
62	32	negcld 11584	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(sin‘𝑥) ∈ ℂ)
63	41	oveq2d 7433	. . . . . . 7 ⊢ (⊤ → (ℂ D cos) = (ℂ D (𝑥 ∈ ℂ ↦ (cos‘𝑥))))
64		dvcos 26217	. . . . . . 7 ⊢ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥))
65	63, 64	eqtr3di 2812	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (cos‘𝑥))) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)))
66	20, 34, 62, 65, 43, 46, 44, 48	dvmptres 26197	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ (cos‘𝑥))) = (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ -(sin‘𝑥)))
67		ax-1cn 11186	. . . . . 6 ⊢ 1 ∈ ℂ
68		dvrec 26189	. . . . . 6 ⊢ (1 ∈ ℂ → (ℂ D (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 / (𝑦↑2))))
69	67, 68	mp1i 14	. . . . 5 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 / (𝑦↑2))))
70		oveq2 7425	. . . . 5 ⊢ (𝑦 = (cos‘𝑥) → (1 / 𝑦) = (1 / (cos‘𝑥)))
71		oveq1 7424	. . . . . . 7 ⊢ (𝑦 = (cos‘𝑥) → (𝑦↑2) = ((cos‘𝑥)↑2))
72	71	oveq2d 7433	. . . . . 6 ⊢ (𝑦 = (cos‘𝑥) → (1 / (𝑦↑2)) = (1 / ((cos‘𝑥)↑2)))
73	72	negeqd 11479	. . . . 5 ⊢ (𝑦 = (cos‘𝑥) → -(1 / (𝑦↑2)) = -(1 / ((cos‘𝑥)↑2)))
74	20, 20, 54, 55, 59, 61, 66, 69, 70, 73	dvmptco 26206	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ (1 / (cos‘𝑥)))) = (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ (-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥))))
75	20, 29, 30, 49, 51, 52, 74	dvmptmul 26195	. . 3 ⊢ (⊤ → (ℂ D (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) · (1 / (cos‘𝑥))))) = (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ (((cos‘𝑥) · (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥)))))
76	75	mptru 1577	. 2 ⊢ (ℂ D (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) · (1 / (cos‘𝑥))))) = (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ (((cos‘𝑥) · (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥))))
77		ovex 7450	. . . . 5 ⊢ ((sin‘𝑥) / (cos‘𝑥)) ∈ V
78	77, 1	dmmpti 6680	. . . 4 ⊢ dom tan = (^◡cos “ (ℂ ∖ {0}))
79	78	eqcomi 2771	. . 3 ⊢ (^◡cos “ (ℂ ∖ {0})) = dom tan
80	8	sqcld 14212	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((cos‘𝑥)↑2) ∈ ℂ)
81	7	sqcld 14212	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((sin‘𝑥)↑2) ∈ ℂ)
82		sqne0 14191	. . . . . . . . 9 ⊢ ((cos‘𝑥) ∈ ℂ → (((cos‘𝑥)↑2) ≠ 0 ↔ (cos‘𝑥) ≠ 0))
83	8, 82	syl 18	. . . . . . . 8 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((cos‘𝑥)↑2) ≠ 0 ↔ (cos‘𝑥) ≠ 0))
84	14, 83	mpbird 260	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((cos‘𝑥)↑2) ≠ 0)
85	80, 81, 80, 84	divdird 12057	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((((cos‘𝑥)↑2) + ((sin‘𝑥)↑2)) / ((cos‘𝑥)↑2)) = ((((cos‘𝑥)↑2) / ((cos‘𝑥)↑2)) + (((sin‘𝑥)↑2) / ((cos‘𝑥)↑2))))
86	80, 81	addcomd 11440	. . . . . . . 8 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((cos‘𝑥)↑2) + ((sin‘𝑥)↑2)) = (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)))
87		sincossq 16270	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) = 1)
88	6, 87	syl 18	. . . . . . . 8 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((sin‘𝑥)↑2) + ((cos‘𝑥)↑2)) = 1)
89	86, 88	eqtrd 2797	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((cos‘𝑥)↑2) + ((sin‘𝑥)↑2)) = 1)
90	89	oveq1d 7432	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((((cos‘𝑥)↑2) + ((sin‘𝑥)↑2)) / ((cos‘𝑥)↑2)) = (1 / ((cos‘𝑥)↑2)))
91	85, 90	eqtr3d 2799	. . . . 5 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((((cos‘𝑥)↑2) / ((cos‘𝑥)↑2)) + (((sin‘𝑥)↑2) / ((cos‘𝑥)↑2))) = (1 / ((cos‘𝑥)↑2)))
92	8, 14	recidd 12014	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((cos‘𝑥) · (1 / (cos‘𝑥))) = 1)
93	80, 84	dividd 12017	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((cos‘𝑥)↑2) / ((cos‘𝑥)↑2)) = 1)
94	92, 93	eqtr4d 2800	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((cos‘𝑥) · (1 / (cos‘𝑥))) = (((cos‘𝑥)↑2) / ((cos‘𝑥)↑2)))
95	7, 7, 80, 84	div23d 12056	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((sin‘𝑥) · (sin‘𝑥)) / ((cos‘𝑥)↑2)) = (((sin‘𝑥) / ((cos‘𝑥)↑2)) · (sin‘𝑥)))
96	7	sqvald 14211	. . . . . . . 8 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((sin‘𝑥)↑2) = ((sin‘𝑥) · (sin‘𝑥)))
97	96	oveq1d 7432	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((sin‘𝑥)↑2) / ((cos‘𝑥)↑2)) = (((sin‘𝑥) · (sin‘𝑥)) / ((cos‘𝑥)↑2)))
98	80, 84	reccld 12012	. . . . . . . . . 10 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (1 / ((cos‘𝑥)↑2)) ∈ ℂ)
99	98, 7	mul2negd 11697	. . . . . . . . 9 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) = ((1 / ((cos‘𝑥)↑2)) · (sin‘𝑥)))
100	7, 80, 84	divrec2d 12023	. . . . . . . . 9 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((sin‘𝑥) / ((cos‘𝑥)↑2)) = ((1 / ((cos‘𝑥)↑2)) · (sin‘𝑥)))
101	99, 100	eqtr4d 2800	. . . . . . . 8 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) = ((sin‘𝑥) / ((cos‘𝑥)↑2)))
102	101	oveq1d 7432	. . . . . . 7 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥)) = (((sin‘𝑥) / ((cos‘𝑥)↑2)) · (sin‘𝑥)))
103	95, 97, 102	3eqtr4rd 2808	. . . . . 6 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥)) = (((sin‘𝑥)↑2) / ((cos‘𝑥)↑2)))
104	94, 103	oveq12d 7435	. . . . 5 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((cos‘𝑥) · (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥))) = ((((cos‘𝑥)↑2) / ((cos‘𝑥)↑2)) + (((sin‘𝑥)↑2) / ((cos‘𝑥)↑2))))
105		2nn0 12549	. . . . . 6 ⊢ 2 ∈ ℕ₀
106		expneg 14137	. . . . . 6 ⊢ (((cos‘𝑥) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((cos‘𝑥)↑-2) = (1 / ((cos‘𝑥)↑2)))
107	8, 105, 106	sylancl 598	. . . . 5 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → ((cos‘𝑥)↑-2) = (1 / ((cos‘𝑥)↑2)))
108	91, 104, 107	3eqtr4d 2807	. . . 4 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) → (((cos‘𝑥) · (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥))) = ((cos‘𝑥)↑-2))
109	108	rgen 3080	. . 3 ⊢ ∀𝑥 ∈ (^◡cos “ (ℂ ∖ {0}))(((cos‘𝑥) · (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥))) = ((cos‘𝑥)↑-2)
110		mpteq12 5197	. . 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 705	. 2 ⊢ (𝑥 ∈ (^◡cos “ (ℂ ∖ {0})) ↦ (((cos‘𝑥) · (1 / (cos‘𝑥))) + ((-(1 / ((cos‘𝑥)↑2)) · -(sin‘𝑥)) · (sin‘𝑥)))) = (𝑥 ∈ dom tan ↦ ((cos‘𝑥)↑-2))
112	18, 76, 111	3eqtri 2789	1 ⊢ (ℂ D tan) = (𝑥 ∈ dom tan ↦ ((cos‘𝑥)↑-2))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 Vcvv 3453 ∖ cdif 3899 ⊆ wss 3902 {csn 4587 {cpr 4589 ↦ cmpt 5190 ^◡ccnv 5658 dom cdm 5659 “ cima 5662 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 + caddc 11131 · cmul 11133 -cneg 11470 / cdiv 11899 2c2 12323 ℕ₀cn0 12532 ↑cexp 14129 sincsin 16155 cosccos 16156 tanctan 16157 TopOpenctopn 17512 ℂ_fldccnfld 21591 D cdv 26097

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-inf2 9624 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206 ax-addf 11207

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-fi 9385 df-sup 9416 df-inf 9417 df-oi 9486 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-z 12620 df-dec 12741 df-uz 12892 df-q 13002 df-rp 13047 df-xneg 13167 df-xadd 13168 df-xmul 13169 df-ico 13408 df-icc 13409 df-fz 13566 df-fzo 13714 df-fl 13857 df-seq 14070 df-exp 14130 df-fac 14342 df-bc 14371 df-hash 14399 df-shft 15144 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-limsup 15562 df-clim 15579 df-rlim 15580 df-sum 15778 df-ef 16159 df-sin 16161 df-cos 16162 df-tan 16163 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-starv 17363 df-sca 17364 df-vsca 17365 df-ip 17366 df-tset 17367 df-ple 17368 df-ds 17370 df-unif 17371 df-hom 17372 df-cco 17373 df-rest 17513 df-topn 17514 df-0g 17532 df-gsum 17533 df-topgen 17534 df-pt 17535 df-prds 17538 df-xrs 17594 df-qtop 17599 df-imas 17600 df-xps 17602 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-submnd 18898 df-mulg 19197 df-cntz 19450 df-cmn 19915 df-psmet 21583 df-xmet 21584 df-met 21585 df-bl 21586 df-mopn 21587 df-fbas 21588 df-fg 21589 df-cnfld 21592 df-top 23125 df-topon 23142 df-topsp 23164 df-bases 23177 df-cld 23250 df-ntr 23251 df-cls 23252 df-nei 23329 df-lp 23367 df-perf 23368 df-cn 23458 df-cnp 23459 df-t1 23545 df-haus 23546 df-tx 23794 df-hmeo 23987 df-fil 24078 df-fm 24170 df-flim 24171 df-flf 24172 df-xms 24552 df-ms 24553 df-tms 24554 df-cncf 25112 df-limc 26100 df-dv 26101

This theorem is used by: (None)

W3C validator