Proof of Theorem atanbndlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rpre 13043 | . . 3
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) | 
| 2 |  | atanrecl 26954 | . . 3
⊢ (𝐴 ∈ ℝ →
(arctan‘𝐴) ∈
ℝ) | 
| 3 | 1, 2 | syl 17 | . 2
⊢ (𝐴 ∈ ℝ+
→ (arctan‘𝐴)
∈ ℝ) | 
| 4 |  | picn 26501 | . . . 4
⊢ π
∈ ℂ | 
| 5 |  | 2cn 12341 | . . . 4
⊢ 2 ∈
ℂ | 
| 6 |  | 2ne0 12370 | . . . 4
⊢ 2 ≠
0 | 
| 7 |  | divneg 11959 | . . . 4
⊢ ((π
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) =
(-π / 2)) | 
| 8 | 4, 5, 6, 7 | mp3an 1463 | . . 3
⊢ -(π /
2) = (-π / 2) | 
| 9 |  | ax-1cn 11213 | . . . . . . . . . . . 12
⊢ 1 ∈
ℂ | 
| 10 |  | ax-icn 11214 | . . . . . . . . . . . . 13
⊢ i ∈
ℂ | 
| 11 | 1 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) | 
| 12 |  | mulcl 11239 | . . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) | 
| 13 | 10, 11, 12 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (i · 𝐴)
∈ ℂ) | 
| 14 |  | addcl 11237 | . . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) | 
| 15 | 9, 13, 14 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1 + (i · 𝐴))
∈ ℂ) | 
| 16 |  | atanre 26928 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ dom
arctan) | 
| 17 | 1, 16 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈ dom
arctan) | 
| 18 |  | atandm2 26920 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) | 
| 19 | 17, 18 | sylib 218 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℂ
∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) | 
| 20 | 19 | simp3d 1145 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1 + (i · 𝐴))
≠ 0) | 
| 21 | 15, 20 | logcld 26612 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(1 + (i · 𝐴))) ∈ ℂ) | 
| 22 |  | subcl 11507 | . . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) | 
| 23 | 9, 13, 22 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1 − (i · 𝐴)) ∈ ℂ) | 
| 24 | 19 | simp2d 1144 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1 − (i · 𝐴)) ≠ 0) | 
| 25 | 23, 24 | logcld 26612 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(1 − (i · 𝐴))) ∈ ℂ) | 
| 26 | 21, 25 | subcld 11620 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) | 
| 27 |  | imre 15147 | . . . . . . . . 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 26927 | . . . . . . . . . . . . . 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 7447 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (2 · ((i / 2) ·
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) | 
| 32 | 10, 5, 6 | divcan2i 12010 | . . . . . . . . . . . . . 14
⊢ (2
· (i / 2)) = i | 
| 33 | 32 | oveq1i 7441 | . . . . . . . . . . . . 13
⊢ ((2
· (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = (i ·
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) | 
| 34 |  | 2re 12340 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ | 
| 35 | 34 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ 2 ∈ ℝ) | 
| 36 | 35 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ 2 ∈ ℂ) | 
| 37 |  | halfcl 12491 | . . . . . . . . . . . . . . 15
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) | 
| 38 | 10, 37 | mp1i 13 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ (i / 2) ∈ ℂ) | 
| 39 | 25, 21 | subcld 11620 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) ∈
ℂ) | 
| 40 | 36, 38, 39 | mulassd 11284 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ ((2 · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) = (2
· ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) | 
| 41 | 33, 40 | eqtr3id 2791 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (i · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = (2 · ((i /
2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) | 
| 42 | 31, 41 | eqtr4d 2780 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (i · ((log‘(1 − (i
· 𝐴))) −
(log‘(1 + (i · 𝐴)))))) | 
| 43 | 21, 25 | negsubdi2d 11636 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ -((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) =
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) | 
| 44 | 43 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (i · -((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) = (i
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) | 
| 45 | 42, 44 | eqtr4d 2780 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (i · -((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴)))))) | 
| 46 |  | mulneg12 11701 | . . . . . . . . . . 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 587 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (-i · ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) = (i
· -((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))))) | 
| 48 | 45, 47 | eqtr4d 2780 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (-i · ((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴)))))) | 
| 49 | 48 | fveq2d 6910 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (ℜ‘(2 · (arctan‘𝐴))) = (ℜ‘(-i ·
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))))) | 
| 50 |  | remulcl 11240 | . . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ (arctan‘𝐴) ∈ ℝ) → (2 ·
(arctan‘𝐴)) ∈
ℝ) | 
| 51 | 34, 3, 50 | sylancr 587 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) ∈ ℝ) | 
| 52 | 51 | rered 15263 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (ℜ‘(2 · (arctan‘𝐴))) = (2 · (arctan‘𝐴))) | 
| 53 | 28, 49, 52 | 3eqtr2rd 2784 | . . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) = (ℑ‘((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴)))))) | 
| 54 |  | rpgt0 13047 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ 0 < 𝐴) | 
| 55 | 1 | rered 15263 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (ℜ‘𝐴) =
𝐴) | 
| 56 | 54, 55 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 0 < (ℜ‘𝐴)) | 
| 57 |  | atanlogsublem 26958 | . . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) | 
| 58 | 17, 56, 57 | syl2anc 584 | . . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) | 
| 59 | 53, 58 | eqeltrd 2841 | . . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) ∈ (-π(,)π)) | 
| 60 |  | eliooord 13446 | . . . . . 6
⊢ ((2
· (arctan‘𝐴))
∈ (-π(,)π) → (-π < (2 · (arctan‘𝐴)) ∧ (2 ·
(arctan‘𝐴)) <
π)) | 
| 61 | 59, 60 | syl 17 | . . . . 5
⊢ (𝐴 ∈ ℝ+
→ (-π < (2 · (arctan‘𝐴)) ∧ (2 · (arctan‘𝐴)) < π)) | 
| 62 | 61 | simpld 494 | . . . 4
⊢ (𝐴 ∈ ℝ+
→ -π < (2 · (arctan‘𝐴))) | 
| 63 |  | pire 26500 | . . . . . . 7
⊢ π
∈ ℝ | 
| 64 | 63 | renegcli 11570 | . . . . . 6
⊢ -π
∈ ℝ | 
| 65 | 64 | a1i 11 | . . . . 5
⊢ (𝐴 ∈ ℝ+
→ -π ∈ ℝ) | 
| 66 |  | 2pos 12369 | . . . . . 6
⊢ 0 <
2 | 
| 67 | 66 | a1i 11 | . . . . 5
⊢ (𝐴 ∈ ℝ+
→ 0 < 2) | 
| 68 |  | ltdivmul 12143 | . . . . 5
⊢ ((-π
∈ ℝ ∧ (arctan‘𝐴) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((-π / 2) < (arctan‘𝐴) ↔ -π < (2 ·
(arctan‘𝐴)))) | 
| 69 | 65, 3, 35, 67, 68 | syl112anc 1376 | . . . 4
⊢ (𝐴 ∈ ℝ+
→ ((-π / 2) < (arctan‘𝐴) ↔ -π < (2 ·
(arctan‘𝐴)))) | 
| 70 | 62, 69 | mpbird 257 | . . 3
⊢ (𝐴 ∈ ℝ+
→ (-π / 2) < (arctan‘𝐴)) | 
| 71 | 8, 70 | eqbrtrid 5178 | . 2
⊢ (𝐴 ∈ ℝ+
→ -(π / 2) < (arctan‘𝐴)) | 
| 72 | 61 | simprd 495 | . . 3
⊢ (𝐴 ∈ ℝ+
→ (2 · (arctan‘𝐴)) < π) | 
| 73 | 63 | a1i 11 | . . . 4
⊢ (𝐴 ∈ ℝ+
→ π ∈ ℝ) | 
| 74 |  | ltmuldiv2 12142 | . . . 4
⊢
(((arctan‘𝐴)
∈ ℝ ∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 <
2)) → ((2 · (arctan‘𝐴)) < π ↔ (arctan‘𝐴) < (π /
2))) | 
| 75 | 3, 73, 35, 67, 74 | syl112anc 1376 | . . 3
⊢ (𝐴 ∈ ℝ+
→ ((2 · (arctan‘𝐴)) < π ↔ (arctan‘𝐴) < (π /
2))) | 
| 76 | 72, 75 | mpbid 232 | . 2
⊢ (𝐴 ∈ ℝ+
→ (arctan‘𝐴)
< (π / 2)) | 
| 77 |  | halfpire 26506 | . . . . 5
⊢ (π /
2) ∈ ℝ | 
| 78 | 77 | renegcli 11570 | . . . 4
⊢ -(π /
2) ∈ ℝ | 
| 79 | 78 | rexri 11319 | . . 3
⊢ -(π /
2) ∈ ℝ* | 
| 80 | 77 | rexri 11319 | . . 3
⊢ (π /
2) ∈ ℝ* | 
| 81 |  | elioo2 13428 | . . 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))) |