atancj - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > atancj		Structured version Visualization version GIF version

Theorem atancj 26963

Description: The arctangent function distributes under conjugation. (The condition that ℜ(𝐴) ≠ 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg 26960 true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -1 and 1, though.) (Contributed by Mario Carneiro, 31-Mar-2015.)

**Assertion**
Ref	Expression
atancj	⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (𝐴 ∈ dom arctan ∧ (∗‘(arctan‘𝐴)) = (arctan‘(∗‘𝐴))))

**Proof of Theorem atancj**
Step	Hyp	Ref	Expression
1		simpl 486	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → 𝐴 ∈ ℂ)
2		simpr 488	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℜ‘𝐴) ≠ 0)
3		fveq2 6862	. . . . . 6 ⊢ (𝐴 = -i → (ℜ‘𝐴) = (ℜ‘-i))
4		ax-icn 11126	. . . . . . . 8 ⊢ i ∈ ℂ
5	4	renegi 15198	. . . . . . 7 ⊢ (ℜ‘-i) = -(ℜ‘i)
6		rei 15174	. . . . . . . 8 ⊢ (ℜ‘i) = 0
7	6	negeqi 11417	. . . . . . 7 ⊢ -(ℜ‘i) = -0
8		neg0 11471	. . . . . . 7 ⊢ -0 = 0
9	5, 7, 8	3eqtri 2788	. . . . . 6 ⊢ (ℜ‘-i) = 0
10	3, 9	eqtrdi 2812	. . . . 5 ⊢ (𝐴 = -i → (ℜ‘𝐴) = 0)
11	10	necon3i 2988	. . . 4 ⊢ ((ℜ‘𝐴) ≠ 0 → 𝐴 ≠ -i)
12	2, 11	syl 17	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → 𝐴 ≠ -i)
13		fveq2 6862	. . . . . 6 ⊢ (𝐴 = i → (ℜ‘𝐴) = (ℜ‘i))
14	13, 6	eqtrdi 2812	. . . . 5 ⊢ (𝐴 = i → (ℜ‘𝐴) = 0)
15	14	necon3i 2988	. . . 4 ⊢ ((ℜ‘𝐴) ≠ 0 → 𝐴 ≠ i)
16	2, 15	syl 17	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → 𝐴 ≠ i)
17		atandm 26929	. . 3 ⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i))
18	1, 12, 16, 17	syl3anbrc 1356	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → 𝐴 ∈ dom arctan)
19		halfcl 12441	. . . . . 6 ⊢ (i ∈ ℂ → (i / 2) ∈ ℂ)
20	4, 19	ax-mp 5	. . . . 5 ⊢ (i / 2) ∈ ℂ
21		ax-1cn 11125	. . . . . . . 8 ⊢ 1 ∈ ℂ
22		mulcl 11151	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
23	4, 1, 22	sylancr 596	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (i · 𝐴) ∈ ℂ)
24		subcl 11423	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i · 𝐴)) ∈ ℂ)
25	21, 23, 24	sylancr 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 − (i · 𝐴)) ∈ ℂ)
26		atandm2 26930	. . . . . . . . 9 ⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0))
27	18, 26	sylib 220	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0))
28	27	simp2d 1155	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 − (i · 𝐴)) ≠ 0)
29	25, 28	logcld 26623	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (log‘(1 − (i · 𝐴))) ∈ ℂ)
30		addcl 11149	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i · 𝐴)) ∈ ℂ)
31	21, 23, 30	sylancr 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 + (i · 𝐴)) ∈ ℂ)
32	27	simp3d 1156	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 + (i · 𝐴)) ≠ 0)
33	31, 32	logcld 26623	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (log‘(1 + (i · 𝐴))) ∈ ℂ)
34	29, 33	subcld 11536	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))) ∈ ℂ)
35		cjmul 15160	. . . . 5 ⊢ (((i / 2) ∈ ℂ ∧ ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))) ∈ ℂ) → (∗‘((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) = ((∗‘(i / 2)) · (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))))
36	20, 34, 35	sylancr 596	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) = ((∗‘(i / 2)) · (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))))
37		2ne0 12318	. . . . . . . 8 ⊢ 2 ≠ 0
38		2cn 12287	. . . . . . . . 9 ⊢ 2 ∈ ℂ
39	4, 38	cjdivi 15209	. . . . . . . 8 ⊢ (2 ≠ 0 → (∗‘(i / 2)) = ((∗‘i) / (∗‘2)))
40	37, 39	ax-mp 5	. . . . . . 7 ⊢ (∗‘(i / 2)) = ((∗‘i) / (∗‘2))
41		divneg 11876	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(i / 2) = (-i / 2))
42	4, 38, 37, 41	mp3an 1481	. . . . . . . 8 ⊢ -(i / 2) = (-i / 2)
43		cji 15177	. . . . . . . . 9 ⊢ (∗‘i) = -i
44		2re 12286	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
45		cjre 15157	. . . . . . . . . 10 ⊢ (2 ∈ ℝ → (∗‘2) = 2)
46	44, 45	ax-mp 5	. . . . . . . . 9 ⊢ (∗‘2) = 2
47	43, 46	oveq12i 7403	. . . . . . . 8 ⊢ ((∗‘i) / (∗‘2)) = (-i / 2)
48	42, 47	eqtr4i 2787	. . . . . . 7 ⊢ -(i / 2) = ((∗‘i) / (∗‘2))
49	40, 48	eqtr4i 2787	. . . . . 6 ⊢ (∗‘(i / 2)) = -(i / 2)
50	49	oveq1i 7401	. . . . 5 ⊢ ((∗‘(i / 2)) · (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) = (-(i / 2) · (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))))
51	34	cjcld 15214	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))) ∈ ℂ)
52		mulneg12 11619	. . . . . 6 ⊢ (((i / 2) ∈ ℂ ∧ (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))) ∈ ℂ) → (-(i / 2) · (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) = ((i / 2) · -(∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))))
53	20, 51, 52	sylancr 596	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (-(i / 2) · (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) = ((i / 2) · -(∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))))
54	50, 53	eqtrid 2808	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → ((∗‘(i / 2)) · (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) = ((i / 2) · -(∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))))
55		cjsub 15167	. . . . . . . . 9 ⊢ (((log‘(1 − (i · 𝐴))) ∈ ℂ ∧ (log‘(1 + (i · 𝐴))) ∈ ℂ) → (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))) = ((∗‘(log‘(1 − (i · 𝐴)))) − (∗‘(log‘(1 + (i · 𝐴))))))
56	29, 33, 55	syl2anc 593	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))) = ((∗‘(log‘(1 − (i · 𝐴)))) − (∗‘(log‘(1 + (i · 𝐴))))))
57		imsub 15153	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(1 − (i · 𝐴))) = ((ℑ‘1) − (ℑ‘(i · 𝐴))))
58	21, 23, 57	sylancr 596	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℑ‘(1 − (i · 𝐴))) = ((ℑ‘1) − (ℑ‘(i · 𝐴))))
59		reim 15127	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
60	59	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
61	60	oveq2d 7407	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → ((ℑ‘1) − (ℜ‘𝐴)) = ((ℑ‘1) − (ℑ‘(i · 𝐴))))
62	58, 61	eqtr4d 2799	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℑ‘(1 − (i · 𝐴))) = ((ℑ‘1) − (ℜ‘𝐴)))
63		df-neg 11411	. . . . . . . . . . . . . 14 ⊢ -(ℜ‘𝐴) = (0 − (ℜ‘𝐴))
64		im1 15173	. . . . . . . . . . . . . . 15 ⊢ (ℑ‘1) = 0
65	64	oveq1i 7401	. . . . . . . . . . . . . 14 ⊢ ((ℑ‘1) − (ℜ‘𝐴)) = (0 − (ℜ‘𝐴))
66	63, 65	eqtr4i 2787	. . . . . . . . . . . . 13 ⊢ -(ℜ‘𝐴) = ((ℑ‘1) − (ℜ‘𝐴))
67	62, 66	eqtr4di 2814	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℑ‘(1 − (i · 𝐴))) = -(ℜ‘𝐴))
68		recl 15128	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
69	68	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℜ‘𝐴) ∈ ℝ)
70	69	recnd 11204	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℜ‘𝐴) ∈ ℂ)
71	70, 2	negne0d 11534	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → -(ℜ‘𝐴) ≠ 0)
72	67, 71	eqnetrd 3023	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℑ‘(1 − (i · 𝐴))) ≠ 0)
73		logcj 26659	. . . . . . . . . . 11 ⊢ (((1 − (i · 𝐴)) ∈ ℂ ∧ (ℑ‘(1 − (i · 𝐴))) ≠ 0) → (log‘(∗‘(1 − (i · 𝐴)))) = (∗‘(log‘(1 − (i · 𝐴)))))
74	25, 72, 73	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (log‘(∗‘(1 − (i · 𝐴)))) = (∗‘(log‘(1 − (i · 𝐴)))))
75		cjsub 15167	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (∗‘(1 − (i · 𝐴))) = ((∗‘1) − (∗‘(i · 𝐴))))
76	21, 23, 75	sylancr 596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(1 − (i · 𝐴))) = ((∗‘1) − (∗‘(i · 𝐴))))
77		1re 11175	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
78		cjre 15157	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → (∗‘1) = 1)
79	77, 78	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘1) = 1)
80		cjmul 15160	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (∗‘(i · 𝐴)) = ((∗‘i) · (∗‘𝐴)))
81	4, 1, 80	sylancr 596	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(i · 𝐴)) = ((∗‘i) · (∗‘𝐴)))
82	43	oveq1i 7401	. . . . . . . . . . . . . . 15 ⊢ ((∗‘i) · (∗‘𝐴)) = (-i · (∗‘𝐴))
83		cjcl 15123	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) ∈ ℂ)
84	83	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘𝐴) ∈ ℂ)
85		mulneg1 11617	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ) → (-i · (∗‘𝐴)) = -(i · (∗‘𝐴)))
86	4, 84, 85	sylancr 596	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (-i · (∗‘𝐴)) = -(i · (∗‘𝐴)))
87	82, 86	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → ((∗‘i) · (∗‘𝐴)) = -(i · (∗‘𝐴)))
88	81, 87	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(i · 𝐴)) = -(i · (∗‘𝐴)))
89	79, 88	oveq12d 7409	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → ((∗‘1) − (∗‘(i · 𝐴))) = (1 − -(i · (∗‘𝐴))))
90		mulcl 11151	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ) → (i · (∗‘𝐴)) ∈ ℂ)
91	4, 84, 90	sylancr 596	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (i · (∗‘𝐴)) ∈ ℂ)
92		subneg 11474	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (i · (∗‘𝐴)) ∈ ℂ) → (1 − -(i · (∗‘𝐴))) = (1 + (i · (∗‘𝐴))))
93	21, 91, 92	sylancr 596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 − -(i · (∗‘𝐴))) = (1 + (i · (∗‘𝐴))))
94	76, 89, 93	3eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(1 − (i · 𝐴))) = (1 + (i · (∗‘𝐴))))
95	94	fveq2d 6866	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (log‘(∗‘(1 − (i · 𝐴)))) = (log‘(1 + (i · (∗‘𝐴)))))
96	74, 95	eqtr3d 2798	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(log‘(1 − (i · 𝐴)))) = (log‘(1 + (i · (∗‘𝐴)))))
97		imadd 15152	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(1 + (i · 𝐴))) = ((ℑ‘1) + (ℑ‘(i · 𝐴))))
98	21, 23, 97	sylancr 596	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℑ‘(1 + (i · 𝐴))) = ((ℑ‘1) + (ℑ‘(i · 𝐴))))
99	60	oveq2d 7407	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (0 + (ℜ‘𝐴)) = (0 + (ℑ‘(i · 𝐴))))
100	64	oveq1i 7401	. . . . . . . . . . . . . 14 ⊢ ((ℑ‘1) + (ℑ‘(i · 𝐴))) = (0 + (ℑ‘(i · 𝐴)))
101	99, 100	eqtr4di 2814	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (0 + (ℜ‘𝐴)) = ((ℑ‘1) + (ℑ‘(i · 𝐴))))
102	70	addlidd 11378	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (0 + (ℜ‘𝐴)) = (ℜ‘𝐴))
103	98, 101, 102	3eqtr2d 2802	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℑ‘(1 + (i · 𝐴))) = (ℜ‘𝐴))
104	103, 2	eqnetrd 3023	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (ℑ‘(1 + (i · 𝐴))) ≠ 0)
105		logcj 26659	. . . . . . . . . . 11 ⊢ (((1 + (i · 𝐴)) ∈ ℂ ∧ (ℑ‘(1 + (i · 𝐴))) ≠ 0) → (log‘(∗‘(1 + (i · 𝐴)))) = (∗‘(log‘(1 + (i · 𝐴)))))
106	31, 104, 105	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (log‘(∗‘(1 + (i · 𝐴)))) = (∗‘(log‘(1 + (i · 𝐴)))))
107		cjadd 15159	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (∗‘(1 + (i · 𝐴))) = ((∗‘1) + (∗‘(i · 𝐴))))
108	21, 23, 107	sylancr 596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(1 + (i · 𝐴))) = ((∗‘1) + (∗‘(i · 𝐴))))
109	79, 88	oveq12d 7409	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → ((∗‘1) + (∗‘(i · 𝐴))) = (1 + -(i · (∗‘𝐴))))
110		negsub 11473	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (i · (∗‘𝐴)) ∈ ℂ) → (1 + -(i · (∗‘𝐴))) = (1 − (i · (∗‘𝐴))))
111	21, 91, 110	sylancr 596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 + -(i · (∗‘𝐴))) = (1 − (i · (∗‘𝐴))))
112	108, 109, 111	3eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(1 + (i · 𝐴))) = (1 − (i · (∗‘𝐴))))
113	112	fveq2d 6866	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (log‘(∗‘(1 + (i · 𝐴)))) = (log‘(1 − (i · (∗‘𝐴)))))
114	106, 113	eqtr3d 2798	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(log‘(1 + (i · 𝐴)))) = (log‘(1 − (i · (∗‘𝐴)))))
115	96, 114	oveq12d 7409	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → ((∗‘(log‘(1 − (i · 𝐴)))) − (∗‘(log‘(1 + (i · 𝐴))))) = ((log‘(1 + (i · (∗‘𝐴)))) − (log‘(1 − (i · (∗‘𝐴))))))
116	56, 115	eqtrd 2796	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))) = ((log‘(1 + (i · (∗‘𝐴)))) − (log‘(1 − (i · (∗‘𝐴))))))
117	116	negeqd 11418	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → -(∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))) = -((log‘(1 + (i · (∗‘𝐴)))) − (log‘(1 − (i · (∗‘𝐴))))))
118		addcl 11149	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ (i · (∗‘𝐴)) ∈ ℂ) → (1 + (i · (∗‘𝐴))) ∈ ℂ)
119	21, 91, 118	sylancr 596	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 + (i · (∗‘𝐴))) ∈ ℂ)
120		atandmcj 26962	. . . . . . . . . 10 ⊢ (𝐴 ∈ dom arctan → (∗‘𝐴) ∈ dom arctan)
121	18, 120	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘𝐴) ∈ dom arctan)
122		atandm2 26930	. . . . . . . . . 10 ⊢ ((∗‘𝐴) ∈ dom arctan ↔ ((∗‘𝐴) ∈ ℂ ∧ (1 − (i · (∗‘𝐴))) ≠ 0 ∧ (1 + (i · (∗‘𝐴))) ≠ 0))
123	122	simp3bi 1159	. . . . . . . . 9 ⊢ ((∗‘𝐴) ∈ dom arctan → (1 + (i · (∗‘𝐴))) ≠ 0)
124	121, 123	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 + (i · (∗‘𝐴))) ≠ 0)
125	119, 124	logcld 26623	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (log‘(1 + (i · (∗‘𝐴)))) ∈ ℂ)
126		subcl 11423	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ (i · (∗‘𝐴)) ∈ ℂ) → (1 − (i · (∗‘𝐴))) ∈ ℂ)
127	21, 91, 126	sylancr 596	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 − (i · (∗‘𝐴))) ∈ ℂ)
128	122	simp2bi 1158	. . . . . . . . 9 ⊢ ((∗‘𝐴) ∈ dom arctan → (1 − (i · (∗‘𝐴))) ≠ 0)
129	121, 128	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (1 − (i · (∗‘𝐴))) ≠ 0)
130	127, 129	logcld 26623	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (log‘(1 − (i · (∗‘𝐴)))) ∈ ℂ)
131	125, 130	negsubdi2d 11552	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → -((log‘(1 + (i · (∗‘𝐴)))) − (log‘(1 − (i · (∗‘𝐴))))) = ((log‘(1 − (i · (∗‘𝐴)))) − (log‘(1 + (i · (∗‘𝐴))))))
132	117, 131	eqtrd 2796	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → -(∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))) = ((log‘(1 − (i · (∗‘𝐴)))) − (log‘(1 + (i · (∗‘𝐴))))))
133	132	oveq2d 7407	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → ((i / 2) · -(∗‘((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) = ((i / 2) · ((log‘(1 − (i · (∗‘𝐴)))) − (log‘(1 + (i · (∗‘𝐴)))))))
134	36, 54, 133	3eqtrd 2800	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) = ((i / 2) · ((log‘(1 − (i · (∗‘𝐴)))) − (log‘(1 + (i · (∗‘𝐴)))))))
135		atanval 26937	. . . . 5 ⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) = ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))))
136	18, 135	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (arctan‘𝐴) = ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴))))))
137	136	fveq2d 6866	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(arctan‘𝐴)) = (∗‘((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))))
138		atanval 26937	. . . 4 ⊢ ((∗‘𝐴) ∈ dom arctan → (arctan‘(∗‘𝐴)) = ((i / 2) · ((log‘(1 − (i · (∗‘𝐴)))) − (log‘(1 + (i · (∗‘𝐴)))))))
139	121, 138	syl 17	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (arctan‘(∗‘𝐴)) = ((i / 2) · ((log‘(1 − (i · (∗‘𝐴)))) − (log‘(1 + (i · (∗‘𝐴)))))))
140	134, 137, 139	3eqtr4d 2806	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (∗‘(arctan‘𝐴)) = (arctan‘(∗‘𝐴)))
141	18, 140	jca 519	1 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (𝐴 ∈ dom arctan ∧ (∗‘(arctan‘𝐴)) = (arctan‘(∗‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 dom cdm 5643 ‘cfv 6516 (class class class)co 7391 ℂcc 11065 ℝcr 11066 0cc0 11067 1c1 11068 ici 11069 + caddc 11070 · cmul 11072 − cmin 11408 -cneg 11409 / cdiv 11838 2c2 12266 ∗ccj 15114 ℜcre 15115 ℑcim 15116 logclog 26607 arctancatan 26917

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-inf2 9590 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145 ax-addf 11146

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-of 7655 df-om 7842 df-1st 7965 df-2nd 7966 df-supp 8135 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-2o 8432 df-er 8672 df-map 8804 df-pm 8805 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9302 df-fi 9351 df-sup 9382 df-inf 9383 df-oi 9452 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-7 12279 df-8 12280 df-9 12281 df-n0 12476 df-z 12563 df-dec 12683 df-uz 12834 df-q 12944 df-rp 12988 df-xneg 13108 df-xadd 13109 df-xmul 13110 df-ioo 13347 df-ioc 13348 df-ico 13349 df-icc 13350 df-fz 13507 df-fzo 13654 df-fl 13796 df-mod 13874 df-seq 14009 df-exp 14069 df-fac 14281 df-bc 14310 df-hash 14338 df-shft 15074 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-limsup 15489 df-clim 15506 df-rlim 15507 df-sum 15705 df-ef 16088 df-sin 16090 df-cos 16091 df-pi 16093 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-mulr 17291 df-starv 17292 df-sca 17293 df-vsca 17294 df-ip 17295 df-tset 17296 df-ple 17297 df-ds 17299 df-unif 17300 df-hom 17301 df-cco 17302 df-rest 17442 df-topn 17443 df-0g 17461 df-gsum 17462 df-topgen 17463 df-pt 17464 df-prds 17467 df-xrs 17523 df-qtop 17528 df-imas 17529 df-xps 17531 df-mre 17605 df-mrc 17606 df-acs 17608 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-submnd 18809 df-mulg 19101 df-cntz 19348 df-cmn 19813 df-psmet 21404 df-xmet 21405 df-met 21406 df-bl 21407 df-mopn 21408 df-fbas 21409 df-fg 21410 df-cnfld 21413 df-top 22942 df-topon 22959 df-topsp 22981 df-bases 22994 df-cld 23067 df-ntr 23068 df-cls 23069 df-nei 23146 df-lp 23184 df-perf 23185 df-cn 23275 df-cnp 23276 df-haus 23363 df-tx 23610 df-hmeo 23803 df-fil 23894 df-fm 23986 df-flim 23987 df-flf 23988 df-xms 24368 df-ms 24369 df-tms 24370 df-cncf 24928 df-limc 25916 df-dv 25917 df-log 26609 df-atan 26920

This theorem is referenced by: atanrecl 26964

W3C validator