Proof of Theorem atanbndlem
Step | Hyp | Ref
| Expression |
1 | | rpre 12480 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
2 | | atanrecl 25649 |
. . 3
⊢ (𝐴 ∈ ℝ →
(arctan‘𝐴) ∈
ℝ) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (arctan‘𝐴)
∈ ℝ) |
4 | | picn 25204 |
. . . 4
⊢ π
∈ ℂ |
5 | | 2cn 11791 |
. . . 4
⊢ 2 ∈
ℂ |
6 | | 2ne0 11820 |
. . . 4
⊢ 2 ≠
0 |
7 | | divneg 11410 |
. . . 4
⊢ ((π
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) =
(-π / 2)) |
8 | 4, 5, 6, 7 | mp3an 1462 |
. . 3
⊢ -(π /
2) = (-π / 2) |
9 | | ax-1cn 10673 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
10 | | ax-icn 10674 |
. . . . . . . . . . . . 13
⊢ i ∈
ℂ |
11 | 1 | recnd 10747 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
12 | | mulcl 10699 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
13 | 10, 11, 12 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (i · 𝐴)
∈ ℂ) |
14 | | addcl 10697 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) |
15 | 9, 13, 14 | sylancr 590 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1 + (i · 𝐴))
∈ ℂ) |
16 | | atanre 25623 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ dom
arctan) |
17 | 1, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈ dom
arctan) |
18 | | atandm2 25615 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |
19 | 17, 18 | sylib 221 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℂ
∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) |
20 | 19 | simp3d 1145 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1 + (i · 𝐴))
≠ 0) |
21 | 15, 20 | logcld 25314 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(1 + (i · 𝐴))) ∈ ℂ) |
22 | | subcl 10963 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) |
23 | 9, 13, 22 | sylancr 590 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1 − (i · 𝐴)) ∈ ℂ) |
24 | 19 | simp2d 1144 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1 − (i · 𝐴)) ≠ 0) |
25 | 23, 24 | logcld 25314 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(1 − (i · 𝐴))) ∈ ℂ) |
26 | 21, 25 | subcld 11075 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) |
27 | | imre 14557 |
. . . . . . . . 9
⊢
(((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(ℜ‘(-i · ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))))) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(ℜ‘(-i · ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))))) |
29 | | atanval 25622 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) = ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
30 | 17, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (arctan‘𝐴) =
((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
31 | 30 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (2 · ((i / 2) ·
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) |
32 | 10, 5, 6 | divcan2i 11461 |
. . . . . . . . . . . . . 14
⊢ (2
· (i / 2)) = i |
33 | 32 | oveq1i 7180 |
. . . . . . . . . . . . 13
⊢ ((2
· (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = (i ·
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
34 | | 2re 11790 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ 2 ∈ ℝ) |
36 | 35 | recnd 10747 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ 2 ∈ ℂ) |
37 | | halfcl 11941 |
. . . . . . . . . . . . . . 15
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) |
38 | 10, 37 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ (i / 2) ∈ ℂ) |
39 | 25, 21 | subcld 11075 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) ∈
ℂ) |
40 | 36, 38, 39 | mulassd 10742 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ ((2 · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) = (2
· ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) |
41 | 33, 40 | eqtr3id 2787 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (i · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = (2 · ((i /
2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) |
42 | 31, 41 | eqtr4d 2776 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (i · ((log‘(1 − (i
· 𝐴))) −
(log‘(1 + (i · 𝐴)))))) |
43 | 21, 25 | negsubdi2d 11091 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ -((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) =
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
44 | 43 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (i · -((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) = (i
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
45 | 42, 44 | eqtr4d 2776 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (i · -((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴)))))) |
46 | | mulneg12 11156 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) → (-i · ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) = (i
· -((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))))) |
47 | 10, 26, 46 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (-i · ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) = (i
· -((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))))) |
48 | 45, 47 | eqtr4d 2776 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (-i · ((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴)))))) |
49 | 48 | fveq2d 6678 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (ℜ‘(2 · (arctan‘𝐴))) = (ℜ‘(-i ·
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))))) |
50 | | remulcl 10700 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ (arctan‘𝐴) ∈ ℝ) → (2 ·
(arctan‘𝐴)) ∈
ℝ) |
51 | 34, 3, 50 | sylancr 590 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) ∈ ℝ) |
52 | 51 | rered 14673 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (ℜ‘(2 · (arctan‘𝐴))) = (2 · (arctan‘𝐴))) |
53 | 28, 49, 52 | 3eqtr2rd 2780 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (ℑ‘((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴)))))) |
54 | | rpgt0 12484 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ 0 < 𝐴) |
55 | 1 | rered 14673 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (ℜ‘𝐴) =
𝐴) |
56 | 54, 55 | breqtrrd 5058 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 0 < (ℜ‘𝐴)) |
57 | | atanlogsublem 25653 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |
58 | 17, 56, 57 | syl2anc 587 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |
59 | 53, 58 | eqeltrd 2833 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) ∈ (-π(,)π)) |
60 | | eliooord 12880 |
. . . . . 6
⊢ ((2
· (arctan‘𝐴))
∈ (-π(,)π) → (-π < (2 · (arctan‘𝐴)) ∧ (2 ·
(arctan‘𝐴)) <
π)) |
61 | 59, 60 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (-π < (2 · (arctan‘𝐴)) ∧ (2 · (arctan‘𝐴)) < π)) |
62 | 61 | simpld 498 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ -π < (2 · (arctan‘𝐴))) |
63 | | pire 25203 |
. . . . . . 7
⊢ π
∈ ℝ |
64 | 63 | renegcli 11025 |
. . . . . 6
⊢ -π
∈ ℝ |
65 | 64 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ -π ∈ ℝ) |
66 | | 2pos 11819 |
. . . . . 6
⊢ 0 <
2 |
67 | 66 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ 0 < 2) |
68 | | ltdivmul 11593 |
. . . . 5
⊢ ((-π
∈ ℝ ∧ (arctan‘𝐴) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((-π / 2) < (arctan‘𝐴) ↔ -π < (2 ·
(arctan‘𝐴)))) |
69 | 65, 3, 35, 67, 68 | syl112anc 1375 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((-π / 2) < (arctan‘𝐴) ↔ -π < (2 ·
(arctan‘𝐴)))) |
70 | 62, 69 | mpbird 260 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (-π / 2) < (arctan‘𝐴)) |
71 | 8, 70 | eqbrtrid 5065 |
. 2
⊢ (𝐴 ∈ ℝ+
→ -(π / 2) < (arctan‘𝐴)) |
72 | 61 | simprd 499 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) < π) |
73 | 63 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ π ∈ ℝ) |
74 | | ltmuldiv2 11592 |
. . . 4
⊢
(((arctan‘𝐴)
∈ ℝ ∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 <
2)) → ((2 · (arctan‘𝐴)) < π ↔ (arctan‘𝐴) < (π /
2))) |
75 | 3, 73, 35, 67, 74 | syl112anc 1375 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((2 · (arctan‘𝐴)) < π ↔ (arctan‘𝐴) < (π /
2))) |
76 | 72, 75 | mpbid 235 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (arctan‘𝐴)
< (π / 2)) |
77 | | halfpire 25209 |
. . . . 5
⊢ (π /
2) ∈ ℝ |
78 | 77 | renegcli 11025 |
. . . 4
⊢ -(π /
2) ∈ ℝ |
79 | 78 | rexri 10777 |
. . 3
⊢ -(π /
2) ∈ ℝ* |
80 | 77 | rexri 10777 |
. . 3
⊢ (π /
2) ∈ ℝ* |
81 | | elioo2 12862 |
. . 3
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ*)
→ ((arctan‘𝐴)
∈ (-(π / 2)(,)(π / 2)) ↔ ((arctan‘𝐴) ∈ ℝ ∧ -(π / 2) <
(arctan‘𝐴) ∧
(arctan‘𝐴) < (π
/ 2)))) |
82 | 79, 80, 81 | mp2an 692 |
. 2
⊢
((arctan‘𝐴)
∈ (-(π / 2)(,)(π / 2)) ↔ ((arctan‘𝐴) ∈ ℝ ∧ -(π / 2) <
(arctan‘𝐴) ∧
(arctan‘𝐴) < (π
/ 2))) |
83 | 3, 71, 76, 82 | syl3anbrc 1344 |
1
⊢ (𝐴 ∈ ℝ+
→ (arctan‘𝐴)
∈ (-(π / 2)(,)(π / 2))) |