Theorem atantan 27233

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 26839	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘𝐴) ≠ 0)
2		atandmtan 27230	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ dom arctan)
3	1, 2	syldan 603	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ dom arctan)
4		atanval 27194	. . 3 ⊢ ((tan‘𝐴) ∈ dom arctan → (arctan‘(tan‘𝐴)) = ((i / 2) · ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴)))))))
5	3, 4	syl 18	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = ((i / 2) · ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴)))))))
6		ax-1cn 11239	. . . . . . 7 ⊢ 1 ∈ ℂ
7		ax-icn 11240	. . . . . . . 8 ⊢ i ∈ ℂ
8		tancl 16277	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ)
9	1, 8	syldan 603	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ ℂ)
10		mulcl 11265	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ (tan‘𝐴) ∈ ℂ) → (i · (tan‘𝐴)) ∈ ℂ)
11	7, 9, 10	sylancr 599	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) ∈ ℂ)
12		addcl 11263	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 + (i · (tan‘𝐴))) ∈ ℂ)
13	6, 11, 12	sylancr 599	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ∈ ℂ)
14		atandm2 27187	. . . . . . . 8 ⊢ ((tan‘𝐴) ∈ dom arctan ↔ ((tan‘𝐴) ∈ ℂ ∧ (1 − (i · (tan‘𝐴))) ≠ 0 ∧ (1 + (i · (tan‘𝐴))) ≠ 0))
15	3, 14	sylib 221	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((tan‘𝐴) ∈ ℂ ∧ (1 − (i · (tan‘𝐴))) ≠ 0 ∧ (1 + (i · (tan‘𝐴))) ≠ 0))
16	15	simp3d 1162	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ≠ 0)
17	13, 16	logcld 26880	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(1 + (i · (tan‘𝐴)))) ∈ ℂ)
18		subcl 11537	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 − (i · (tan‘𝐴))) ∈ ℂ)
19	6, 11, 18	sylancr 599	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ∈ ℂ)
20	15	simp2d 1161	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ≠ 0)
21	19, 20	logcld 26880	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(1 − (i · (tan‘𝐴)))) ∈ ℂ)
22	17, 21	negsubdi2d 11666	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴))))))
23		efsub 16248	. . . . . . . . 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 596	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴)))))) = ((exp‘(log‘(1 + (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i · (tan‘𝐴)))))))
25		coscl 16275	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
26	25	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
27		sincl 16274	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
28	27	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
29		mulcl 11265	. . . . . . . . . . . . 13 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
30	7, 28, 29	sylancr 599	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
31	26, 30, 26, 1	divdird 12112	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴))))
32	26, 1	dividd 12072	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘𝐴) / (cos‘𝐴)) = 1)
33	7	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → i ∈ ℂ)
34	33, 28, 26, 1	divassd 12109	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴))))
35		tanval 16276	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
36	1, 35	syldan 603	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
37	36	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴))))
38	34, 37	eqtr4d 2799	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · (tan‘𝐴)))
39	32, 38	oveq12d 7430	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 + (i · (tan‘𝐴))))
40	31, 39	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 + (i · (tan‘𝐴))))
41		efival 16300	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
42	41	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
43	42	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)))
44		eflog 26886	. . . . . . . . . . 11 ⊢ (((1 + (i · (tan‘𝐴))) ∈ ℂ ∧ (1 + (i · (tan‘𝐴))) ≠ 0) → (exp‘(log‘(1 + (i · (tan‘𝐴))))) = (1 + (i · (tan‘𝐴))))
45	13, 16, 44	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 + (i · (tan‘𝐴))))) = (1 + (i · (tan‘𝐴))))
46	40, 43, 45	3eqtr4d 2806	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 + (i · (tan‘𝐴))))))
47	26, 30, 26, 1	divsubdird 12113	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴))))
48	32, 38	oveq12d 7430	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 − (i · (tan‘𝐴))))
49	47, 48	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 − (i · (tan‘𝐴))))
50		negcl 11538	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
51	50	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ)
52		efival 16300	. . . . . . . . . . . . . 14 ⊢ (-𝐴 ∈ ℂ → (exp‘(i · -𝐴)) = ((cos‘-𝐴) + (i · (sin‘-𝐴))))
53	51, 52	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘-𝐴) + (i · (sin‘-𝐴))))
54		cosneg 16295	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴))
55	54	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘-𝐴) = (cos‘𝐴))
56		sinneg 16294	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴))
57	56	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (sin‘-𝐴) = -(sin‘𝐴))
58	57	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = (i · -(sin‘𝐴)))
59		mulneg2 11734	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · -(sin‘𝐴)) = -(i · (sin‘𝐴)))
60	7, 28, 59	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -(sin‘𝐴)) = -(i · (sin‘𝐴)))
61	58, 60	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = -(i · (sin‘𝐴)))
62	55, 61	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘-𝐴) + (i · (sin‘-𝐴))) = ((cos‘𝐴) + -(i · (sin‘𝐴))))
63	53, 62	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘𝐴) + -(i · (sin‘𝐴))))
64		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ)
65		mulneg2 11734	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · -𝐴) = -(i · 𝐴))
66	7, 64, 65	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -𝐴) = -(i · 𝐴))
67	66	fveq2d 6881	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = (exp‘-(i · 𝐴)))
68	26, 30	negsubd 11656	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((cos‘𝐴) + -(i · (sin‘𝐴))) = ((cos‘𝐴) − (i · (sin‘𝐴))))
69	63, 67, 68	3eqtr3d 2804	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴))))
70	69	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)))
71		eflog 26886	. . . . . . . . . . 11 ⊢ (((1 − (i · (tan‘𝐴))) ∈ ℂ ∧ (1 − (i · (tan‘𝐴))) ≠ 0) → (exp‘(log‘(1 − (i · (tan‘𝐴))))) = (1 − (i · (tan‘𝐴))))
72	19, 20, 71	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 − (i · (tan‘𝐴))))) = (1 − (i · (tan‘𝐴))))
73	49, 70, 72	3eqtr4d 2806	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 − (i · (tan‘𝐴))))))
74	46, 73	oveq12d 7430	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(log‘(1 + (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i · (tan‘𝐴)))))))
75		mulcl 11265	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
76	7, 64, 75	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ)
77		efcl 16228	. . . . . . . . . . 11 ⊢ ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
78	76, 77	syl 18	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ)
79	76	negcld 11637	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -(i · 𝐴) ∈ ℂ)
80		efcl 16228	. . . . . . . . . . 11 ⊢ (-(i · 𝐴) ∈ ℂ → (exp‘-(i · 𝐴)) ∈ ℂ)
81	79, 80	syl 18	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ∈ ℂ)
82		efne0 16244	. . . . . . . . . . 11 ⊢ (-(i · 𝐴) ∈ ℂ → (exp‘-(i · 𝐴)) ≠ 0)
83	79, 82	syl 18	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ≠ 0)
84	78, 81, 26, 83, 1	divcan7d 12102	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
85		efsub 16248	. . . . . . . . . 10 ⊢ (((i · 𝐴) ∈ ℂ ∧ -(i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
86	76, 79, 85	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i · 𝐴))))
87	76, 76	subnegd 11657	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
88	76	2timesd 12570	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
89	87, 88	eqtr4d 2799	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = (2 · (i · 𝐴)))
90	89	fveq2d 6881	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = (exp‘(2 · (i · 𝐴))))
91	84, 86, 90	3eqtr2d 2802	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = (exp‘(2 · (i · 𝐴))))
92	24, 74, 91	3eqtr2d 2802	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴)))))) = (exp‘(2 · (i · 𝐴))))
93	92	fveq2d 6881	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))) = (log‘(exp‘(2 · (i · 𝐴)))))
94	64	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 𝐴 ∈ ℂ)
95	94	renegd 15356	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) = -(ℜ‘𝐴))
96	94	recld 15341	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) ∈ ℝ)
97	96	renegcld 11724	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈ ℝ)
98		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) < 0)
99	96	lt0neg1d 11866	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((ℜ‘𝐴) < 0 ↔ 0 < -(ℜ‘𝐴)))
100	98, 99	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < -(ℜ‘𝐴))
101		eliooord 13517	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2)) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
102	101	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
103	102	simpld 500	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -(π / 2) < (ℜ‘𝐴))
104	103	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(π / 2) < (ℜ‘𝐴))
105		halfpire 26775	. . . . . . . . . . . . . . . . 17 ⊢ (π / 2) ∈ ℝ
106		ltnegcon1 11798	. . . . . . . . . . . . . . . . 17 ⊢ (((π / 2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (-(π / 2) < (ℜ‘𝐴) ↔ -(ℜ‘𝐴) < (π / 2)))
107	105, 96, 106	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (-(π / 2) < (ℜ‘𝐴) ↔ -(ℜ‘𝐴) < (π / 2)))
108	104, 107	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) < (π / 2))
109		0xr 11337	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ*
110	105	rexri 11348	. . . . . . . . . . . . . . . 16 ⊢ (π / 2) ∈ ℝ*
111		elioo2 13498	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ* ∧ (π / 2) ∈ ℝ*) → (-(ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 < -(ℜ‘𝐴) ∧ -(ℜ‘𝐴) < (π / 2))))
112	109, 110, 111	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (-(ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 < -(ℜ‘𝐴) ∧ -(ℜ‘𝐴) < (π / 2)))
113	97, 100, 108, 112	syl3anbrc 1362	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈ (0(,)(π / 2)))
114	95, 113	eqeltrd 2861	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) ∈ (0(,)(π / 2)))
115		tanregt0 26849	. . . . . . . . . . . . 13 ⊢ ((-𝐴 ∈ ℂ ∧ (ℜ‘-𝐴) ∈ (0(,)(π / 2))) → 0 < (ℜ‘(tan‘-𝐴)))
116	51, 114, 115	syl2an2r 698	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < (ℜ‘(tan‘-𝐴)))
117		tanneg 16296	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘-𝐴) = -(tan‘𝐴))
118	1, 117	syldan 603	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (tan‘-𝐴) = -(tan‘𝐴))
119	118	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘-𝐴) = -(tan‘𝐴))
120	119	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘-𝐴)) = (ℜ‘-(tan‘𝐴)))
121	9	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘𝐴) ∈ ℂ)
122	121	renegd 15356	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-(tan‘𝐴)) = -(ℜ‘(tan‘𝐴)))
123	120, 122	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘-𝐴)) = -(ℜ‘(tan‘𝐴)))
124	116, 123	breqtrd 5131	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < -(ℜ‘(tan‘𝐴)))
125	9	recld 15341	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘(tan‘𝐴)) ∈ ℝ)
126	125	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) ∈ ℝ)
127	126	lt0neg1d 11866	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((ℜ‘(tan‘𝐴)) < 0 ↔ 0 < -(ℜ‘(tan‘𝐴))))
128	124, 127	mpbird 260	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) < 0)
129	128	lt0ne0d 11862	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘(tan‘𝐴)) ≠ 0)
130		atanlogsub 27226	. . . . . . . . 9 ⊢ (((tan‘𝐴) ∈ dom arctan ∧ (ℜ‘(tan‘𝐴)) ≠ 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
131	3, 129, 130	syl2an2r 698	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
132		1re 11289	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
133		ioossre 13519	. . . . . . . . . . . . . 14 ⊢ (-1(,)1) ⊆ ℝ
134	7	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ∈ ℂ)
135	11	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ ℂ)
136		ine0 11732	. . . . . . . . . . . . . . . . 17 ⊢ i ≠ 0
137	136	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ≠ 0)
138		ixi 11926	. . . . . . . . . . . . . . . . . . 19 ⊢ (i · i) = -1
139	138	oveq1i 7422	. . . . . . . . . . . . . . . . . 18 ⊢ ((i · i) · (tan‘𝐴)) = (-1 · (tan‘𝐴))
140	9	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘𝐴) ∈ ℂ)
141	140	mulm1d 11749	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = -(tan‘𝐴))
142	118	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = -(tan‘𝐴))
143	141, 142	eqtr4d 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = (tan‘-𝐴))
144	139, 143	eqtrid 2808	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · (tan‘𝐴)) = (tan‘-𝐴))
145	134, 134, 140	mulassd 11313	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · (tan‘𝐴)) = (i · (i · (tan‘𝐴))))
146	138	oveq1i 7422	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((i · i) · 𝐴) = (-1 · 𝐴)
147	64	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 𝐴 ∈ ℂ)
148	147	mulm1d 11749	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · 𝐴) = -𝐴)
149	146, 148	eqtrid 2808	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = -𝐴)
150	134, 134, 147	mulassd 11313	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = (i · (i · 𝐴)))
151	149, 150	eqtr3d 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -𝐴 = (i · (i · 𝐴)))
152	151	fveq2d 6881	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = (tan‘(i · (i · 𝐴))))
153	144, 145, 152	3eqtr3d 2804	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (i · (tan‘𝐴))) = (tan‘(i · (i · 𝐴))))
154	134, 135, 137, 153	mvllmuld 12130	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) = ((tan‘(i · (i · 𝐴))) / i))
155	76	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℂ)
156		reim 15256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
157	156	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
158	157	eqeq1d 2763	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) = 0 ↔ (ℑ‘(i · 𝐴)) = 0))
159	158	biimpa 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (ℑ‘(i · 𝐴)) = 0)
160	155, 159	reim0bd 15347	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℝ)
161		tanhbnd 16309	. . . . . . . . . . . . . . . 16 ⊢ ((i · 𝐴) ∈ ℝ → ((tan‘(i · (i · 𝐴))) / i) ∈ (-1(,)1))
162	160, 161	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((tan‘(i · (i · 𝐴))) / i) ∈ (-1(,)1))
163	154, 162	eqeltrd 2861	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ (-1(,)1))
164	133, 163	sselid 3929	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈ ℝ)
165		readdcl 11264	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ (i · (tan‘𝐴)) ∈ ℝ) → (1 + (i · (tan‘𝐴))) ∈ ℝ)
166	132, 164, 165	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i · (tan‘𝐴))) ∈ ℝ)
167		df-neg 11525	. . . . . . . . . . . . . 14 ⊢ -1 = (0 − 1)
168		eliooord 13517	. . . . . . . . . . . . . . . 16 ⊢ ((i · (tan‘𝐴)) ∈ (-1(,)1) → (-1 < (i · (tan‘𝐴)) ∧ (i · (tan‘𝐴)) < 1))
169	163, 168	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 < (i · (tan‘𝐴)) ∧ (i · (tan‘𝐴)) < 1))
170	169	simpld 500	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -1 < (i · (tan‘𝐴)))
171	167, 170	eqbrtrrid 5141	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (0 − 1) < (i · (tan‘𝐴)))
172		0red 11292	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 ∈ ℝ)
173	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 1 ∈ ℝ)
174	172, 173, 164	ltsubadd2d 11895	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((0 − 1) < (i · (tan‘𝐴)) ↔ 0 < (1 + (i · (tan‘𝐴)))))
175	171, 174	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 < (1 + (i · (tan‘𝐴))))
176	166, 175	elrpd 13142	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i · (tan‘𝐴))) ∈ ℝ+)
177	176	relogcld 26933	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 + (i · (tan‘𝐴)))) ∈ ℝ)
178	169	simprd 501	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) < 1)
179		difrp 13141	. . . . . . . . . . . . 13 ⊢ (((i · (tan‘𝐴)) ∈ ℝ ∧ 1 ∈ ℝ) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i · (tan‘𝐴))) ∈ ℝ+))
180	164, 132, 179	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i · (tan‘𝐴))) ∈ ℝ+))
181	178, 180	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 − (i · (tan‘𝐴))) ∈ ℝ+)
182	181	relogcld 26933	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 − (i · (tan‘𝐴)))) ∈ ℝ)
183	177, 182	resubcld 11725	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ℝ)
184		relogrn 26871	. . . . . . . . 9 ⊢ (((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ℝ → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
185	183, 184	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
186	64	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 𝐴 ∈ ℂ)
187	186	recld 15341	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℝ)
188		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘𝐴))
189	102	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < (π / 2))
190	189	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) < (π / 2))
191		elioo2 13498	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ* ∧ (π / 2) ∈ ℝ*) → ((ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2))))
192	109, 110, 191	mp2an 705	. . . . . . . . . . . 12 ⊢ ((ℜ‘𝐴) ∈ (0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
193	187, 188, 190, 192	syl3anbrc 1362	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ (0(,)(π / 2)))
194		tanregt0 26849	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)(π / 2))) → 0 < (ℜ‘(tan‘𝐴)))
195	64, 193, 194	syl2an2r 698	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘(tan‘𝐴)))
196	195	gt0ne0d 11861	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(tan‘𝐴)) ≠ 0)
197	3, 196, 130	syl2an2r 698	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
198		recl 15257	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
199	198	adantr 486	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ)
200		0re 11291	. . . . . . . . 9 ⊢ 0 ∈ ℝ
201		lttri4 11375	. . . . . . . . 9 ⊢ (((ℜ‘𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 < (ℜ‘𝐴)))
202	199, 200, 201	sylancl 598	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 < (ℜ‘𝐴)))
203	131, 185, 197, 202	mpjao3dan 1459	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log)
204		logef 26891	. . . . . . 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 18	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))) = ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))))
206		2cn 12399	. . . . . . . . 9 ⊢ 2 ∈ ℂ
207		mulcl 11265	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · (i · 𝐴)) ∈ ℂ)
208	206, 76, 207	sylancr 599	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ℂ)
209		picn 26767	. . . . . . . . . . . 12 ⊢ π ∈ ℂ
210		2ne0 12430	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
211		divneg 11989	. . . . . . . . . . . 12 ⊢ ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = (-π / 2))
212	209, 206, 210, 211	mp3an 1490	. . . . . . . . . . 11 ⊢ -(π / 2) = (-π / 2)
213	212, 103	eqbrtrrid 5141	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-π / 2) < (ℜ‘𝐴))
214		pire 26765	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ
215	214	renegcli 11600	. . . . . . . . . . . 12 ⊢ -π ∈ ℝ
216	215	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π ∈ ℝ)
217		2re 12398	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
218	217	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 2 ∈ ℝ)
219		2pos 12428	. . . . . . . . . . . 12 ⊢ 0 < 2
220	219	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 0 < 2)
221		ltdivmul 12173	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 · (ℜ‘𝐴))))
222	216, 199, 218, 220, 221	syl112anc 1401	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 · (ℜ‘𝐴))))
223	213, 222	mpbid 235	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π < (2 · (ℜ‘𝐴)))
224		immul2 15284	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℑ‘(i · 𝐴))))
225	217, 76, 224	sylancr 599	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℑ‘(i · 𝐴))))
226	157	oveq2d 7428	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) = (2 · (ℑ‘(i · 𝐴))))
227	225, 226	eqtr4d 2799	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 · (ℜ‘𝐴)))
228	223, 227	breqtrrd 5133	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -π < (ℑ‘(2 · (i · 𝐴))))
229		remulcl 11266	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (2 · (ℜ‘𝐴)) ∈ ℝ)
230	217, 199, 229	sylancr 599	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ∈ ℝ)
231	214	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → π ∈ ℝ)
232		ltmuldiv2 12172	. . . . . . . . . . . 12 ⊢ (((ℜ‘𝐴) ∈ ℝ ∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π / 2)))
233	199, 231, 218, 220, 232	syl112anc 1401	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π / 2)))
234	189, 233	mpbird 260	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) < π)
235	230, 231, 234	ltled 11439	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ≤ π)
236	227, 235	eqbrtrd 5127	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) ≤ π)
237		ellogrn 26869	. . . . . . . 8 ⊢ ((2 · (i · 𝐴)) ∈ ran log ↔ ((2 · (i · 𝐴)) ∈ ℂ ∧ -π < (ℑ‘(2 · (i · 𝐴))) ∧ (ℑ‘(2 · (i · 𝐴))) ≤ π))
238	208, 228, 236, 237	syl3anbrc 1362	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ran log)
239		logef 26891	. . . . . . 7 ⊢ ((2 · (i · 𝐴)) ∈ ran log → (log‘(exp‘(2 · (i · 𝐴)))) = (2 · (i · 𝐴)))
240	238, 239	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (log‘(exp‘(2 · (i · 𝐴)))) = (2 · (i · 𝐴)))
241	93, 205, 240	3eqtr3d 2804	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = (2 · (i · 𝐴)))
242	241	negeqd 11532	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → -((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i · (tan‘𝐴))))) = -(2 · (i · 𝐴)))
243	22, 242	eqtr3d 2798	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴))))) = -(2 · (i · 𝐴)))
244	243	oveq2d 7428	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · ((log‘(1 − (i · (tan‘𝐴)))) − (log‘(1 + (i · (tan‘𝐴)))))) = ((i / 2) · -(2 · (i · 𝐴))))
245		halfcl 12553	. . . . 5 ⊢ (i ∈ ℂ → (i / 2) ∈ ℂ)
246	7, 245	mp1i 14	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i / 2) ∈ ℂ)
247	206	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 2 ∈ ℂ)
248	246, 247, 79	mulassd 11313	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i · 𝐴)) = ((i / 2) · (2 · -(i · 𝐴))))
249	7, 206, 210	divcan1i 12042	. . . . 5 ⊢ ((i / 2) · 2) = i
250	249	oveq1i 7422	. . . 4 ⊢ (((i / 2) · 2) · -(i · 𝐴)) = (i · -(i · 𝐴))
251	33, 33, 51	mulassd 11313	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = (i · (i · -𝐴)))
252	138	oveq1i 7422	. . . . . 6 ⊢ ((i · i) · -𝐴) = (-1 · -𝐴)
253		mul2neg 11736	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (-1 · -𝐴) = (1 · 𝐴))
254	6, 64, 253	sylancr 599	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = (1 · 𝐴))
255		mullid 11288	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
256	255	adantr 486	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴)
257	254, 256	eqtrd 2796	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = 𝐴)
258	252, 257	eqtrid 2808	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = 𝐴)
259	66	oveq2d 7428	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · (i · -𝐴)) = (i · -(i · 𝐴)))
260	251, 258, 259	3eqtr3rd 2805	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (i · -(i · 𝐴)) = 𝐴)
261	250, 260	eqtrid 2808	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i · 𝐴)) = 𝐴)
262		mulneg2 11734	. . . . 5 ⊢ ((2 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · -(i · 𝐴)) = -(2 · (i · 𝐴)))
263	206, 76, 262	sylancr 599	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (2 · -(i · 𝐴)) = -(2 · (i · 𝐴)))
264	263	oveq2d 7428	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · (2 · -(i · 𝐴))) = ((i / 2) · -(2 · (i · 𝐴))))
265	248, 261, 264	3eqtr3rd 2805	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → ((i / 2) · -(2 · (i · 𝐴))) = 𝐴)
266	5, 244, 265	3eqtrd 2800	1 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956   class class class wbr 5103  dom cdm 5651  ran crn 5652  ‘cfv 6531  (class class class)co 7412  ℂcc 11179  ℝcr 11180  0cc0 11181  1c1 11182  ici 11183   + caddc 11184   · cmul 11186  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325   − cmin 11522  -cneg 11523   / cdiv 11954  2c2 12378  ℝ⁺crp 13101  (,)cioo 13457  ℜcre 15244  ℑcim 15245  expce 16207  sincsin 16209  cosccos 16210  tanctan 16211  πcpi 16212  logclog 26864  arctancatan 27174

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 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-inf2 9626  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258  ax-pre-sup 11259  ax-addf 11260

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7682  df-om 7867  df-1st 7990  df-2nd 7991  df-supp 8162  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-2o 8461  df-er 8701  df-map 8833  df-pm 8834  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9338  df-fi 9387  df-sup 9418  df-inf 9419  df-oi 9488  df-card 10001  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-div 11955  df-nn 12317  df-2 12386  df-3 12387  df-4 12388  df-5 12389  df-6 12390  df-7 12391  df-8 12392  df-9 12393  df-n0 12588  df-z 12675  df-dec 12796  df-uz 12947  df-q 13057  df-rp 13102  df-xneg 13222  df-xadd 13223  df-xmul 13224  df-ioo 13461  df-ioc 13462  df-ico 13463  df-icc 13464  df-fz 13621  df-fzo 13769  df-fl 13912  df-mod 13990  df-seq 14125  df-exp 14185  df-fac 14398  df-bc 14427  df-hash 14455  df-shft 15200  df-cj 15246  df-re 15247  df-im 15248  df-sqrt 15382  df-abs 15383  df-limsup 15618  df-clim 15635  df-rlim 15636  df-sum 15834  df-ef 16213  df-sin 16215  df-cos 16216  df-tan 16217  df-pi 16218  df-struct 17305  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-ress 17389  df-plusg 17421  df-mulr 17422  df-starv 17423  df-sca 17424  df-vsca 17425  df-ip 17426  df-tset 17427  df-ple 17428  df-ds 17430  df-unif 17431  df-hom 17432  df-cco 17433  df-rest 17573  df-topn 17574  df-0g 17592  df-gsum 17593  df-topgen 17594  df-pt 17595  df-prds 17598  df-xrs 17654  df-qtop 17659  df-imas 17660  df-xps 17662  df-mre 17736  df-mrc 17737  df-acs 17739  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-submnd 18959  df-mulg 19258  df-cntz 19511  df-cmn 19976  df-psmet 21650  df-xmet 21651  df-met 21652  df-bl 21653  df-mopn 21654  df-fbas 21655  df-fg 21656  df-cnfld 21659  df-top 23192  df-topon 23209  df-topsp 23231  df-bases 23244  df-cld 23317  df-ntr 23318  df-cls 23319  df-nei 23396  df-lp 23434  df-perf 23435  df-cn 23525  df-cnp 23526  df-haus 23613  df-tx 23861  df-hmeo 24054  df-fil 24145  df-fm 24237  df-flim 24238  df-flf 24239  df-xms 24619  df-ms 24620  df-tms 24621  df-cncf 25179  df-limc 26166  df-dv 26167  df-log 26866  df-atan 27177

This theorem is used by:  atantanb  27234  atan1  27238