Proof of Theorem ang180lem2
Step | Hyp | Ref
| Expression |
1 | | 2cn 11905 |
. . . . . . 7
⊢ 2 ∈
ℂ |
2 | | 1re 10833 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
3 | 2 | rehalfcli 12079 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
4 | 3 | recni 10847 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
5 | 1, 4 | negsubdii 11163 |
. . . . . 6
⊢ -(2
− (1 / 2)) = (-2 + (1 / 2)) |
6 | | 4d2e2 12000 |
. . . . . . . . 9
⊢ (4 / 2) =
2 |
7 | 6 | oveq1i 7223 |
. . . . . . . 8
⊢ ((4 / 2)
− (1 / 2)) = (2 − (1 / 2)) |
8 | | 4cn 11915 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
9 | | ax-1cn 10787 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
10 | | 2cnne0 12040 |
. . . . . . . . . 10
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
11 | | divsubdir 11526 |
. . . . . . . . . 10
⊢ ((4
∈ ℂ ∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
→ ((4 − 1) / 2) = ((4 / 2) − (1 / 2))) |
12 | 8, 9, 10, 11 | mp3an 1463 |
. . . . . . . . 9
⊢ ((4
− 1) / 2) = ((4 / 2) − (1 / 2)) |
13 | | 4m1e3 11959 |
. . . . . . . . . 10
⊢ (4
− 1) = 3 |
14 | 13 | oveq1i 7223 |
. . . . . . . . 9
⊢ ((4
− 1) / 2) = (3 / 2) |
15 | 12, 14 | eqtr3i 2767 |
. . . . . . . 8
⊢ ((4 / 2)
− (1 / 2)) = (3 / 2) |
16 | 7, 15 | eqtr3i 2767 |
. . . . . . 7
⊢ (2
− (1 / 2)) = (3 / 2) |
17 | 16 | negeqi 11071 |
. . . . . 6
⊢ -(2
− (1 / 2)) = -(3 / 2) |
18 | 5, 17 | eqtr3i 2767 |
. . . . 5
⊢ (-2 + (1
/ 2)) = -(3 / 2) |
19 | | 3re 11910 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
20 | 19 | rehalfcli 12079 |
. . . . . . . . . . . 12
⊢ (3 / 2)
∈ ℝ |
21 | 20 | recni 10847 |
. . . . . . . . . . 11
⊢ (3 / 2)
∈ ℂ |
22 | | picn 25349 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
23 | 21, 1, 22 | mulassi 10844 |
. . . . . . . . . 10
⊢ (((3 / 2)
· 2) · π) = ((3 / 2) · (2 ·
π)) |
24 | | 3cn 11911 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℂ |
25 | | 2ne0 11934 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
26 | 24, 1, 25 | divcan1i 11576 |
. . . . . . . . . . 11
⊢ ((3 / 2)
· 2) = 3 |
27 | 26 | oveq1i 7223 |
. . . . . . . . . 10
⊢ (((3 / 2)
· 2) · π) = (3 · π) |
28 | 23, 27 | eqtr3i 2767 |
. . . . . . . . 9
⊢ ((3 / 2)
· (2 · π)) = (3 · π) |
29 | 28 | negeqi 11071 |
. . . . . . . 8
⊢ -((3 / 2)
· (2 · π)) = -(3 · π) |
30 | | 2re 11904 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
31 | | pire 25348 |
. . . . . . . . . . 11
⊢ π
∈ ℝ |
32 | 30, 31 | remulcli 10849 |
. . . . . . . . . 10
⊢ (2
· π) ∈ ℝ |
33 | 32 | recni 10847 |
. . . . . . . . 9
⊢ (2
· π) ∈ ℂ |
34 | 21, 33 | mulneg1i 11278 |
. . . . . . . 8
⊢ (-(3 / 2)
· (2 · π)) = -((3 / 2) · (2 ·
π)) |
35 | 24, 22 | mulneg2i 11279 |
. . . . . . . 8
⊢ (3
· -π) = -(3 · π) |
36 | 29, 34, 35 | 3eqtr4i 2775 |
. . . . . . 7
⊢ (-(3 / 2)
· (2 · π)) = (3 · -π) |
37 | 31 | renegcli 11139 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ |
38 | 30, 37 | remulcli 10849 |
. . . . . . . . . . 11
⊢ (2
· -π) ∈ ℝ |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) ∈
ℝ) |
40 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π ∈
ℝ) |
41 | | simp1 1138 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ∈ ℂ) |
42 | | subcl 11077 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) |
43 | 9, 41, 42 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ∈ ℂ) |
44 | | simp3 1140 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 1) |
45 | 44 | necomd 2996 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ≠ 𝐴) |
46 | | subeq0 11104 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
47 | 9, 41, 46 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
48 | 47 | necon3bid 2985 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) ≠ 0 ↔ 1 ≠ 𝐴)) |
49 | 45, 48 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ≠ 0) |
50 | 43, 49 | reccld 11601 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ∈
ℂ) |
51 | 43, 49 | recne0d 11602 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ≠ 0) |
52 | 50, 51 | logcld 25459 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘(1 / (1 −
𝐴))) ∈
ℂ) |
53 | | subcl 11077 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) |
54 | 41, 9, 53 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ∈ ℂ) |
55 | | simp2 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 0) |
56 | 54, 41, 55 | divcld 11608 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ∈ ℂ) |
57 | | subeq0 11104 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 −
1) = 0 ↔ 𝐴 =
1)) |
58 | 41, 9, 57 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) = 0 ↔ 𝐴 = 1)) |
59 | 58 | necon3bid 2985 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) ≠ 0 ↔ 𝐴 ≠ 1)) |
60 | 44, 59 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ≠ 0) |
61 | 54, 41, 60, 55 | divne0d 11624 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ≠ 0) |
62 | 56, 61 | logcld 25459 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘((𝐴 − 1) / 𝐴)) ∈ ℂ) |
63 | 52, 62 | addcld 10852 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) ∈ ℂ) |
64 | 63 | imcld 14758 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ) |
65 | | logcl 25457 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
66 | 65 | 3adant3 1134 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘𝐴) ∈ ℂ) |
67 | 66 | imcld 14758 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘𝐴)) ∈ ℝ) |
68 | 52 | imcld 14758 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘(1
/ (1 − 𝐴)))) ∈
ℝ) |
69 | 62 | imcld 14758 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘((𝐴 − 1) / 𝐴))) ∈ ℝ) |
70 | 50, 51 | logimcld 25460 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π <
(ℑ‘(log‘(1 / (1 − 𝐴)))) ∧ (ℑ‘(log‘(1 / (1
− 𝐴)))) ≤
π)) |
71 | 70 | simpld 498 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π <
(ℑ‘(log‘(1 / (1 − 𝐴))))) |
72 | 56, 61 | logimcld 25460 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π <
(ℑ‘(log‘((𝐴 − 1) / 𝐴))) ∧ (ℑ‘(log‘((𝐴 − 1) / 𝐴))) ≤ π)) |
73 | 72 | simpld 498 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π <
(ℑ‘(log‘((𝐴 − 1) / 𝐴)))) |
74 | 40, 40, 68, 69, 71, 73 | lt2addd 11455 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π + -π) <
((ℑ‘(log‘(1 / (1 − 𝐴)))) + (ℑ‘(log‘((𝐴 − 1) / 𝐴))))) |
75 | | negpicn 25352 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℂ |
76 | 75 | 2timesi 11968 |
. . . . . . . . . . . 12
⊢ (2
· -π) = (-π + -π) |
77 | 76 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) = (-π
+ -π)) |
78 | 52, 62 | imaddd 14778 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) = ((ℑ‘(log‘(1 / (1
− 𝐴)))) +
(ℑ‘(log‘((𝐴 − 1) / 𝐴))))) |
79 | 74, 77, 78 | 3brtr4d 5085 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) <
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) |
80 | | logimcl 25458 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
81 | 80 | 3adant3 1134 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
82 | 81 | simpld 498 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π <
(ℑ‘(log‘𝐴))) |
83 | 39, 40, 64, 67, 79, 82 | lt2addd 11455 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((2 · -π) + -π)
< ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴)))) |
84 | | df-3 11894 |
. . . . . . . . . . . 12
⊢ 3 = (2 +
1) |
85 | 84 | oveq1i 7223 |
. . . . . . . . . . 11
⊢ (3
· -π) = ((2 + 1) · -π) |
86 | 1, 9, 75 | adddiri 10846 |
. . . . . . . . . . 11
⊢ ((2 + 1)
· -π) = ((2 · -π) + (1 · -π)) |
87 | 75 | mulid2i 10838 |
. . . . . . . . . . . 12
⊢ (1
· -π) = -π |
88 | 87 | oveq2i 7224 |
. . . . . . . . . . 11
⊢ ((2
· -π) + (1 · -π)) = ((2 · -π) +
-π) |
89 | 85, 86, 88 | 3eqtri 2769 |
. . . . . . . . . 10
⊢ (3
· -π) = ((2 · -π) + -π) |
90 | 89 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) = ((2
· -π) + -π)) |
91 | | ang180lem1.2 |
. . . . . . . . . . 11
⊢ 𝑇 = (((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) |
92 | 91 | fveq2i 6720 |
. . . . . . . . . 10
⊢
(ℑ‘𝑇) =
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) |
93 | 63, 66 | imaddd 14778 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = ((ℑ‘((log‘(1 / (1
− 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) +
(ℑ‘(log‘𝐴)))) |
94 | 92, 93 | syl5eq 2790 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) =
((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴)))) |
95 | 83, 90, 94 | 3brtr4d 5085 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) <
(ℑ‘𝑇)) |
96 | 63, 66 | addcld 10852 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) ∈ ℂ) |
97 | 91, 96 | eqeltrid 2842 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑇 ∈ ℂ) |
98 | | imval 14670 |
. . . . . . . . . 10
⊢ (𝑇 ∈ ℂ →
(ℑ‘𝑇) =
(ℜ‘(𝑇 /
i))) |
99 | 97, 98 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) = (ℜ‘(𝑇 / i))) |
100 | | ang.1 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0})
↦ (ℑ‘(log‘(𝑦 / 𝑥)))) |
101 | | ang180lem1.3 |
. . . . . . . . . . . 12
⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 /
2)) |
102 | 100, 91, 101 | ang180lem1 25692 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑁 ∈ ℤ ∧ (𝑇 / i) ∈ ℝ)) |
103 | 102 | simprd 499 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ∈ ℝ) |
104 | 103 | rered 14787 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℜ‘(𝑇 / i)) = (𝑇 / i)) |
105 | 99, 104 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) = (𝑇 / i)) |
106 | 95, 105 | breqtrd 5079 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) <
(𝑇 / i)) |
107 | 36, 106 | eqbrtrid 5088 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(3 / 2) · (2
· π)) < (𝑇 /
i)) |
108 | 20 | renegcli 11139 |
. . . . . . . 8
⊢ -(3 / 2)
∈ ℝ |
109 | 108 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(3 / 2) ∈
ℝ) |
110 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ∈
ℝ) |
111 | | 2pos 11933 |
. . . . . . . . 9
⊢ 0 <
2 |
112 | | pipos 25350 |
. . . . . . . . 9
⊢ 0 <
π |
113 | 30, 31, 111, 112 | mulgt0ii 10965 |
. . . . . . . 8
⊢ 0 < (2
· π) |
114 | 113 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 < (2 ·
π)) |
115 | | ltmuldiv 11705 |
. . . . . . 7
⊢ ((-(3 /
2) ∈ ℝ ∧ (𝑇
/ i) ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2
· π))) → ((-(3 / 2) · (2 · π)) < (𝑇 / i) ↔ -(3 / 2) <
((𝑇 / i) / (2 ·
π)))) |
116 | 109, 103,
110, 114, 115 | syl112anc 1376 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((-(3 / 2) · (2
· π)) < (𝑇 /
i) ↔ -(3 / 2) < ((𝑇
/ i) / (2 · π)))) |
117 | 107, 116 | mpbid 235 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(3 / 2) < ((𝑇 / i) / (2 ·
π))) |
118 | 18, 117 | eqbrtrid 5088 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 + (1 / 2)) < ((𝑇 / i) / (2 ·
π))) |
119 | 30 | renegcli 11139 |
. . . . . 6
⊢ -2 ∈
ℝ |
120 | 119 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 ∈
ℝ) |
121 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / 2) ∈
ℝ) |
122 | 32, 113 | gt0ne0ii 11368 |
. . . . . . 7
⊢ (2
· π) ≠ 0 |
123 | 122 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ≠
0) |
124 | 103, 110,
123 | redivcld 11660 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) ∈
ℝ) |
125 | 120, 121,
124 | ltaddsubd 11432 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((-2 + (1 / 2)) < ((𝑇 / i) / (2 · π))
↔ -2 < (((𝑇 / i) /
(2 · π)) − (1 / 2)))) |
126 | 118, 125 | mpbid 235 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 < (((𝑇 / i) / (2 · π)) − (1 /
2))) |
127 | 126, 101 | breqtrrdi 5095 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 < 𝑁) |
128 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → π ∈
ℝ) |
129 | 70 | simprd 499 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘(1
/ (1 − 𝐴)))) ≤
π) |
130 | 72 | simprd 499 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘((𝐴 − 1) / 𝐴))) ≤ π) |
131 | 68, 69, 128, 128, 129, 130 | le2addd 11451 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
((ℑ‘(log‘(1 / (1 − 𝐴)))) + (ℑ‘(log‘((𝐴 − 1) / 𝐴)))) ≤ (π + π)) |
132 | 22 | 2timesi 11968 |
. . . . . . . . . . . 12
⊢ (2
· π) = (π + π) |
133 | 132 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) = (π +
π)) |
134 | 131, 78, 133 | 3brtr4d 5085 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ≤ (2 ·
π)) |
135 | 81 | simprd 499 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘𝐴)) ≤ π) |
136 | 64, 67, 110, 128, 134, 135 | le2addd 11451 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))) ≤ ((2 · π) +
π)) |
137 | 105, 94 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) = ((ℑ‘((log‘(1 / (1
− 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) +
(ℑ‘(log‘𝐴)))) |
138 | 84 | oveq1i 7223 |
. . . . . . . . . . 11
⊢ (3
· π) = ((2 + 1) · π) |
139 | 1, 9, 22 | adddiri 10846 |
. . . . . . . . . . 11
⊢ ((2 + 1)
· π) = ((2 · π) + (1 · π)) |
140 | 22 | mulid2i 10838 |
. . . . . . . . . . . 12
⊢ (1
· π) = π |
141 | 140 | oveq2i 7224 |
. . . . . . . . . . 11
⊢ ((2
· π) + (1 · π)) = ((2 · π) +
π) |
142 | 138, 139,
141 | 3eqtri 2769 |
. . . . . . . . . 10
⊢ (3
· π) = ((2 · π) + π) |
143 | 142 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · π) = ((2
· π) + π)) |
144 | 136, 137,
143 | 3brtr4d 5085 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ≤ (3 ·
π)) |
145 | 33 | subid1i 11150 |
. . . . . . . . . 10
⊢ ((2
· π) − 0) = (2 · π) |
146 | 145, 122 | eqnetri 3011 |
. . . . . . . . 9
⊢ ((2
· π) − 0) ≠ 0 |
147 | | negsub 11126 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 + -𝐴) = (1 − 𝐴)) |
148 | 9, 41, 147 | sylancr 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 + -𝐴) = (1 − 𝐴)) |
149 | 148 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 + -𝐴) = (1 − 𝐴)) |
150 | | 1rp 12590 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ+ |
151 | 143, 137 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) −
(𝑇 / i)) = (((2 ·
π) + π) − ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))))) |
152 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ∈
ℂ) |
153 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → π ∈
ℂ) |
154 | 64 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℂ) |
155 | 67 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
156 | 152, 153,
154, 155 | addsub4d 11236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((2 · π) + π)
− ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴)))) = (((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴))))) |
157 | 151, 156 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) −
(𝑇 / i)) = (((2 ·
π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴))))) |
158 | 157 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((3 · π)
− (𝑇 / i)) = (((2
· π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴))))) |
159 | 19, 31 | remulcli 10849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (3
· π) ∈ ℝ |
160 | 159 | recni 10847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (3
· π) ∈ ℂ |
161 | | ax-icn 10788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ i ∈
ℂ |
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → i ∈
ℂ) |
163 | | ine0 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ i ≠
0 |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → i ≠ 0) |
165 | 97, 162, 164 | divcld 11608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ∈ ℂ) |
166 | | subeq0 11104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((3
· π) ∈ ℂ ∧ (𝑇 / i) ∈ ℂ) → (((3 ·
π) − (𝑇 / i)) = 0
↔ (3 · π) = (𝑇 / i))) |
167 | 160, 165,
166 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((3 · π) −
(𝑇 / i)) = 0 ↔ (3
· π) = (𝑇 /
i))) |
168 | 167 | biimpar 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((3 · π)
− (𝑇 / i)) =
0) |
169 | 158, 168 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (((2 ·
π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴)))) = 0) |
170 | | resubcl 11142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((2
· π) ∈ ℝ ∧ (ℑ‘((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ) → ((2 ·
π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ∈ ℝ) |
171 | 32, 64, 170 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ∈ ℝ) |
172 | | subge0 11345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((2
· π) ∈ ℝ ∧ (ℑ‘((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ) → (0 ≤ ((2
· π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ↔ (ℑ‘((log‘(1 /
(1 − 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) ≤ (2 ·
π))) |
173 | 32, 64, 172 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (0 ≤ ((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ↔ (ℑ‘((log‘(1 /
(1 − 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) ≤ (2 ·
π))) |
174 | 134, 173 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 ≤ ((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))))) |
175 | | resubcl 11142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (π −
(ℑ‘(log‘𝐴))) ∈ ℝ) |
176 | 31, 67, 175 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (π −
(ℑ‘(log‘𝐴))) ∈ ℝ) |
177 | | subge0 11345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (0 ≤ (π
− (ℑ‘(log‘𝐴))) ↔ (ℑ‘(log‘𝐴)) ≤ π)) |
178 | 31, 67, 177 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (0 ≤ (π −
(ℑ‘(log‘𝐴))) ↔ (ℑ‘(log‘𝐴)) ≤ π)) |
179 | 135, 178 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 ≤ (π −
(ℑ‘(log‘𝐴)))) |
180 | | add20 11344 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((((2
· π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ∈ ℝ ∧ 0 ≤ ((2
· π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))))) ∧ ((π −
(ℑ‘(log‘𝐴))) ∈ ℝ ∧ 0 ≤ (π
− (ℑ‘(log‘𝐴))))) → ((((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴)))) = 0 ↔ (((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π −
(ℑ‘(log‘𝐴))) = 0))) |
181 | 171, 174,
176, 179, 180 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴)))) = 0 ↔ (((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π −
(ℑ‘(log‘𝐴))) = 0))) |
182 | 181 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴)))) = 0) → (((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π −
(ℑ‘(log‘𝐴))) = 0)) |
183 | 169, 182 | syldan 594 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (((2 ·
π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π −
(ℑ‘(log‘𝐴))) = 0)) |
184 | 183 | simprd 499 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (π −
(ℑ‘(log‘𝐴))) = 0) |
185 | 155 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
186 | | subeq0 11104 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((π
∈ ℂ ∧ (ℑ‘(log‘𝐴)) ∈ ℂ) → ((π −
(ℑ‘(log‘𝐴))) = 0 ↔ π =
(ℑ‘(log‘𝐴)))) |
187 | 22, 185, 186 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((π −
(ℑ‘(log‘𝐴))) = 0 ↔ π =
(ℑ‘(log‘𝐴)))) |
188 | 184, 187 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → π =
(ℑ‘(log‘𝐴))) |
189 | 188 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) →
(ℑ‘(log‘𝐴)) = π) |
190 | | lognegb 25478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) |
191 | 190 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-𝐴 ∈ ℝ+ ↔
(ℑ‘(log‘𝐴)) = π)) |
192 | 191 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) |
193 | 189, 192 | mpbird 260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → -𝐴 ∈
ℝ+) |
194 | | rpaddcl 12608 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ+ ∧ -𝐴 ∈ ℝ+) → (1 +
-𝐴) ∈
ℝ+) |
195 | 150, 193,
194 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 + -𝐴) ∈
ℝ+) |
196 | 149, 195 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 − 𝐴) ∈
ℝ+) |
197 | 196 | rpreccld 12638 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 / (1 −
𝐴)) ∈
ℝ+) |
198 | 197 | relogcld 25511 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (log‘(1 / (1
− 𝐴))) ∈
ℝ) |
199 | | negsubdi2 11137 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝐴 −
1) = (1 − 𝐴)) |
200 | 41, 9, 199 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(𝐴 − 1) = (1 − 𝐴)) |
201 | 200 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(𝐴 − 1) / -𝐴) = ((1 − 𝐴) / -𝐴)) |
202 | 54, 41, 55 | div2negd 11623 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(𝐴 − 1) / -𝐴) = ((𝐴 − 1) / 𝐴)) |
203 | 201, 202 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) / -𝐴) = ((𝐴 − 1) / 𝐴)) |
204 | 203 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((1 − 𝐴) / -𝐴) = ((𝐴 − 1) / 𝐴)) |
205 | 196, 193 | rpdivcld 12645 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((1 − 𝐴) / -𝐴) ∈
ℝ+) |
206 | 204, 205 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((𝐴 − 1) / 𝐴) ∈
ℝ+) |
207 | 206 | relogcld 25511 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (log‘((𝐴 − 1) / 𝐴)) ∈ ℝ) |
208 | 198, 207 | readdcld 10862 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((log‘(1 /
(1 − 𝐴))) +
(log‘((𝐴 − 1) /
𝐴))) ∈
ℝ) |
209 | 208 | reim0d 14788 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) = 0) |
210 | 209 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = ((2 · π) −
0)) |
211 | 183 | simpld 498 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0) |
212 | 210, 211 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π)
− 0) = 0) |
213 | 212 | ex 416 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) = (𝑇 / i) → ((2 · π)
− 0) = 0)) |
214 | 213 | necon3d 2961 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((2 · π) −
0) ≠ 0 → (3 · π) ≠ (𝑇 / i))) |
215 | 146, 214 | mpi 20 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · π) ≠
(𝑇 / i)) |
216 | | ltlen 10933 |
. . . . . . . . 9
⊢ (((𝑇 / i) ∈ ℝ ∧ (3
· π) ∈ ℝ) → ((𝑇 / i) < (3 · π) ↔ ((𝑇 / i) ≤ (3 · π)
∧ (3 · π) ≠ (𝑇 / i)))) |
217 | 103, 159,
216 | sylancl 589 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) < (3 · π) ↔ ((𝑇 / i) ≤ (3 · π)
∧ (3 · π) ≠ (𝑇 / i)))) |
218 | 144, 215,
217 | mpbir2and 713 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) < (3 ·
π)) |
219 | 218, 28 | breqtrrdi 5095 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) < ((3 / 2) · (2 ·
π))) |
220 | 20 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 / 2) ∈
ℝ) |
221 | | ltdivmul2 11709 |
. . . . . . 7
⊢ (((𝑇 / i) ∈ ℝ ∧ (3 /
2) ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2
· π))) → (((𝑇 / i) / (2 · π)) < (3 / 2)
↔ (𝑇 / i) < ((3 /
2) · (2 · π)))) |
222 | 103, 220,
110, 114, 221 | syl112anc 1376 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((𝑇 / i) / (2 · π)) < (3 / 2)
↔ (𝑇 / i) < ((3 /
2) · (2 · π)))) |
223 | 219, 222 | mpbird 260 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) < (3 /
2)) |
224 | 84 | oveq1i 7223 |
. . . . . 6
⊢ (3 / 2) =
((2 + 1) / 2) |
225 | 1, 9, 1, 25 | divdiri 11589 |
. . . . . 6
⊢ ((2 + 1)
/ 2) = ((2 / 2) + (1 / 2)) |
226 | | 2div2e1 11971 |
. . . . . . 7
⊢ (2 / 2) =
1 |
227 | 226 | oveq1i 7223 |
. . . . . 6
⊢ ((2 / 2)
+ (1 / 2)) = (1 + (1 / 2)) |
228 | 224, 225,
227 | 3eqtri 2769 |
. . . . 5
⊢ (3 / 2) =
(1 + (1 / 2)) |
229 | 223, 228 | breqtrdi 5094 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) < (1 + (1 /
2))) |
230 | 2 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ∈
ℝ) |
231 | 124, 121,
230 | ltsubaddd 11428 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((𝑇 / i) / (2 · π)) − (1 / 2))
< 1 ↔ ((𝑇 / i) / (2
· π)) < (1 + (1 / 2)))) |
232 | 229, 231 | mpbird 260 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((𝑇 / i) / (2 · π)) − (1 / 2))
< 1) |
233 | 101, 232 | eqbrtrid 5088 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑁 < 1) |
234 | 127, 233 | jca 515 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 < 𝑁 ∧ 𝑁 < 1)) |