cotsqcscsq

Description: Prove the tangent squared cosecant squared identity ( 1 + ( ( cotA ) ^ 2 ) ) = ( ( cscA ) ^ 2 ) ) . (Contributed by David A. Wheeler, 27-May-2015)

		Ref	Expression
	Assertion	cotsqcscsq	$⊢ (A \in ℂ \land \sin A \neq 0) \to 1 + {\cot (A)}^{2} = {\csc (A)}^{2}$

Proof

Step	Hyp	Ref	Expression
1		cotval	$⊢ (A \in ℂ \land \sin A \neq 0) \to \cot (A) = \frac{\cos A}{\sin A}$
2	1	oveq1d	$⊢ (A \in ℂ \land \sin A \neq 0) \to {\cot (A)}^{2} = {(\frac{\cos A}{\sin A})}^{2}$
3	2	oveq2d	$⊢ (A \in ℂ \land \sin A \neq 0) \to 1 + {\cot (A)}^{2} = 1 + {(\frac{\cos A}{\sin A})}^{2}$
4		sincossq	$⊢ A \in ℂ \to {\sin A}^{2} + {\cos A}^{2} = 1$
5	4	oveq1d	$⊢ A \in ℂ \to \frac{{\sin A}^{2} + {\cos A}^{2}}{{\sin A}^{2}} = \frac{1}{{\sin A}^{2}}$
6	5	adantr	$⊢ (A \in ℂ \land \sin A \neq 0) \to \frac{{\sin A}^{2} + {\cos A}^{2}}{{\sin A}^{2}} = \frac{1}{{\sin A}^{2}}$
7		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
8	7	sqcld	$⊢ A \in ℂ \to {\sin A}^{2} \in ℂ$
9	8	adantr	$⊢ (A \in ℂ \land \sin A \neq 0) \to {\sin A}^{2} \in ℂ$
10		sqne0	$⊢ \sin A \in ℂ \to ({\sin A}^{2} \neq 0 \leftrightarrow \sin A \neq 0)$
11	7 10	syl	$⊢ A \in ℂ \to ({\sin A}^{2} \neq 0 \leftrightarrow \sin A \neq 0)$
12	11	biimpar	$⊢ (A \in ℂ \land \sin A \neq 0) \to {\sin A}^{2} \neq 0$
13	9 12	dividd	$⊢ (A \in ℂ \land \sin A \neq 0) \to \frac{{\sin A}^{2}}{{\sin A}^{2}} = 1$
14	13	oveq1d	$⊢ (A \in ℂ \land \sin A \neq 0) \to (\frac{{\sin A}^{2}}{{\sin A}^{2}}) + (\frac{{\cos A}^{2}}{{\sin A}^{2}}) = 1 + (\frac{{\cos A}^{2}}{{\sin A}^{2}})$
15		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
16	15	sqcld	$⊢ A \in ℂ \to {\cos A}^{2} \in ℂ$
17	16	adantr	$⊢ (A \in ℂ \land \sin A \neq 0) \to {\cos A}^{2} \in ℂ$
18	9 17 9 12	divdird	$⊢ (A \in ℂ \land \sin A \neq 0) \to \frac{{\sin A}^{2} + {\cos A}^{2}}{{\sin A}^{2}} = (\frac{{\sin A}^{2}}{{\sin A}^{2}}) + (\frac{{\cos A}^{2}}{{\sin A}^{2}})$
19	15 7	jca	$⊢ A \in ℂ \to (\cos A \in ℂ \land \sin A \in ℂ)$
20		2nn0	$⊢ 2 \in ℕ_{0}$
21		expdiv	$⊢ (\cos A \in ℂ \land (\sin A \in ℂ \land \sin A \neq 0) \land 2 \in ℕ_{0}) \to {(\frac{\cos A}{\sin A})}^{2} = \frac{{\cos A}^{2}}{{\sin A}^{2}}$
22	20 21	mp3an3	$⊢ (\cos A \in ℂ \land (\sin A \in ℂ \land \sin A \neq 0)) \to {(\frac{\cos A}{\sin A})}^{2} = \frac{{\cos A}^{2}}{{\sin A}^{2}}$
23	22	anassrs	$⊢ ((\cos A \in ℂ \land \sin A \in ℂ) \land \sin A \neq 0) \to {(\frac{\cos A}{\sin A})}^{2} = \frac{{\cos A}^{2}}{{\sin A}^{2}}$
24	19 23	sylan	$⊢ (A \in ℂ \land \sin A \neq 0) \to {(\frac{\cos A}{\sin A})}^{2} = \frac{{\cos A}^{2}}{{\sin A}^{2}}$
25	24	oveq2d	$⊢ (A \in ℂ \land \sin A \neq 0) \to 1 + {(\frac{\cos A}{\sin A})}^{2} = 1 + (\frac{{\cos A}^{2}}{{\sin A}^{2}})$
26	14 18 25	3eqtr4rd	$⊢ (A \in ℂ \land \sin A \neq 0) \to 1 + {(\frac{\cos A}{\sin A})}^{2} = \frac{{\sin A}^{2} + {\cos A}^{2}}{{\sin A}^{2}}$
27		cscval	$⊢ (A \in ℂ \land \sin A \neq 0) \to \csc (A) = \frac{1}{\sin A}$
28	27	oveq1d	$⊢ (A \in ℂ \land \sin A \neq 0) \to {\csc (A)}^{2} = {(\frac{1}{\sin A})}^{2}$
29		ax-1cn	$⊢ 1 \in ℂ$
30		expdiv	$⊢ (1 \in ℂ \land (\sin A \in ℂ \land \sin A \neq 0) \land 2 \in ℕ_{0}) \to {(\frac{1}{\sin A})}^{2} = \frac{1^{2}}{{\sin A}^{2}}$
31	29 20 30	mp3an13	$⊢ (\sin A \in ℂ \land \sin A \neq 0) \to {(\frac{1}{\sin A})}^{2} = \frac{1^{2}}{{\sin A}^{2}}$
32	7 31	sylan	$⊢ (A \in ℂ \land \sin A \neq 0) \to {(\frac{1}{\sin A})}^{2} = \frac{1^{2}}{{\sin A}^{2}}$
33		sq1	$⊢ 1^{2} = 1$
34	33	oveq1i	$⊢ \frac{1^{2}}{{\sin A}^{2}} = \frac{1}{{\sin A}^{2}}$
35	32 34	eqtrdi	$⊢ (A \in ℂ \land \sin A \neq 0) \to {(\frac{1}{\sin A})}^{2} = \frac{1}{{\sin A}^{2}}$
36	28 35	eqtrd	$⊢ (A \in ℂ \land \sin A \neq 0) \to {\csc (A)}^{2} = \frac{1}{{\sin A}^{2}}$
37	6 26 36	3eqtr4rd	$⊢ (A \in ℂ \land \sin A \neq 0) \to {\csc (A)}^{2} = 1 + {(\frac{\cos A}{\sin A})}^{2}$
38	3 37	eqtr4d	$⊢ (A \in ℂ \land \sin A \neq 0) \to 1 + {\cot (A)}^{2} = {\csc (A)}^{2}$

Metamath Proof Explorer

Theorem cotsqcscsq

Proof