Theorem atantan 26082

Description: The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.)

Assertion

Ref	Expression
atantan	⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴)

Proof of Theorem atantan

Step	Hyp	Ref	Expression
1		cosne0 25694	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘𝐴) ≠ 0)
2		atandmtan 26079	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ dom arctan)
3	1, 2	syldan 591	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ dom arctan)
4		atanval 26043	. . 3 ⊢ ((tan‘𝐴) ∈ dom arctan → (arctan‘(tan‘𝐴)) = ((i / 2) · ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴)))))))
5	3, 4	syl 17	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = ((i / 2) · ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴)))))))
6		ax-1cn 10938	. . . . . . 7 ⊢ 1 ∈ ℂ
7		ax-icn 10939	. . . . . . . 8 ⊢ i ∈ ℂ
8		tancl 15847	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ)
9	1, 8	syldan 591	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ ℂ)
10		mulcl 10964	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ (tan‘𝐴) ∈ ℂ) → (i · (tan‘𝐴)) ∈ ℂ)
11	7, 9, 10	sylancr 587	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) ∈ ℂ)
12		addcl 10962	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 + (i · (tan‘𝐴))) ∈ ℂ)
13	6, 11, 12	sylancr 587	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ∈ ℂ)
14		atandm2 26036	. . . . . . . 8 ⊢ ((tan‘𝐴) ∈ dom arctan ↔ ((tan‘𝐴) ∈ ℂ ∧ (1 − (i · (tan‘𝐴))) ≠ 0 ∧ (1 + (i · (tan‘𝐴))) ≠ 0))
15	3, 14	sylib 217	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((tan‘𝐴) ∈ ℂ ∧ (1 − (i · (tan‘𝐴))) ≠ 0 ∧ (1 + (i · (tan‘𝐴))) ≠ 0))
16	15	simp3d 1143	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ≠ 0)
17	13, 16	logcld 25735	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(1 + (i · (tan‘𝐴)))) ∈ ℂ)
18		subcl 11229	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 − (i · (tan‘𝐴))) ∈ ℂ)
19	6, 11, 18	sylancr 587	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ∈ ℂ)
20	15	simp2d 1142	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ≠ 0)
21	19, 20	logcld 25735	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(1 − (i · (tan‘𝐴)))) ∈ ℂ)
22	17, 21	negsubdi2d 11357	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴))))))
23		efsub 15818	. . . . . . . . 9 ⊢ (((log‘(1 + (i · (tan‘𝐴)))) ∈ ℂ ∧ (log‘(1 − (i · (tan‘𝐴)))) ∈ ℂ) → (exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴)))))) = ((exp‘(log‘(1 + (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i · (tan‘𝐴)))))))
24	17, 21, 23	syl2anc 584	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴)))))) = ((exp‘(log‘(1 + (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i · (tan‘𝐴)))))))
25		coscl 15845	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
26	25	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
27		sincl 15844	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
28	27	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
29		mulcl 10964	. . . . . . . . . . . . 13 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
30	7, 28, 29	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
31	26, 30, 26, 1	divdird 11798	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴))))
32	26, 1	dividd 11758	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘𝐴) / (cos‘𝐴)) = 1)
33	7	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → i ∈ ℂ)
34	33, 28, 26, 1	divassd 11795	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴))))
35		tanval 15846	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
36	1, 35	syldan 591	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
37	36	oveq2d 7300	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴))))
38	34, 37	eqtr4d 2782	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · (tan‘𝐴)))
39	32, 38	oveq12d 7302	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 + (i · (tan‘𝐴))))
40	31, 39	eqtrd 2779	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 + (i · (tan‘𝐴))))
41		efival 15870	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
42	41	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
43	42	oveq1d 7299	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)))
44		eflog 25741	. . . . . . . . . . 11 ⊢ (((1 + (i · (tan‘𝐴))) ∈ ℂ ∧ (1 + (i · (tan‘𝐴))) ≠ 0) → (exp‘(log‘(1 + (i · (tan‘𝐴))))) = (1 + (i · (tan‘𝐴))))
45	13, 16, 44	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 + (i · (tan‘𝐴))))) = (1 + (i · (tan‘𝐴))))
46	40, 43, 45	3eqtr4d 2789	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 + (i · (tan‘𝐴))))))
47	26, 30, 26, 1	divsubdird 11799	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴))))
48	32, 38	oveq12d 7302	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 − (i · (tan‘𝐴))))
49	47, 48	eqtrd 2779	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 − (i · (tan‘𝐴))))
50		negcl 11230	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
51	50	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ)
52		efival 15870	. . . . . . . . . . . . . 14 ⊢ (-𝐴 ∈ ℂ → (exp‘(i · -𝐴)) = ((cos‘-𝐴) + (i · (sin‘-𝐴))))
53	51, 52	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘-𝐴) + (i · (sin‘-𝐴))))
54		cosneg 15865	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴))
55	54	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘-𝐴) = (cos‘𝐴))
56		sinneg 15864	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴))
57	56	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (sin‘-𝐴) = -(sin‘𝐴))
58	57	oveq2d 7300	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = (i · -(sin‘𝐴)))
59		mulneg2 11421	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · -(sin‘𝐴)) = -(i · (sin‘𝐴)))
60	7, 28, 59	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -(sin‘𝐴)) = -(i · (sin‘𝐴)))
61	58, 60	eqtrd 2779	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = -(i · (sin‘𝐴)))
62	55, 61	oveq12d 7302	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘-𝐴) + (i · (sin‘-𝐴))) = ((cos‘𝐴) + -(i · (sin‘𝐴))))
63	53, 62	eqtrd 2779	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘𝐴) + -(i · (sin‘𝐴))))
64		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ)
65		mulneg2 11421	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · -𝐴) = -(i · 𝐴))
66	7, 64, 65	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -𝐴) = -(i · 𝐴))
67	66	fveq2d 6787	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = (exp‘-(i · 𝐴)))
68	26, 30	negsubd 11347	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘𝐴) + -(i · (sin‘𝐴))) = ((cos‘𝐴) − (i · (sin‘𝐴))))
69	63, 67, 68	3eqtr3d 2787	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴))))
70	69	oveq1d 7299	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)))
71		eflog 25741	. . . . . . . . . . 11 ⊢ (((1 − (i · (tan‘𝐴))) ∈ ℂ ∧ (1 − (i · (tan‘𝐴))) ≠ 0) → (exp‘(log‘(1 − (i · (tan‘𝐴))))) = (1 − (i · (tan‘𝐴))))
72	19, 20, 71	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 − (i · (tan‘𝐴))))) = (1 − (i · (tan‘𝐴))))
73	49, 70, 72	3eqtr4d 2789	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 − (i · (tan‘𝐴))))))
74	46, 73	oveq12d 7302	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(log‘(1 + (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i · (tan‘𝐴)))))))
75		mulcl 10964	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
76	7, 64, 75	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ)
77		efcl 15801	. . . . . . . . . . 11 ⊢ ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
78	76, 77	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ)
79	76	negcld 11328	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -(i · 𝐴) ∈ ℂ)
80		efcl 15801	. . . . . . . . . . 11 ⊢ (-(i · 𝐴) ∈ ℂ → (exp‘-(i · 𝐴)) ∈ ℂ)
81	79, 80	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ∈ ℂ)
82		efne0 15815	. . . . . . . . . . 11 ⊢ (-(i · 𝐴) ∈ ℂ → (exp‘-(i · 𝐴)) ≠ 0)
83	79, 82	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ≠ 0)
84	78, 81, 26, 83, 1	divcan7d 11788	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
85		efsub 15818	. . . . . . . . . 10 ⊢ (((i · 𝐴) ∈ ℂ ∧ -(i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
86	76, 79, 85	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
87	76, 76	subnegd 11348	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
88	76	2timesd 12225	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
89	87, 88	eqtr4d 2782	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = (2 · (i · 𝐴)))
90	89	fveq2d 6787	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = (exp‘(2 · (i · 𝐴))))
91	84, 86, 90	3eqtr2d 2785	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = (exp‘(2 · (i · 𝐴))))
92	24, 74, 91	3eqtr2d 2785	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴)))))) = (exp‘(2 · (i · 𝐴))))
93	92	fveq2d 6787	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))) = (log‘(exp‘(2 · (i · 𝐴)))))
94	64	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 𝐴 ∈ ℂ)
95	94	renegd 14929	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) = -(ℜ‘𝐴))
96	94	recld 14914	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) ∈ ℝ)
97	96	renegcld 11411	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈ ℝ)
98		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) < 0)
99	96	lt0neg1d 11553	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((ℜ‘𝐴) < 0 ↔ 0 < -(ℜ‘𝐴)))
100	98, 99	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < -(ℜ‘𝐴))
101		eliooord 13147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2)) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
102	101	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
103	102	simpld 495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -(π / 2) < (ℜ‘𝐴))
104	103	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(π / 2) < (ℜ‘𝐴))
105		halfpire 25630	. . . . . . . . . . . . . . . . 17 ⊢ (π / 2) ∈ ℝ
106		ltnegcon1 11485	. . . . . . . . . . . . . . . . 17 ⊢ (((π / 2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (-(π / 2) < (ℜ‘𝐴) ↔ -(ℜ‘𝐴) < (π / 2)))
107	105, 96, 106	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (-(π / 2) < (ℜ‘𝐴) ↔ -(ℜ‘𝐴) < (π / 2)))
108	104, 107	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) < (π / 2))
109		0xr 11031	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ*
110	105	rexri 11042	. . . . . . . . . . . . . . . 16 ⊢ (π / 2) ∈ ℝ*
111		elioo2 13129	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ* ∧ (π / 2) ∈ ℝ*) → (-(ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 < -(ℜ‘𝐴) ∧ -(ℜ‘𝐴) < (π / 2))))
112	109, 110, 111	mp2an 689	. . . . . . . . . . . . . . 15 ⊢ (-(ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 < -(ℜ‘𝐴) ∧ -(ℜ‘𝐴) < (π / 2)))
113	97, 100, 108, 112	syl3anbrc 1342	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈ (0(,)(π / 2)))
114	95, 113	eqeltrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) ∈ (0(,)(π / 2)))
115		tanregt0 25704	. . . . . . . . . . . . 13 ⊢ ((-𝐴 ∈ ℂ ∧ (ℜ‘-𝐴) ∈ (0(,)(π / 2))) → 0 < (ℜ‘(tan‘-𝐴)))
116	51, 114, 115	syl2an2r 682	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < (ℜ‘(tan‘-𝐴)))
117		tanneg 15866	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘-𝐴) = -(tan‘𝐴))
118	1, 117	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘-𝐴) = -(tan‘𝐴))
119	118	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘-𝐴) = -(tan‘𝐴))
120	119	fveq2d 6787	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘-𝐴)) = (ℜ‘-(tan‘𝐴)))
121	9	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘𝐴) ∈ ℂ)
122	121	renegd 14929	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-(tan‘𝐴)) = -(ℜ‘(tan‘𝐴)))
123	120, 122	eqtrd 2779	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘-𝐴)) = -(ℜ‘(tan‘𝐴)))
124	116, 123	breqtrd 5101	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < -(ℜ‘(tan‘𝐴)))
125	9	recld 14914	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘(tan‘𝐴)) ∈ ℝ)
126	125	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) ∈ ℝ)
127	126	lt0neg1d 11553	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((ℜ‘(tan‘𝐴)) < 0 ↔ 0 < -(ℜ‘(tan‘𝐴))))
128	124, 127	mpbird 256	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) < 0)
129	128	lt0ne0d 11549	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) ≠ 0)
130		atanlogsub 26075	. . . . . . . . 9 ⊢ (((tan‘𝐴) ∈ dom arctan ∧ (ℜ‘(tan‘𝐴)) ≠ 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
131	3, 129, 130	syl2an2r 682	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
132		1re 10984	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
133		ioossre 13149	. . . . . . . . . . . . . 14 ⊢ (-1(,)1) ⊆ ℝ
134	7	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ∈ ℂ)
135	11	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ ℂ)
136		ine0 11419	. . . . . . . . . . . . . . . . 17 ⊢ i ≠ 0
137	136	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ≠ 0)
138		ixi 11613	. . . . . . . . . . . . . . . . . . 19 ⊢ (i · i) = -1
139	138	oveq1i 7294	. . . . . . . . . . . . . . . . . 18 ⊢ ((i · i) · (tan‘𝐴)) = (-1 · (tan‘𝐴))
140	9	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘𝐴) ∈ ℂ)
141	140	mulm1d 11436	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = -(tan‘𝐴))
142	118	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = -(tan‘𝐴))
143	141, 142	eqtr4d 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = (tan‘-𝐴))
144	139, 143	eqtrid 2791	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · (tan‘𝐴)) = (tan‘-𝐴))
145	134, 134, 140	mulassd 11007	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · (tan‘𝐴)) = (i · (i · (tan‘𝐴))))
146	138	oveq1i 7294	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((i · i) · 𝐴) = (-1 · 𝐴)
147	64	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 𝐴 ∈ ℂ)
148	147	mulm1d 11436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · 𝐴) = -𝐴)
149	146, 148	eqtrid 2791	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = -𝐴)
150	134, 134, 147	mulassd 11007	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = (i · (i · 𝐴)))
151	149, 150	eqtr3d 2781	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -𝐴 = (i · (i · 𝐴)))
152	151	fveq2d 6787	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = (tan‘(i · (i · 𝐴))))
153	144, 145, 152	3eqtr3d 2787	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (i · (tan‘𝐴))) = (tan‘(i · (i · 𝐴))))
154	134, 135, 137, 153	mvllmuld 11816	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) = ((tan‘(i · (i · 𝐴))) / i))
155	76	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℂ)
156		reim 14829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
157	156	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
158	157	eqeq1d 2741	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) = 0 ↔ (ℑ‘(i · 𝐴)) = 0))
159	158	biimpa 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (ℑ‘(i · 𝐴)) = 0)
160	155, 159	reim0bd 14920	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℝ)
161		tanhbnd 15879	. . . . . . . . . . . . . . . 16 ⊢ ((i · 𝐴) ∈ ℝ → ((tan‘(i · (i · 𝐴))) / i) ∈ (-1(,)1))
162	160, 161	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((tan‘(i · (i · 𝐴))) / i) ∈ (-1(,)1))
163	154, 162	eqeltrd 2840	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ (-1(,)1))
164	133, 163	sselid 3920	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ ℝ)
165		readdcl 10963	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ (i · (tan‘𝐴)) ∈ ℝ) → (1 + (i · (tan‘𝐴))) ∈ ℝ)
166	132, 164, 165	sylancr 587	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i · (tan‘𝐴))) ∈ ℝ)
167		df-neg 11217	. . . . . . . . . . . . . 14 ⊢ -1 = (0 − 1)
168		eliooord 13147	. . . . . . . . . . . . . . . 16 ⊢ ((i · (tan‘𝐴)) ∈ (-1(,)1) → (-1 < (i · (tan‘𝐴)) ∧ (i · (tan‘𝐴)) < 1))
169	163, 168	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 < (i · (tan‘𝐴)) ∧ (i · (tan‘𝐴)) < 1))
170	169	simpld 495	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -1 < (i · (tan‘𝐴)))
171	167, 170	eqbrtrrid 5111	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (0 − 1) < (i · (tan‘𝐴)))
172		0red 10987	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 ∈ ℝ)
173	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 1 ∈ ℝ)
174	172, 173, 164	ltsubadd2d 11582	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((0 − 1) < (i · (tan‘𝐴)) ↔ 0 < (1 + (i · (tan‘𝐴)))))
175	171, 174	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 < (1 + (i · (tan‘𝐴))))
176	166, 175	elrpd 12778	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i · (tan‘𝐴))) ∈ ℝ+)
177	176	relogcld 25787	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 + (i · (tan‘𝐴)))) ∈ ℝ)
178	169	simprd 496	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) < 1)
179		difrp 12777	. . . . . . . . . . . . 13 ⊢ (((i · (tan‘𝐴)) ∈ ℝ ∧ 1 ∈ ℝ) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i · (tan‘𝐴))) ∈ ℝ+))
180	164, 132, 179	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i · (tan‘𝐴))) ∈ ℝ+))
181	178, 180	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 − (i · (tan‘𝐴))) ∈ ℝ+)
182	181	relogcld 25787	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 − (i · (tan‘𝐴)))) ∈ ℝ)
183	177, 182	resubcld 11412	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ℝ)
184		relogrn 25726	. . . . . . . . 9 ⊢ (((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ℝ → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
185	183, 184	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
186	64	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 𝐴 ∈ ℂ)
187	186	recld 14914	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℝ)
188		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘𝐴))
189	102	simprd 496	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < (π / 2))
190	189	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) < (π / 2))
191		elioo2 13129	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ* ∧ (π / 2) ∈ ℝ*) → ((ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2))))
192	109, 110, 191	mp2an 689	. . . . . . . . . . . 12 ⊢ ((ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
193	187, 188, 190, 192	syl3anbrc 1342	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ (0(,)(π / 2)))
194		tanregt0 25704	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)(π / 2))) → 0 < (ℜ‘(tan‘𝐴)))
195	64, 193, 194	syl2an2r 682	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘(tan‘𝐴)))
196	195	gt0ne0d 11548	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(tan‘𝐴)) ≠ 0)
197	3, 196, 130	syl2an2r 682	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
198		recl 14830	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
199	198	adantr 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ)
200		0re 10986	. . . . . . . . 9 ⊢ 0 ∈ ℝ
201		lttri4 11068	. . . . . . . . 9 ⊢ (((ℜ‘𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 < (ℜ‘𝐴)))
202	199, 200, 201	sylancl 586	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 < (ℜ‘𝐴)))
203	131, 185, 197, 202	mpjao3dan 1430	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
204		logef 25746	. . . . . . 7 ⊢ (((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log → (log‘(exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))) = ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))
205	203, 204	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))) = ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))
206		2cn 12057	. . . . . . . . 9 ⊢ 2 ∈ ℂ
207		mulcl 10964	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · (i · 𝐴)) ∈ ℂ)
208	206, 76, 207	sylancr 587	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ℂ)
209		picn 25625	. . . . . . . . . . . 12 ⊢ π ∈ ℂ
210		2ne0 12086	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
211		divneg 11676	. . . . . . . . . . . 12 ⊢ ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = (-π / 2))
212	209, 206, 210, 211	mp3an 1460	. . . . . . . . . . 11 ⊢ -(π / 2) = (-π / 2)
213	212, 103	eqbrtrrid 5111	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-π / 2) < (ℜ‘𝐴))
214		pire 25624	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ
215	214	renegcli 11291	. . . . . . . . . . . 12 ⊢ -π ∈ ℝ
216	215	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π ∈ ℝ)
217		2re 12056	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
218	217	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 2 ∈ ℝ)
219		2pos 12085	. . . . . . . . . . . 12 ⊢ 0 < 2
220	219	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 0 < 2)
221		ltdivmul 11859	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 · (ℜ‘𝐴))))
222	216, 199, 218, 220, 221	syl112anc 1373	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 · (ℜ‘𝐴))))
223	213, 222	mpbid 231	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π < (2 · (ℜ‘𝐴)))
224		immul2 14857	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℑ‘(i · 𝐴))))
225	217, 76, 224	sylancr 587	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℑ‘(i · 𝐴))))
226	157	oveq2d 7300	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) = (2 · (ℑ‘(i · 𝐴))))
227	225, 226	eqtr4d 2782	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℜ‘𝐴)))
228	223, 227	breqtrrd 5103	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π < (ℑ‘(2 · (i · 𝐴))))
229		remulcl 10965	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (2 · (ℜ‘𝐴)) ∈ ℝ)
230	217, 199, 229	sylancr 587	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ∈ ℝ)
231	214	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → π ∈ ℝ)
232		ltmuldiv2 11858	. . . . . . . . . . . 12 ⊢ (((ℜ‘𝐴) ∈ ℝ ∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π / 2)))
233	199, 231, 218, 220, 232	syl112anc 1373	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π / 2)))
234	189, 233	mpbird 256	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) < π)
235	230, 231, 234	ltled 11132	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ≤ π)
236	227, 235	eqbrtrd 5097	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) ≤ π)
237		ellogrn 25724	. . . . . . . 8 ⊢ ((2 · (i · 𝐴)) ∈ ran log ↔ ((2 · (i · 𝐴)) ∈ ℂ ∧ -π < (ℑ‘(2 · (i · 𝐴))) ∧ (ℑ‘(2 · (i · 𝐴))) ≤ π))
238	208, 228, 236, 237	syl3anbrc 1342	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ran log)
239		logef 25746	. . . . . . 7 ⊢ ((2 · (i · 𝐴)) ∈ ran log → (log‘(exp‘(2 · (i · 𝐴)))) = (2 · (i · 𝐴)))
240	238, 239	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(exp‘(2 · (i · 𝐴)))) = (2 · (i · 𝐴)))
241	93, 205, 240	3eqtr3d 2787	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = (2 · (i · 𝐴)))
242	241	negeqd 11224	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = -(2 · (i · 𝐴)))
243	22, 242	eqtr3d 2781	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴))))) = -(2 · (i · 𝐴)))
244	243	oveq2d 7300	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴)))))) = ((i / 2) · -(2 · (i · 𝐴))))
245		halfcl 12207	. . . . 5 ⊢ (i ∈ ℂ → (i / 2) ∈ ℂ)
246	7, 245	mp1i 13	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i / 2) ∈ ℂ)
247	206	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 2 ∈ ℂ)
248	246, 247, 79	mulassd 11007	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i · 𝐴)) = ((i / 2) · (2 · -(i · 𝐴))))
249	7, 206, 210	divcan1i 11728	. . . . 5 ⊢ ((i / 2) · 2) = i
250	249	oveq1i 7294	. . . 4 ⊢ (((i / 2) · 2) · -(i · 𝐴)) = (i · -(i · 𝐴))
251	33, 33, 51	mulassd 11007	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = (i · (i · -𝐴)))
252	138	oveq1i 7294	. . . . . 6 ⊢ ((i · i) · -𝐴) = (-1 · -𝐴)
253		mul2neg 11423	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (-1 · -𝐴) = (1 · 𝐴))
254	6, 64, 253	sylancr 587	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = (1 · 𝐴))
255		mulid2 10983	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
256	255	adantr 481	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴)
257	254, 256	eqtrd 2779	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = 𝐴)
258	252, 257	eqtrid 2791	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = 𝐴)
259	66	oveq2d 7300	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (i · -𝐴)) = (i · -(i · 𝐴)))
260	251, 258, 259	3eqtr3rd 2788	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -(i · 𝐴)) = 𝐴)
261	250, 260	eqtrid 2791	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i · 𝐴)) = 𝐴)
262		mulneg2 11421	. . . . 5 ⊢ ((2 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · -(i · 𝐴)) = -(2 · (i · 𝐴)))
263	206, 76, 262	sylancr 587	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · -(i · 𝐴)) = -(2 · (i · 𝐴)))
264	263	oveq2d 7300	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · (2 · -(i · 𝐴))) = ((i / 2) · -(2 · (i · 𝐴))))
265	248, 261, 264	3eqtr3rd 2788	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · -(2 · (i · 𝐴))) = 𝐴)
266	5, 244, 265	3eqtrd 2783	1 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1085   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2944   class class class wbr 5075  dom cdm 5590  ran crn 5591  ‘cfv 6437  (class class class)co 7284  ℂcc 10878  ℝcr 10879  0cc0 10880  1c1 10881  ici 10882   + caddc 10883   · cmul 10885  ℝ^*cxr 11017   < clt 11018   ≤ cle 11019   − cmin 11214  -cneg 11215   / cdiv 11641  2c2 12037  ℝ⁺crp 12739  (,)cioo 13088  ℜcre 14817  ℑcim 14818  expce 15780  sincsin 15782  cosccos 15783  tanctan 15784  πcpi 15785  logclog 25719  arctancatan 26023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958  ax-addf 10959  ax-mulf 10960

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-supp 7987  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-er 8507  df-map 8626  df-pm 8627  df-ixp 8695  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fsupp 9138  df-fi 9179  df-sup 9210  df-inf 9211  df-oi 9278  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051  df-9 12052  df-n0 12243  df-z 12329  df-dec 12447  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-ioo 13092  df-ioc 13093  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-mod 13599  df-seq 13731  df-exp 13792  df-fac 13997  df-bc 14026  df-hash 14054  df-shft 14787  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-limsup 15189  df-clim 15206  df-rlim 15207  df-sum 15407  df-ef 15786  df-sin 15788  df-cos 15789  df-tan 15790  df-pi 15791  df-struct 16857  df-sets 16874  df-slot 16892  df-ndx 16904  df-base 16922  df-ress 16951  df-plusg 16984  df-mulr 16985  df-starv 16986  df-sca 16987  df-vsca 16988  df-ip 16989  df-tset 16990  df-ple 16991  df-ds 16993  df-unif 16994  df-hom 16995  df-cco 16996  df-rest 17142  df-topn 17143  df-0g 17161  df-gsum 17162  df-topgen 17163  df-pt 17164  df-prds 17167  df-xrs 17222  df-qtop 17227  df-imas 17228  df-xps 17230  df-mre 17304  df-mrc 17305  df-acs 17307  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-submnd 18440  df-mulg 18710  df-cntz 18932  df-cmn 19397  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-mopn 20602  df-fbas 20603  df-fg 20604  df-cnfld 20607  df-top 22052  df-topon 22069  df-topsp 22091  df-bases 22105  df-cld 22179  df-ntr 22180  df-cls 22181  df-nei 22258  df-lp 22296  df-perf 22297  df-cn 22387  df-cnp 22388  df-haus 22475  df-tx 22722  df-hmeo 22915  df-fil 23006  df-fm 23098  df-flim 23099  df-flf 23100  df-xms 23482  df-ms 23483  df-tms 23484  df-cncf 24050  df-limc 25039  df-dv 25040  df-log 25721  df-atan 26026

This theorem is referenced by:  atantanb  26083  atan1  26087