Theorem atanlogaddlem 26840

Description: Lemma for atanlogadd 26841. (Contributed by Mario Carneiro, 3-Apr-2015.)

Assertion

Ref	Expression
atanlogaddlem	⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)

Proof of Theorem atanlogaddlem

Step	Hyp	Ref	Expression
1		0re 11136	. . . 4 ⊢ 0 ∈ ℝ
2		atandm2 26804	. . . . . 6 ⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0))
3	2	simp1bi 1145	. . . . 5 ⊢ (𝐴 ∈ dom arctan → 𝐴 ∈ ℂ)
4	3	recld 15120	. . . 4 ⊢ (𝐴 ∈ dom arctan → (ℜ‘𝐴) ∈ ℝ)
5		leloe 11221	. . . 4 ⊢ ((0 ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (0 ≤ (ℜ‘𝐴) ↔ (0 < (ℜ‘𝐴) ∨ 0 = (ℜ‘𝐴))))
6	1, 4, 5	sylancr 587	. . 3 ⊢ (𝐴 ∈ dom arctan → (0 ≤ (ℜ‘𝐴) ↔ (0 < (ℜ‘𝐴) ∨ 0 = (ℜ‘𝐴))))
7	6	biimpa 476	. 2 ⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → (0 < (ℜ‘𝐴) ∨ 0 = (ℜ‘𝐴)))
8		ax-1cn 11086	. . . . . . . 8 ⊢ 1 ∈ ℂ
9		ax-icn 11087	. . . . . . . . 9 ⊢ i ∈ ℂ
10		mulcl 11112	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
11	9, 3, 10	sylancr 587	. . . . . . . 8 ⊢ (𝐴 ∈ dom arctan → (i · 𝐴) ∈ ℂ)
12		addcl 11110	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i · 𝐴)) ∈ ℂ)
13	8, 11, 12	sylancr 587	. . . . . . 7 ⊢ (𝐴 ∈ dom arctan → (1 + (i · 𝐴)) ∈ ℂ)
14	2	simp3bi 1147	. . . . . . 7 ⊢ (𝐴 ∈ dom arctan → (1 + (i · 𝐴)) ≠ 0)
15	13, 14	logcld 26496	. . . . . 6 ⊢ (𝐴 ∈ dom arctan → (log‘(1 + (i · 𝐴))) ∈ ℂ)
16		subcl 11381	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i · 𝐴)) ∈ ℂ)
17	8, 11, 16	sylancr 587	. . . . . . 7 ⊢ (𝐴 ∈ dom arctan → (1 − (i · 𝐴)) ∈ ℂ)
18	2	simp2bi 1146	. . . . . . 7 ⊢ (𝐴 ∈ dom arctan → (1 − (i · 𝐴)) ≠ 0)
19	17, 18	logcld 26496	. . . . . 6 ⊢ (𝐴 ∈ dom arctan → (log‘(1 − (i · 𝐴))) ∈ ℂ)
20	15, 19	addcld 11153	. . . . 5 ⊢ (𝐴 ∈ dom arctan → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ℂ)
21	20	adantr 480	. . . 4 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ℂ)
22		pire 26383	. . . . . . . 8 ⊢ π ∈ ℝ
23	22	renegcli 11444	. . . . . . 7 ⊢ -π ∈ ℝ
24	23	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -π ∈ ℝ)
25	19	adantr 480	. . . . . . 7 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(1 − (i · 𝐴))) ∈ ℂ)
26	25	imcld 15121	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 − (i · 𝐴)))) ∈ ℝ)
27	15	adantr 480	. . . . . . . 8 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(1 + (i · 𝐴))) ∈ ℂ)
28	27	imcld 15121	. . . . . . 7 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 + (i · 𝐴)))) ∈ ℝ)
29	28, 26	readdcld 11163	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴))))) ∈ ℝ)
30	17	adantr 480	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (1 − (i · 𝐴)) ∈ ℂ)
31		im1 15081	. . . . . . . . . . . . 13 ⊢ (ℑ‘1) = 0
32	31	oveq1i 7363	. . . . . . . . . . . 12 ⊢ ((ℑ‘1) − (ℑ‘(i · 𝐴))) = (0 − (ℑ‘(i · 𝐴)))
33		df-neg 11369	. . . . . . . . . . . 12 ⊢ -(ℑ‘(i · 𝐴)) = (0 − (ℑ‘(i · 𝐴)))
34	32, 33	eqtr4i 2755	. . . . . . . . . . 11 ⊢ ((ℑ‘1) − (ℑ‘(i · 𝐴))) = -(ℑ‘(i · 𝐴))
35	11	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · 𝐴) ∈ ℂ)
36		imsub 15061	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(1 − (i · 𝐴))) = ((ℑ‘1) − (ℑ‘(i · 𝐴))))
37	8, 35, 36	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(1 − (i · 𝐴))) = ((ℑ‘1) − (ℑ‘(i · 𝐴))))
38	3	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 𝐴 ∈ ℂ)
39		reim 15035	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
40	38, 39	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
41	40	negeqd 11376	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -(ℜ‘𝐴) = -(ℑ‘(i · 𝐴)))
42	34, 37, 41	3eqtr4a 2790	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(1 − (i · 𝐴))) = -(ℜ‘𝐴))
43	4	lt0neg2d 11709	. . . . . . . . . . 11 ⊢ (𝐴 ∈ dom arctan → (0 < (ℜ‘𝐴) ↔ -(ℜ‘𝐴) < 0))
44	43	biimpa 476	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -(ℜ‘𝐴) < 0)
45	42, 44	eqbrtrd 5117	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(1 − (i · 𝐴))) < 0)
46		argimlt0 26539	. . . . . . . . 9 ⊢ (((1 − (i · 𝐴)) ∈ ℂ ∧ (ℑ‘(1 − (i · 𝐴))) < 0) → (ℑ‘(log‘(1 − (i · 𝐴)))) ∈ (-π(,)0))
47	30, 45, 46	syl2anc 584	. . . . . . . 8 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 − (i · 𝐴)))) ∈ (-π(,)0))
48		eliooord 13327	. . . . . . . 8 ⊢ ((ℑ‘(log‘(1 − (i · 𝐴)))) ∈ (-π(,)0) → (-π < (ℑ‘(log‘(1 − (i · 𝐴)))) ∧ (ℑ‘(log‘(1 − (i · 𝐴)))) < 0))
49	47, 48	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (-π < (ℑ‘(log‘(1 − (i · 𝐴)))) ∧ (ℑ‘(log‘(1 − (i · 𝐴)))) < 0))
50	49	simpld 494	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -π < (ℑ‘(log‘(1 − (i · 𝐴)))))
51	13	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (1 + (i · 𝐴)) ∈ ℂ)
52		simpr 484	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘𝐴))
53		imadd 15060	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(1 + (i · 𝐴))) = ((ℑ‘1) + (ℑ‘(i · 𝐴))))
54	8, 35, 53	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(1 + (i · 𝐴))) = ((ℑ‘1) + (ℑ‘(i · 𝐴))))
55	40	oveq2d 7369	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘1) + (ℜ‘𝐴)) = ((ℑ‘1) + (ℑ‘(i · 𝐴))))
56	31	oveq1i 7363	. . . . . . . . . . . . 13 ⊢ ((ℑ‘1) + (ℜ‘𝐴)) = (0 + (ℜ‘𝐴))
57	38	recld 15120	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℝ)
58	57	recnd 11162	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℂ)
59	58	addlidd 11336	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (0 + (ℜ‘𝐴)) = (ℜ‘𝐴))
60	56, 59	eqtrid 2776	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘1) + (ℜ‘𝐴)) = (ℜ‘𝐴))
61	54, 55, 60	3eqtr2d 2770	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(1 + (i · 𝐴))) = (ℜ‘𝐴))
62	52, 61	breqtrrd 5123	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 < (ℑ‘(1 + (i · 𝐴))))
63		argimgt0 26538	. . . . . . . . . 10 ⊢ (((1 + (i · 𝐴)) ∈ ℂ ∧ 0 < (ℑ‘(1 + (i · 𝐴)))) → (ℑ‘(log‘(1 + (i · 𝐴)))) ∈ (0(,)π))
64	51, 62, 63	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 + (i · 𝐴)))) ∈ (0(,)π))
65		eliooord 13327	. . . . . . . . 9 ⊢ ((ℑ‘(log‘(1 + (i · 𝐴)))) ∈ (0(,)π) → (0 < (ℑ‘(log‘(1 + (i · 𝐴)))) ∧ (ℑ‘(log‘(1 + (i · 𝐴)))) < π))
66	64, 65	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (0 < (ℑ‘(log‘(1 + (i · 𝐴)))) ∧ (ℑ‘(log‘(1 + (i · 𝐴)))) < π))
67	66	simpld 494	. . . . . . 7 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 < (ℑ‘(log‘(1 + (i · 𝐴)))))
68	28, 26	ltaddpos2d 11724	. . . . . . 7 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (0 < (ℑ‘(log‘(1 + (i · 𝐴)))) ↔ (ℑ‘(log‘(1 − (i · 𝐴)))) < ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴)))))))
69	67, 68	mpbid 232	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 − (i · 𝐴)))) < ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴))))))
70	24, 26, 29, 50, 69	lttrd 11296	. . . . 5 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -π < ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴))))))
71	27, 25	imaddd 15141	. . . . 5 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴))))) = ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴))))))
72	70, 71	breqtrrd 5123	. . . 4 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -π < (ℑ‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴))))))
73	22	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → π ∈ ℝ)
74		0red 11137	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 ∈ ℝ)
75	49	simprd 495	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 − (i · 𝐴)))) < 0)
76	26, 74, 28, 75	ltadd2dd 11294	. . . . . . . 8 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴))))) < ((ℑ‘(log‘(1 + (i · 𝐴)))) + 0))
77	28	recnd 11162	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 + (i · 𝐴)))) ∈ ℂ)
78	77	addridd 11335	. . . . . . . 8 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(1 + (i · 𝐴)))) + 0) = (ℑ‘(log‘(1 + (i · 𝐴)))))
79	76, 78	breqtrd 5121	. . . . . . 7 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴))))) < (ℑ‘(log‘(1 + (i · 𝐴)))))
80	66	simprd 495	. . . . . . 7 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 + (i · 𝐴)))) < π)
81	29, 28, 73, 79, 80	lttrd 11296	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴))))) < π)
82	29, 73, 81	ltled 11283	. . . . 5 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(1 + (i · 𝐴)))) + (ℑ‘(log‘(1 − (i · 𝐴))))) ≤ π)
83	71, 82	eqbrtrd 5117	. . . 4 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴))))) ≤ π)
84		ellogrn 26485	. . . 4 ⊢ (((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log ↔ (((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ℂ ∧ -π < (ℑ‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴))))) ∧ (ℑ‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴))))) ≤ π))
85	21, 72, 83, 84	syl3anbrc 1344	. . 3 ⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
86		0red 11137	. . . 4 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → 0 ∈ ℝ)
87	11	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → (i · 𝐴) ∈ ℂ)
88		simpr 484	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → 0 = (ℜ‘𝐴))
89	3	adantr 480	. . . . . . 7 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → 𝐴 ∈ ℂ)
90	89, 39	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
91	88, 90	eqtr2d 2765	. . . . 5 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → (ℑ‘(i · 𝐴)) = 0)
92	87, 91	reim0bd 15126	. . . 4 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → (i · 𝐴) ∈ ℝ)
93	15, 19	addcomd 11337	. . . . . 6 ⊢ (𝐴 ∈ dom arctan → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) = ((log‘(1 − (i · 𝐴))) + (log‘(1 + (i · 𝐴)))))
94	93	ad2antrr 726	. . . . 5 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) = ((log‘(1 − (i · 𝐴))) + (log‘(1 + (i · 𝐴)))))
95		logrncl 26493	. . . . . . . 8 ⊢ (((1 − (i · 𝐴)) ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0) → (log‘(1 − (i · 𝐴))) ∈ ran log)
96	17, 18, 95	syl2anc 584	. . . . . . 7 ⊢ (𝐴 ∈ dom arctan → (log‘(1 − (i · 𝐴))) ∈ ran log)
97	96	ad2antrr 726	. . . . . 6 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → (log‘(1 − (i · 𝐴))) ∈ ran log)
98		1re 11134	. . . . . . . . 9 ⊢ 1 ∈ ℝ
99	92	adantr 480	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → (i · 𝐴) ∈ ℝ)
100		readdcl 11111	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (i · 𝐴) ∈ ℝ) → (1 + (i · 𝐴)) ∈ ℝ)
101	98, 99, 100	sylancr 587	. . . . . . . 8 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → (1 + (i · 𝐴)) ∈ ℝ)
102		0red 11137	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → 0 ∈ ℝ)
103		1red 11135	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → 1 ∈ ℝ)
104		0lt1 11661	. . . . . . . . . 10 ⊢ 0 < 1
105	104	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → 0 < 1)
106		addge01 11649	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ (i · 𝐴) ∈ ℝ) → (0 ≤ (i · 𝐴) ↔ 1 ≤ (1 + (i · 𝐴))))
107	98, 92, 106	sylancr 587	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → (0 ≤ (i · 𝐴) ↔ 1 ≤ (1 + (i · 𝐴))))
108	107	biimpa 476	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → 1 ≤ (1 + (i · 𝐴)))
109	102, 103, 101, 105, 108	ltletrd 11295	. . . . . . . 8 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → 0 < (1 + (i · 𝐴)))
110	101, 109	elrpd 12953	. . . . . . 7 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → (1 + (i · 𝐴)) ∈ ℝ+)
111	110	relogcld 26549	. . . . . 6 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → (log‘(1 + (i · 𝐴))) ∈ ℝ)
112		logrnaddcl 26500	. . . . . 6 ⊢ (((log‘(1 − (i · 𝐴))) ∈ ran log ∧ (log‘(1 + (i · 𝐴))) ∈ ℝ) → ((log‘(1 − (i · 𝐴))) + (log‘(1 + (i · 𝐴)))) ∈ ran log)
113	97, 111, 112	syl2anc 584	. . . . 5 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → ((log‘(1 − (i · 𝐴))) + (log‘(1 + (i · 𝐴)))) ∈ ran log)
114	94, 113	eqeltrd 2828	. . . 4 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ 0 ≤ (i · 𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
115		logrncl 26493	. . . . . . 7 ⊢ (((1 + (i · 𝐴)) ∈ ℂ ∧ (1 + (i · 𝐴)) ≠ 0) → (log‘(1 + (i · 𝐴))) ∈ ran log)
116	13, 14, 115	syl2anc 584	. . . . . 6 ⊢ (𝐴 ∈ dom arctan → (log‘(1 + (i · 𝐴))) ∈ ran log)
117	116	ad2antrr 726	. . . . 5 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → (log‘(1 + (i · 𝐴))) ∈ ran log)
118	92	adantr 480	. . . . . . . 8 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → (i · 𝐴) ∈ ℝ)
119		resubcl 11447	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ (i · 𝐴) ∈ ℝ) → (1 − (i · 𝐴)) ∈ ℝ)
120	98, 118, 119	sylancr 587	. . . . . . 7 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → (1 − (i · 𝐴)) ∈ ℝ)
121		0red 11137	. . . . . . . 8 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → 0 ∈ ℝ)
122		1red 11135	. . . . . . . 8 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → 1 ∈ ℝ)
123	104	a1i 11	. . . . . . . 8 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → 0 < 1)
124		1m0e1 12263	. . . . . . . . 9 ⊢ (1 − 0) = 1
125		1red 11135	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → 1 ∈ ℝ)
126	92, 86, 125	lesub2d 11747	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → ((i · 𝐴) ≤ 0 ↔ (1 − 0) ≤ (1 − (i · 𝐴))))
127	126	biimpa 476	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → (1 − 0) ≤ (1 − (i · 𝐴)))
128	124, 127	eqbrtrrid 5131	. . . . . . . 8 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → 1 ≤ (1 − (i · 𝐴)))
129	121, 122, 120, 123, 128	ltletrd 11295	. . . . . . 7 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → 0 < (1 − (i · 𝐴)))
130	120, 129	elrpd 12953	. . . . . 6 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → (1 − (i · 𝐴)) ∈ ℝ+)
131	130	relogcld 26549	. . . . 5 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → (log‘(1 − (i · 𝐴))) ∈ ℝ)
132		logrnaddcl 26500	. . . . 5 ⊢ (((log‘(1 + (i · 𝐴))) ∈ ran log ∧ (log‘(1 − (i · 𝐴))) ∈ ℝ) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
133	117, 131, 132	syl2anc 584	. . . 4 ⊢ (((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) ∧ (i · 𝐴) ≤ 0) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
134	86, 92, 114, 133	lecasei 11241	. . 3 ⊢ ((𝐴 ∈ dom arctan ∧ 0 = (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
135	85, 134	jaodan 959	. 2 ⊢ ((𝐴 ∈ dom arctan ∧ (0 < (ℜ‘𝐴) ∨ 0 = (ℜ‘𝐴))) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
136	7, 135	syldan 591	1 ⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925   class class class wbr 5095  dom cdm 5623  ran crn 5624  ‘cfv 6486  (class class class)co 7353  ℂcc 11026  ℝcr 11027  0cc0 11028  1c1 11029  ici 11030   + caddc 11031   · cmul 11033   < clt 11168   ≤ cle 11169   − cmin 11366  -cneg 11367  (,)cioo 13267  ℜcre 15023  ℑcim 15024  πcpi 15992  logclog 26480  arctancatan 26791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-inf2 9556  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105  ax-pre-sup 11106  ax-addf 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-iin 4947  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7617  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8632  df-map 8762  df-pm 8763  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-fi 9320  df-sup 9351  df-inf 9352  df-oi 9421  df-card 9854  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-div 11797  df-nn 12148  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217  df-n0 12404  df-z 12491  df-dec 12611  df-uz 12755  df-q 12869  df-rp 12913  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13271  df-ioc 13272  df-ico 13273  df-icc 13274  df-fz 13430  df-fzo 13577  df-fl 13715  df-mod 13793  df-seq 13928  df-exp 13988  df-fac 14200  df-bc 14229  df-hash 14257  df-shft 14993  df-cj 15025  df-re 15026  df-im 15027  df-sqrt 15161  df-abs 15162  df-limsup 15397  df-clim 15414  df-rlim 15415  df-sum 15613  df-ef 15993  df-sin 15995  df-cos 15996  df-pi 15998  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17140  df-ress 17161  df-plusg 17193  df-mulr 17194  df-starv 17195  df-sca 17196  df-vsca 17197  df-ip 17198  df-tset 17199  df-ple 17200  df-ds 17202  df-unif 17203  df-hom 17204  df-cco 17205  df-rest 17345  df-topn 17346  df-0g 17364  df-gsum 17365  df-topgen 17366  df-pt 17367  df-prds 17370  df-xrs 17425  df-qtop 17430  df-imas 17431  df-xps 17433  df-mre 17507  df-mrc 17508  df-acs 17510  df-mgm 18533  df-sgrp 18612  df-mnd 18628  df-submnd 18677  df-mulg 18966  df-cntz 19215  df-cmn 19680  df-psmet 21272  df-xmet 21273  df-met 21274  df-bl 21275  df-mopn 21276  df-fbas 21277  df-fg 21278  df-cnfld 21281  df-top 22798  df-topon 22815  df-topsp 22837  df-bases 22850  df-cld 22923  df-ntr 22924  df-cls 22925  df-nei 23002  df-lp 23040  df-perf 23041  df-cn 23131  df-cnp 23132  df-haus 23219  df-tx 23466  df-hmeo 23659  df-fil 23750  df-fm 23842  df-flim 23843  df-flf 23844  df-xms 24225  df-ms 24226  df-tms 24227  df-cncf 24788  df-limc 25784  df-dv 25785  df-log 26482  df-atan 26794

This theorem is referenced by:  atanlogadd  26841