Theorem atantan 26951

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 26556	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘𝐴) ≠ 0)
2		atandmtan 26948	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ dom arctan)
3	1, 2	syldan 589	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ dom arctan)
4		atanval 26912	. . 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 11216	. . . . . . 7 ⊢ 1 ∈ ℂ
7		ax-icn 11217	. . . . . . . 8 ⊢ i ∈ ℂ
8		tancl 16131	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ)
9	1, 8	syldan 589	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ ℂ)
10		mulcl 11242	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ (tan‘𝐴) ∈ ℂ) → (i · (tan‘𝐴)) ∈ ℂ)
11	7, 9, 10	sylancr 585	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) ∈ ℂ)
12		addcl 11240	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 + (i · (tan‘𝐴))) ∈ ℂ)
13	6, 11, 12	sylancr 585	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ∈ ℂ)
14		atandm2 26905	. . . . . . . 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 1141	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ≠ 0)
17	13, 16	logcld 26597	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(1 + (i · (tan‘𝐴)))) ∈ ℂ)
18		subcl 11509	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 − (i · (tan‘𝐴))) ∈ ℂ)
19	6, 11, 18	sylancr 585	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ∈ ℂ)
20	15	simp2d 1140	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ≠ 0)
21	19, 20	logcld 26597	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(1 − (i · (tan‘𝐴)))) ∈ ℂ)
22	17, 21	negsubdi2d 11637	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴))))))
23		efsub 16102	. . . . . . . . 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 582	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴)))))) = ((exp‘(log‘(1 + (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i · (tan‘𝐴)))))))
25		coscl 16129	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
26	25	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
27		sincl 16128	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
28	27	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
29		mulcl 11242	. . . . . . . . . . . . 13 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
30	7, 28, 29	sylancr 585	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
31	26, 30, 26, 1	divdird 12079	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴))))
32	26, 1	dividd 12039	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘𝐴) / (cos‘𝐴)) = 1)
33	7	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → i ∈ ℂ)
34	33, 28, 26, 1	divassd 12076	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴))))
35		tanval 16130	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
36	1, 35	syldan 589	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
37	36	oveq2d 7440	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴))))
38	34, 37	eqtr4d 2769	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · (tan‘𝐴)))
39	32, 38	oveq12d 7442	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 + (i · (tan‘𝐴))))
40	31, 39	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 + (i · (tan‘𝐴))))
41		efival 16154	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
42	41	adantr 479	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
43	42	oveq1d 7439	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)))
44		eflog 26603	. . . . . . . . . . 11 ⊢ (((1 + (i · (tan‘𝐴))) ∈ ℂ ∧ (1 + (i · (tan‘𝐴))) ≠ 0) → (exp‘(log‘(1 + (i · (tan‘𝐴))))) = (1 + (i · (tan‘𝐴))))
45	13, 16, 44	syl2anc 582	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 + (i · (tan‘𝐴))))) = (1 + (i · (tan‘𝐴))))
46	40, 43, 45	3eqtr4d 2776	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 + (i · (tan‘𝐴))))))
47	26, 30, 26, 1	divsubdird 12080	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴))))
48	32, 38	oveq12d 7442	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 − (i · (tan‘𝐴))))
49	47, 48	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 − (i · (tan‘𝐴))))
50		negcl 11510	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
51	50	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ)
52		efival 16154	. . . . . . . . . . . . . 14 ⊢ (-𝐴 ∈ ℂ → (exp‘(i · -𝐴)) = ((cos‘-𝐴) + (i · (sin‘-𝐴))))
53	51, 52	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘-𝐴) + (i · (sin‘-𝐴))))
54		cosneg 16149	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴))
55	54	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘-𝐴) = (cos‘𝐴))
56		sinneg 16148	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴))
57	56	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (sin‘-𝐴) = -(sin‘𝐴))
58	57	oveq2d 7440	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = (i · -(sin‘𝐴)))
59		mulneg2 11701	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · -(sin‘𝐴)) = -(i · (sin‘𝐴)))
60	7, 28, 59	sylancr 585	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -(sin‘𝐴)) = -(i · (sin‘𝐴)))
61	58, 60	eqtrd 2766	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = -(i · (sin‘𝐴)))
62	55, 61	oveq12d 7442	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘-𝐴) + (i · (sin‘-𝐴))) = ((cos‘𝐴) + -(i · (sin‘𝐴))))
63	53, 62	eqtrd 2766	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘𝐴) + -(i · (sin‘𝐴))))
64		simpl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ)
65		mulneg2 11701	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · -𝐴) = -(i · 𝐴))
66	7, 64, 65	sylancr 585	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -𝐴) = -(i · 𝐴))
67	66	fveq2d 6905	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = (exp‘-(i · 𝐴)))
68	26, 30	negsubd 11627	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘𝐴) + -(i · (sin‘𝐴))) = ((cos‘𝐴) − (i · (sin‘𝐴))))
69	63, 67, 68	3eqtr3d 2774	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴))))
70	69	oveq1d 7439	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)))
71		eflog 26603	. . . . . . . . . . 11 ⊢ (((1 − (i · (tan‘𝐴))) ∈ ℂ ∧ (1 − (i · (tan‘𝐴))) ≠ 0) → (exp‘(log‘(1 − (i · (tan‘𝐴))))) = (1 − (i · (tan‘𝐴))))
72	19, 20, 71	syl2anc 582	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 − (i · (tan‘𝐴))))) = (1 − (i · (tan‘𝐴))))
73	49, 70, 72	3eqtr4d 2776	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 − (i · (tan‘𝐴))))))
74	46, 73	oveq12d 7442	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(log‘(1 + (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i · (tan‘𝐴)))))))
75		mulcl 11242	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
76	7, 64, 75	sylancr 585	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ)
77		efcl 16084	. . . . . . . . . . 11 ⊢ ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
78	76, 77	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ)
79	76	negcld 11608	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -(i · 𝐴) ∈ ℂ)
80		efcl 16084	. . . . . . . . . . 11 ⊢ (-(i · 𝐴) ∈ ℂ → (exp‘-(i · 𝐴)) ∈ ℂ)
81	79, 80	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ∈ ℂ)
82		efne0 16099	. . . . . . . . . . 11 ⊢ (-(i · 𝐴) ∈ ℂ → (exp‘-(i · 𝐴)) ≠ 0)
83	79, 82	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ≠ 0)
84	78, 81, 26, 83, 1	divcan7d 12069	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
85		efsub 16102	. . . . . . . . . 10 ⊢ (((i · 𝐴) ∈ ℂ ∧ -(i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
86	76, 79, 85	syl2anc 582	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
87	76, 76	subnegd 11628	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
88	76	2timesd 12507	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
89	87, 88	eqtr4d 2769	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = (2 · (i · 𝐴)))
90	89	fveq2d 6905	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = (exp‘(2 · (i · 𝐴))))
91	84, 86, 90	3eqtr2d 2772	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = (exp‘(2 · (i · 𝐴))))
92	24, 74, 91	3eqtr2d 2772	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴)))))) = (exp‘(2 · (i · 𝐴))))
93	92	fveq2d 6905	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))) = (log‘(exp‘(2 · (i · 𝐴)))))
94	64	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 𝐴 ∈ ℂ)
95	94	renegd 15214	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) = -(ℜ‘𝐴))
96	94	recld 15199	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) ∈ ℝ)
97	96	renegcld 11691	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈ ℝ)
98		simpr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) < 0)
99	96	lt0neg1d 11833	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((ℜ‘𝐴) < 0 ↔ 0 < -(ℜ‘𝐴)))
100	98, 99	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < -(ℜ‘𝐴))
101		eliooord 13437	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2)) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
102	101	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
103	102	simpld 493	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -(π / 2) < (ℜ‘𝐴))
104	103	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(π / 2) < (ℜ‘𝐴))
105		halfpire 26492	. . . . . . . . . . . . . . . . 17 ⊢ (π / 2) ∈ ℝ
106		ltnegcon1 11765	. . . . . . . . . . . . . . . . 17 ⊢ (((π / 2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (-(π / 2) < (ℜ‘𝐴) ↔ -(ℜ‘𝐴) < (π / 2)))
107	105, 96, 106	sylancr 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (-(π / 2) < (ℜ‘𝐴) ↔ -(ℜ‘𝐴) < (π / 2)))
108	104, 107	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) < (π / 2))
109		0xr 11311	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ*
110	105	rexri 11322	. . . . . . . . . . . . . . . 16 ⊢ (π / 2) ∈ ℝ*
111		elioo2 13419	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ* ∧ (π / 2) ∈ ℝ*) → (-(ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 < -(ℜ‘𝐴) ∧ -(ℜ‘𝐴) < (π / 2))))
112	109, 110, 111	mp2an 690	. . . . . . . . . . . . . . 15 ⊢ (-(ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 < -(ℜ‘𝐴) ∧ -(ℜ‘𝐴) < (π / 2)))
113	97, 100, 108, 112	syl3anbrc 1340	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈ (0(,)(π / 2)))
114	95, 113	eqeltrd 2826	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) ∈ (0(,)(π / 2)))
115		tanregt0 26566	. . . . . . . . . . . . 13 ⊢ ((-𝐴 ∈ ℂ ∧ (ℜ‘-𝐴) ∈ (0(,)(π / 2))) → 0 < (ℜ‘(tan‘-𝐴)))
116	51, 114, 115	syl2an2r 683	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < (ℜ‘(tan‘-𝐴)))
117		tanneg 16150	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘-𝐴) = -(tan‘𝐴))
118	1, 117	syldan 589	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘-𝐴) = -(tan‘𝐴))
119	118	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘-𝐴) = -(tan‘𝐴))
120	119	fveq2d 6905	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘-𝐴)) = (ℜ‘-(tan‘𝐴)))
121	9	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘𝐴) ∈ ℂ)
122	121	renegd 15214	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-(tan‘𝐴)) = -(ℜ‘(tan‘𝐴)))
123	120, 122	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘-𝐴)) = -(ℜ‘(tan‘𝐴)))
124	116, 123	breqtrd 5179	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < -(ℜ‘(tan‘𝐴)))
125	9	recld 15199	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘(tan‘𝐴)) ∈ ℝ)
126	125	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) ∈ ℝ)
127	126	lt0neg1d 11833	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((ℜ‘(tan‘𝐴)) < 0 ↔ 0 < -(ℜ‘(tan‘𝐴))))
128	124, 127	mpbird 256	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) < 0)
129	128	lt0ne0d 11829	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) ≠ 0)
130		atanlogsub 26944	. . . . . . . . 9 ⊢ (((tan‘𝐴) ∈ dom arctan ∧ (ℜ‘(tan‘𝐴)) ≠ 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
131	3, 129, 130	syl2an2r 683	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
132		1re 11264	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
133		ioossre 13439	. . . . . . . . . . . . . 14 ⊢ (-1(,)1) ⊆ ℝ
134	7	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ∈ ℂ)
135	11	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ ℂ)
136		ine0 11699	. . . . . . . . . . . . . . . . 17 ⊢ i ≠ 0
137	136	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ≠ 0)
138		ixi 11893	. . . . . . . . . . . . . . . . . . 19 ⊢ (i · i) = -1
139	138	oveq1i 7434	. . . . . . . . . . . . . . . . . 18 ⊢ ((i · i) · (tan‘𝐴)) = (-1 · (tan‘𝐴))
140	9	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘𝐴) ∈ ℂ)
141	140	mulm1d 11716	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = -(tan‘𝐴))
142	118	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = -(tan‘𝐴))
143	141, 142	eqtr4d 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = (tan‘-𝐴))
144	139, 143	eqtrid 2778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · (tan‘𝐴)) = (tan‘-𝐴))
145	134, 134, 140	mulassd 11287	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · (tan‘𝐴)) = (i · (i · (tan‘𝐴))))
146	138	oveq1i 7434	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((i · i) · 𝐴) = (-1 · 𝐴)
147	64	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 𝐴 ∈ ℂ)
148	147	mulm1d 11716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · 𝐴) = -𝐴)
149	146, 148	eqtrid 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = -𝐴)
150	134, 134, 147	mulassd 11287	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = (i · (i · 𝐴)))
151	149, 150	eqtr3d 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -𝐴 = (i · (i · 𝐴)))
152	151	fveq2d 6905	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = (tan‘(i · (i · 𝐴))))
153	144, 145, 152	3eqtr3d 2774	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (i · (tan‘𝐴))) = (tan‘(i · (i · 𝐴))))
154	134, 135, 137, 153	mvllmuld 12097	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) = ((tan‘(i · (i · 𝐴))) / i))
155	76	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℂ)
156		reim 15114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
157	156	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
158	157	eqeq1d 2728	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) = 0 ↔ (ℑ‘(i · 𝐴)) = 0))
159	158	biimpa 475	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (ℑ‘(i · 𝐴)) = 0)
160	155, 159	reim0bd 15205	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℝ)
161		tanhbnd 16163	. . . . . . . . . . . . . . . 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 2826	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ (-1(,)1))
164	133, 163	sselid 3977	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ ℝ)
165		readdcl 11241	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ (i · (tan‘𝐴)) ∈ ℝ) → (1 + (i · (tan‘𝐴))) ∈ ℝ)
166	132, 164, 165	sylancr 585	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i · (tan‘𝐴))) ∈ ℝ)
167		df-neg 11497	. . . . . . . . . . . . . 14 ⊢ -1 = (0 − 1)
168		eliooord 13437	. . . . . . . . . . . . . . . 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 493	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -1 < (i · (tan‘𝐴)))
171	167, 170	eqbrtrrid 5189	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (0 − 1) < (i · (tan‘𝐴)))
172		0red 11267	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 ∈ ℝ)
173	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 1 ∈ ℝ)
174	172, 173, 164	ltsubadd2d 11862	. . . . . . . . . . . . 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 13067	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i · (tan‘𝐴))) ∈ ℝ+)
177	176	relogcld 26650	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 + (i · (tan‘𝐴)))) ∈ ℝ)
178	169	simprd 494	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) < 1)
179		difrp 13066	. . . . . . . . . . . . 13 ⊢ (((i · (tan‘𝐴)) ∈ ℝ ∧ 1 ∈ ℝ) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i · (tan‘𝐴))) ∈ ℝ+))
180	164, 132, 179	sylancl 584	. . . . . . . . . . . 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 26650	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 − (i · (tan‘𝐴)))) ∈ ℝ)
183	177, 182	resubcld 11692	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ℝ)
184		relogrn 26588	. . . . . . . . 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 479	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 𝐴 ∈ ℂ)
187	186	recld 15199	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℝ)
188		simpr 483	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘𝐴))
189	102	simprd 494	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < (π / 2))
190	189	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) < (π / 2))
191		elioo2 13419	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ* ∧ (π / 2) ∈ ℝ*) → ((ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2))))
192	109, 110, 191	mp2an 690	. . . . . . . . . . . 12 ⊢ ((ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
193	187, 188, 190, 192	syl3anbrc 1340	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ (0(,)(π / 2)))
194		tanregt0 26566	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)(π / 2))) → 0 < (ℜ‘(tan‘𝐴)))
195	64, 193, 194	syl2an2r 683	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘(tan‘𝐴)))
196	195	gt0ne0d 11828	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(tan‘𝐴)) ≠ 0)
197	3, 196, 130	syl2an2r 683	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
198		recl 15115	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
199	198	adantr 479	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ)
200		0re 11266	. . . . . . . . 9 ⊢ 0 ∈ ℝ
201		lttri4 11348	. . . . . . . . 9 ⊢ (((ℜ‘𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 < (ℜ‘𝐴)))
202	199, 200, 201	sylancl 584	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 < (ℜ‘𝐴)))
203	131, 185, 197, 202	mpjao3dan 1429	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
204		logef 26608	. . . . . . 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 12339	. . . . . . . . 9 ⊢ 2 ∈ ℂ
207		mulcl 11242	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · (i · 𝐴)) ∈ ℂ)
208	206, 76, 207	sylancr 585	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ℂ)
209		picn 26487	. . . . . . . . . . . 12 ⊢ π ∈ ℂ
210		2ne0 12368	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
211		divneg 11957	. . . . . . . . . . . 12 ⊢ ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = (-π / 2))
212	209, 206, 210, 211	mp3an 1458	. . . . . . . . . . 11 ⊢ -(π / 2) = (-π / 2)
213	212, 103	eqbrtrrid 5189	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-π / 2) < (ℜ‘𝐴))
214		pire 26486	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ
215	214	renegcli 11571	. . . . . . . . . . . 12 ⊢ -π ∈ ℝ
216	215	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π ∈ ℝ)
217		2re 12338	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
218	217	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 2 ∈ ℝ)
219		2pos 12367	. . . . . . . . . . . 12 ⊢ 0 < 2
220	219	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 0 < 2)
221		ltdivmul 12141	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 · (ℜ‘𝐴))))
222	216, 199, 218, 220, 221	syl112anc 1371	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 · (ℜ‘𝐴))))
223	213, 222	mpbid 231	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π < (2 · (ℜ‘𝐴)))
224		immul2 15142	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℑ‘(i · 𝐴))))
225	217, 76, 224	sylancr 585	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℑ‘(i · 𝐴))))
226	157	oveq2d 7440	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) = (2 · (ℑ‘(i · 𝐴))))
227	225, 226	eqtr4d 2769	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℜ‘𝐴)))
228	223, 227	breqtrrd 5181	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π < (ℑ‘(2 · (i · 𝐴))))
229		remulcl 11243	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (2 · (ℜ‘𝐴)) ∈ ℝ)
230	217, 199, 229	sylancr 585	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ∈ ℝ)
231	214	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → π ∈ ℝ)
232		ltmuldiv2 12140	. . . . . . . . . . . 12 ⊢ (((ℜ‘𝐴) ∈ ℝ ∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π / 2)))
233	199, 231, 218, 220, 232	syl112anc 1371	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π / 2)))
234	189, 233	mpbird 256	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) < π)
235	230, 231, 234	ltled 11412	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ≤ π)
236	227, 235	eqbrtrd 5175	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) ≤ π)
237		ellogrn 26586	. . . . . . . 8 ⊢ ((2 · (i · 𝐴)) ∈ ran log ↔ ((2 · (i · 𝐴)) ∈ ℂ ∧ -π < (ℑ‘(2 · (i · 𝐴))) ∧ (ℑ‘(2 · (i · 𝐴))) ≤ π))
238	208, 228, 236, 237	syl3anbrc 1340	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ran log)
239		logef 26608	. . . . . . 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 2774	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = (2 · (i · 𝐴)))
242	241	negeqd 11504	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = -(2 · (i · 𝐴)))
243	22, 242	eqtr3d 2768	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴))))) = -(2 · (i · 𝐴)))
244	243	oveq2d 7440	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴)))))) = ((i / 2) · -(2 · (i · 𝐴))))
245		halfcl 12489	. . . . 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 11287	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i · 𝐴)) = ((i / 2) · (2 · -(i · 𝐴))))
249	7, 206, 210	divcan1i 12009	. . . . 5 ⊢ ((i / 2) · 2) = i
250	249	oveq1i 7434	. . . 4 ⊢ (((i / 2) · 2) · -(i · 𝐴)) = (i · -(i · 𝐴))
251	33, 33, 51	mulassd 11287	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = (i · (i · -𝐴)))
252	138	oveq1i 7434	. . . . . 6 ⊢ ((i · i) · -𝐴) = (-1 · -𝐴)
253		mul2neg 11703	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (-1 · -𝐴) = (1 · 𝐴))
254	6, 64, 253	sylancr 585	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = (1 · 𝐴))
255		mullid 11263	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
256	255	adantr 479	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴)
257	254, 256	eqtrd 2766	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = 𝐴)
258	252, 257	eqtrid 2778	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = 𝐴)
259	66	oveq2d 7440	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (i · -𝐴)) = (i · -(i · 𝐴)))
260	251, 258, 259	3eqtr3rd 2775	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -(i · 𝐴)) = 𝐴)
261	250, 260	eqtrid 2778	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i · 𝐴)) = 𝐴)
262		mulneg2 11701	. . . . 5 ⊢ ((2 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · -(i · 𝐴)) = -(2 · (i · 𝐴)))
263	206, 76, 262	sylancr 585	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · -(i · 𝐴)) = -(2 · (i · 𝐴)))
264	263	oveq2d 7440	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · (2 · -(i · 𝐴))) = ((i / 2) · -(2 · (i · 𝐴))))
265	248, 261, 264	3eqtr3rd 2775	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · -(2 · (i · 𝐴))) = 𝐴)
266	5, 244, 265	3eqtrd 2770	1 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ w3o 1083   ∧ w3a 1084   = wceq 1534   ∈ wcel 2099   ≠ wne 2930   class class class wbr 5153  dom cdm 5682  ran crn 5683  ‘cfv 6554  (class class class)co 7424  ℂcc 11156  ℝcr 11157  0cc0 11158  1c1 11159  ici 11160   + caddc 11161   · cmul 11163  ℝ^*cxr 11297   < clt 11298   ≤ cle 11299   − cmin 11494  -cneg 11495   / cdiv 11921  2c2 12319  ℝ⁺crp 13028  (,)cioo 13378  ℜcre 15102  ℑcim 15103  expce 16063  sincsin 16065  cosccos 16066  tanctan 16067  πcpi 16068  logclog 26581  arctancatan 26892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236  ax-addf 11237

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-tp 4638  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-om 7877  df-1st 8003  df-2nd 8004  df-supp 8175  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-er 8734  df-map 8857  df-pm 8858  df-ixp 8927  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fsupp 9406  df-fi 9454  df-sup 9485  df-inf 9486  df-oi 9553  df-card 9982  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12611  df-dec 12730  df-uz 12875  df-q 12985  df-rp 13029  df-xneg 13146  df-xadd 13147  df-xmul 13148  df-ioo 13382  df-ioc 13383  df-ico 13384  df-icc 13385  df-fz 13539  df-fzo 13682  df-fl 13812  df-mod 13890  df-seq 14022  df-exp 14082  df-fac 14291  df-bc 14320  df-hash 14348  df-shft 15072  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-limsup 15473  df-clim 15490  df-rlim 15491  df-sum 15691  df-ef 16069  df-sin 16071  df-cos 16072  df-tan 16073  df-pi 16074  df-struct 17149  df-sets 17166  df-slot 17184  df-ndx 17196  df-base 17214  df-ress 17243  df-plusg 17279  df-mulr 17280  df-starv 17281  df-sca 17282  df-vsca 17283  df-ip 17284  df-tset 17285  df-ple 17286  df-ds 17288  df-unif 17289  df-hom 17290  df-cco 17291  df-rest 17437  df-topn 17438  df-0g 17456  df-gsum 17457  df-topgen 17458  df-pt 17459  df-prds 17462  df-xrs 17517  df-qtop 17522  df-imas 17523  df-xps 17525  df-mre 17599  df-mrc 17600  df-acs 17602  df-mgm 18633  df-sgrp 18712  df-mnd 18728  df-submnd 18774  df-mulg 19062  df-cntz 19311  df-cmn 19780  df-psmet 21335  df-xmet 21336  df-met 21337  df-bl 21338  df-mopn 21339  df-fbas 21340  df-fg 21341  df-cnfld 21344  df-top 22887  df-topon 22904  df-topsp 22926  df-bases 22940  df-cld 23014  df-ntr 23015  df-cls 23016  df-nei 23093  df-lp 23131  df-perf 23132  df-cn 23222  df-cnp 23223  df-haus 23310  df-tx 23557  df-hmeo 23750  df-fil 23841  df-fm 23933  df-flim 23934  df-flf 23935  df-xms 24317  df-ms 24318  df-tms 24319  df-cncf 24889  df-limc 25886  df-dv 25887  df-log 26583  df-atan 26895

This theorem is referenced by:  atantanb  26952  atan1  26956