tanval3

Description: Express the tangent function directly in terms of exp . (Contributed by Mario Carneiro, 25-Feb-2015)

		Ref	Expression
	Assertion	tanval3	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	\|- _i e. CC
2		simpl	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> A e. CC )
3		mulcl	\|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4	1 2 3	sylancr	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. A ) e. CC )
5		efcl	\|- ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
6	4 5	syl	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( _i x. A ) ) e. CC )
7		negicn	\|- -u _i e. CC
8		mulcl	\|- ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
9	7 2 8	sylancr	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( -u _i x. A ) e. CC )
10		efcl	\|- ( ( -u _i x. A ) e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
11	9 10	syl	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( -u _i x. A ) ) e. CC )
12	6 11	subcld	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) e. CC )
13	6 11	addcld	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) e. CC )
14		mulcl	\|- ( ( _i e. CC /\ ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) e. CC ) -> ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) e. CC )
15	1 13 14	sylancr	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) e. CC )
16		2z	\|- 2 e. ZZ
17		efexp	\|- ( ( ( _i x. A ) e. CC /\ 2 e. ZZ ) -> ( exp ` ( 2 x. ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) ^ 2 ) )
18	4 16 17	sylancl	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( 2 x. ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) ^ 2 ) )
19	6	sqvald	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) ^ 2 ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) )
20	18 19	eqtrd	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( 2 x. ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) )
21		mulneg1	\|- ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = -u ( _i x. A ) )
22	1 2 21	sylancr	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( -u _i x. A ) = -u ( _i x. A ) )
23	22	fveq2d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( -u _i x. A ) ) = ( exp ` -u ( _i x. A ) ) )
24	23	oveq2d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` -u ( _i x. A ) ) ) )
25		efcan	\|- ( ( _i x. A ) e. CC -> ( ( exp ` ( _i x. A ) ) x. ( exp ` -u ( _i x. A ) ) ) = 1 )
26	4 25	syl	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` -u ( _i x. A ) ) ) = 1 )
27	24 26	eqtr2d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> 1 = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) )
28	20 27	oveq12d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) + ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) ) )
29	6 6 11	adddid	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) + ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) ) )
30	28 29	eqtr4d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) = ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) )
31	30	oveq2d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) = ( _i x. ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
32	1	a1i	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> _i e. CC )
33	32 6 13	mul12d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
34	31 33	eqtrd	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) = ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
35		2cn	\|- 2 e. CC
36		mulcl	\|- ( ( 2 e. CC /\ ( _i x. A ) e. CC ) -> ( 2 x. ( _i x. A ) ) e. CC )
37	35 4 36	sylancr	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( 2 x. ( _i x. A ) ) e. CC )
38		efcl	\|- ( ( 2 x. ( _i x. A ) ) e. CC -> ( exp ` ( 2 x. ( _i x. A ) ) ) e. CC )
39	37 38	syl	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( 2 x. ( _i x. A ) ) ) e. CC )
40		ax-1cn	\|- 1 e. CC
41		addcl	\|- ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) e. CC /\ 1 e. CC ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) e. CC )
42	39 40 41	sylancl	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) e. CC )
43		ine0	\|- _i =/= 0
44	43	a1i	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> _i =/= 0 )
45		simpr	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 )
46	32 42 44 45	mulne0d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) =/= 0 )
47	34 46	eqnetrrd	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) =/= 0 )
48	6 15 47	mulne0bbd	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) =/= 0 )
49		efne0	\|- ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) =/= 0 )
50	4 49	syl	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( _i x. A ) ) =/= 0 )
51	12 15 6 48 50	divcan5d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) ) / ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
52	20 27	oveq12d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) - ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) ) )
53	6 6 11	subdid	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) - ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) ) )
54	52 53	eqtr4d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) = ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) ) )
55	54 34	oveq12d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) ) / ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) ) )
56		cosval	\|- ( A e. CC -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
57	56	adantr	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
58		2cnd	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> 2 e. CC )
59	32 13 48	mulne0bbd	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) =/= 0 )
60		2ne0	\|- 2 =/= 0
61	60	a1i	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> 2 =/= 0 )
62	13 58 59 61	divne0d	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) =/= 0 )
63	57 62	eqnetrd	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( cos ` A ) =/= 0 )
64		tanval2	\|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
65	63 64	syldan	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
66	51 55 65	3eqtr4rd	\|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) ) )

Metamath Proof Explorer

Theorem tanval3

Proof