Proof of Theorem ang180lem2
Step | Hyp | Ref
| Expression |
1 | | 2cn 10968 |
. . . . . . 7
⊢ 2 ∈
ℂ |
2 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
3 | 2 | rehalfcli 11158 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
4 | 3 | recni 9931 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
5 | 1, 4 | negsubdii 10245 |
. . . . . 6
⊢ -(2
− (1 / 2)) = (-2 + (1 / 2)) |
6 | | 4d2e2 11061 |
. . . . . . . . 9
⊢ (4 / 2) =
2 |
7 | 6 | oveq1i 6559 |
. . . . . . . 8
⊢ ((4 / 2)
− (1 / 2)) = (2 − (1 / 2)) |
8 | | 4cn 10975 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
9 | | ax-1cn 9873 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
10 | | 2cnne0 11119 |
. . . . . . . . . 10
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
11 | | divsubdir 10600 |
. . . . . . . . . 10
⊢ ((4
∈ ℂ ∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
→ ((4 − 1) / 2) = ((4 / 2) − (1 / 2))) |
12 | 8, 9, 10, 11 | mp3an 1416 |
. . . . . . . . 9
⊢ ((4
− 1) / 2) = ((4 / 2) − (1 / 2)) |
13 | | 3cn 10972 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
14 | 9, 13 | addcomi 10106 |
. . . . . . . . . . . 12
⊢ (1 + 3) =
(3 + 1) |
15 | | df-4 10958 |
. . . . . . . . . . . 12
⊢ 4 = (3 +
1) |
16 | 14, 15 | eqtr4i 2635 |
. . . . . . . . . . 11
⊢ (1 + 3) =
4 |
17 | 8, 9, 13, 16 | subaddrii 10249 |
. . . . . . . . . 10
⊢ (4
− 1) = 3 |
18 | 17 | oveq1i 6559 |
. . . . . . . . 9
⊢ ((4
− 1) / 2) = (3 / 2) |
19 | 12, 18 | eqtr3i 2634 |
. . . . . . . 8
⊢ ((4 / 2)
− (1 / 2)) = (3 / 2) |
20 | 7, 19 | eqtr3i 2634 |
. . . . . . 7
⊢ (2
− (1 / 2)) = (3 / 2) |
21 | 20 | negeqi 10153 |
. . . . . 6
⊢ -(2
− (1 / 2)) = -(3 / 2) |
22 | 5, 21 | eqtr3i 2634 |
. . . . 5
⊢ (-2 + (1
/ 2)) = -(3 / 2) |
23 | | 3re 10971 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
24 | 23 | rehalfcli 11158 |
. . . . . . . . . . . 12
⊢ (3 / 2)
∈ ℝ |
25 | 24 | recni 9931 |
. . . . . . . . . . 11
⊢ (3 / 2)
∈ ℂ |
26 | | picn 24015 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
27 | 25, 1, 26 | mulassi 9928 |
. . . . . . . . . 10
⊢ (((3 / 2)
· 2) · π) = ((3 / 2) · (2 ·
π)) |
28 | | 2ne0 10990 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
29 | 13, 1, 28 | divcan1i 10648 |
. . . . . . . . . . 11
⊢ ((3 / 2)
· 2) = 3 |
30 | 29 | oveq1i 6559 |
. . . . . . . . . 10
⊢ (((3 / 2)
· 2) · π) = (3 · π) |
31 | 27, 30 | eqtr3i 2634 |
. . . . . . . . 9
⊢ ((3 / 2)
· (2 · π)) = (3 · π) |
32 | 31 | negeqi 10153 |
. . . . . . . 8
⊢ -((3 / 2)
· (2 · π)) = -(3 · π) |
33 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
34 | | pire 24014 |
. . . . . . . . . . 11
⊢ π
∈ ℝ |
35 | 33, 34 | remulcli 9933 |
. . . . . . . . . 10
⊢ (2
· π) ∈ ℝ |
36 | 35 | recni 9931 |
. . . . . . . . 9
⊢ (2
· π) ∈ ℂ |
37 | 25, 36 | mulneg1i 10355 |
. . . . . . . 8
⊢ (-(3 / 2)
· (2 · π)) = -((3 / 2) · (2 ·
π)) |
38 | 13, 26 | mulneg2i 10356 |
. . . . . . . 8
⊢ (3
· -π) = -(3 · π) |
39 | 32, 37, 38 | 3eqtr4i 2642 |
. . . . . . 7
⊢ (-(3 / 2)
· (2 · π)) = (3 · -π) |
40 | 34 | renegcli 10221 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ |
41 | 33, 40 | remulcli 9933 |
. . . . . . . . . . 11
⊢ (2
· -π) ∈ ℝ |
42 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) ∈
ℝ) |
43 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π ∈
ℝ) |
44 | | simp1 1054 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ∈ ℂ) |
45 | | subcl 10159 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) |
46 | 9, 44, 45 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ∈ ℂ) |
47 | | simp3 1056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 1) |
48 | 47 | necomd 2837 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ≠ 𝐴) |
49 | | subeq0 10186 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
50 | 9, 44, 49 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
51 | 50 | necon3bid 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) ≠ 0 ↔ 1 ≠ 𝐴)) |
52 | 48, 51 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ≠ 0) |
53 | 46, 52 | reccld 10673 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ∈
ℂ) |
54 | 46, 52 | recne0d 10674 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ≠ 0) |
55 | 53, 54 | logcld 24121 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘(1 / (1 −
𝐴))) ∈
ℂ) |
56 | | subcl 10159 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) |
57 | 44, 9, 56 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ∈ ℂ) |
58 | | simp2 1055 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 0) |
59 | 57, 44, 58 | divcld 10680 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ∈ ℂ) |
60 | | subeq0 10186 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 −
1) = 0 ↔ 𝐴 =
1)) |
61 | 44, 9, 60 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) = 0 ↔ 𝐴 = 1)) |
62 | 61 | necon3bid 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) ≠ 0 ↔ 𝐴 ≠ 1)) |
63 | 47, 62 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ≠ 0) |
64 | 57, 44, 63, 58 | divne0d 10696 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ≠ 0) |
65 | 59, 64 | logcld 24121 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘((𝐴 − 1) / 𝐴)) ∈ ℂ) |
66 | 55, 65 | addcld 9938 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) ∈ ℂ) |
67 | 66 | imcld 13783 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ) |
68 | | logcl 24119 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
69 | 68 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘𝐴) ∈ ℂ) |
70 | 69 | imcld 13783 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘𝐴)) ∈ ℝ) |
71 | 55 | imcld 13783 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘(1
/ (1 − 𝐴)))) ∈
ℝ) |
72 | 65 | imcld 13783 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘((𝐴 − 1) / 𝐴))) ∈ ℝ) |
73 | 53, 54 | logimcld 24122 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π <
(ℑ‘(log‘(1 / (1 − 𝐴)))) ∧ (ℑ‘(log‘(1 / (1
− 𝐴)))) ≤
π)) |
74 | 73 | simpld 474 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π <
(ℑ‘(log‘(1 / (1 − 𝐴))))) |
75 | 59, 64 | logimcld 24122 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π <
(ℑ‘(log‘((𝐴 − 1) / 𝐴))) ∧ (ℑ‘(log‘((𝐴 − 1) / 𝐴))) ≤ π)) |
76 | 75 | simpld 474 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π <
(ℑ‘(log‘((𝐴 − 1) / 𝐴)))) |
77 | 43, 43, 71, 72, 74, 76 | lt2addd 10529 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π + -π) <
((ℑ‘(log‘(1 / (1 − 𝐴)))) + (ℑ‘(log‘((𝐴 − 1) / 𝐴))))) |
78 | | negpicn 24018 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℂ |
79 | 78 | 2timesi 11024 |
. . . . . . . . . . . 12
⊢ (2
· -π) = (-π + -π) |
80 | 79 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) = (-π
+ -π)) |
81 | 55, 65 | imaddd 13803 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) = ((ℑ‘(log‘(1 / (1
− 𝐴)))) +
(ℑ‘(log‘((𝐴 − 1) / 𝐴))))) |
82 | 77, 80, 81 | 3brtr4d 4615 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) <
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) |
83 | | logimcl 24120 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
84 | 83 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
85 | 84 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π <
(ℑ‘(log‘𝐴))) |
86 | 42, 43, 67, 70, 82, 85 | lt2addd 10529 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((2 · -π) + -π)
< ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴)))) |
87 | | df-3 10957 |
. . . . . . . . . . . 12
⊢ 3 = (2 +
1) |
88 | 87 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ (3
· -π) = ((2 + 1) · -π) |
89 | 1, 9, 78 | adddiri 9930 |
. . . . . . . . . . 11
⊢ ((2 + 1)
· -π) = ((2 · -π) + (1 · -π)) |
90 | 78 | mulid2i 9922 |
. . . . . . . . . . . 12
⊢ (1
· -π) = -π |
91 | 90 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ ((2
· -π) + (1 · -π)) = ((2 · -π) +
-π) |
92 | 88, 89, 91 | 3eqtri 2636 |
. . . . . . . . . 10
⊢ (3
· -π) = ((2 · -π) + -π) |
93 | 92 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) = ((2
· -π) + -π)) |
94 | | ang180lem1.2 |
. . . . . . . . . . 11
⊢ 𝑇 = (((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) |
95 | 94 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(ℑ‘𝑇) =
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) |
96 | 66, 69 | imaddd 13803 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = ((ℑ‘((log‘(1 / (1
− 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) +
(ℑ‘(log‘𝐴)))) |
97 | 95, 96 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) =
((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴)))) |
98 | 86, 93, 97 | 3brtr4d 4615 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) <
(ℑ‘𝑇)) |
99 | 66, 69 | addcld 9938 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) ∈ ℂ) |
100 | 94, 99 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑇 ∈ ℂ) |
101 | | imval 13695 |
. . . . . . . . . 10
⊢ (𝑇 ∈ ℂ →
(ℑ‘𝑇) =
(ℜ‘(𝑇 /
i))) |
102 | 100, 101 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) = (ℜ‘(𝑇 / i))) |
103 | | ang.1 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0})
↦ (ℑ‘(log‘(𝑦 / 𝑥)))) |
104 | | ang180lem1.3 |
. . . . . . . . . . . 12
⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 /
2)) |
105 | 103, 94, 104 | ang180lem1 24339 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑁 ∈ ℤ ∧ (𝑇 / i) ∈ ℝ)) |
106 | 105 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ∈ ℝ) |
107 | 106 | rered 13812 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℜ‘(𝑇 / i)) = (𝑇 / i)) |
108 | 102, 107 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) = (𝑇 / i)) |
109 | 98, 108 | breqtrd 4609 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) <
(𝑇 / i)) |
110 | 39, 109 | syl5eqbr 4618 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(3 / 2) · (2
· π)) < (𝑇 /
i)) |
111 | 24 | renegcli 10221 |
. . . . . . . 8
⊢ -(3 / 2)
∈ ℝ |
112 | 111 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(3 / 2) ∈
ℝ) |
113 | 35 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ∈
ℝ) |
114 | | 2pos 10989 |
. . . . . . . . 9
⊢ 0 <
2 |
115 | | pipos 24016 |
. . . . . . . . 9
⊢ 0 <
π |
116 | 33, 34, 114, 115 | mulgt0ii 10049 |
. . . . . . . 8
⊢ 0 < (2
· π) |
117 | 116 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 < (2 ·
π)) |
118 | | ltmuldiv 10775 |
. . . . . . 7
⊢ ((-(3 /
2) ∈ ℝ ∧ (𝑇
/ i) ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2
· π))) → ((-(3 / 2) · (2 · π)) < (𝑇 / i) ↔ -(3 / 2) <
((𝑇 / i) / (2 ·
π)))) |
119 | 112, 106,
113, 117, 118 | syl112anc 1322 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((-(3 / 2) · (2
· π)) < (𝑇 /
i) ↔ -(3 / 2) < ((𝑇
/ i) / (2 · π)))) |
120 | 110, 119 | mpbid 221 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(3 / 2) < ((𝑇 / i) / (2 ·
π))) |
121 | 22, 120 | syl5eqbr 4618 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 + (1 / 2)) < ((𝑇 / i) / (2 ·
π))) |
122 | 33 | renegcli 10221 |
. . . . . 6
⊢ -2 ∈
ℝ |
123 | 122 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 ∈
ℝ) |
124 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / 2) ∈
ℝ) |
125 | 35, 116 | gt0ne0ii 10443 |
. . . . . . 7
⊢ (2
· π) ≠ 0 |
126 | 125 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ≠
0) |
127 | 106, 113,
126 | redivcld 10732 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) ∈
ℝ) |
128 | 123, 124,
127 | ltaddsubd 10506 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((-2 + (1 / 2)) < ((𝑇 / i) / (2 · π))
↔ -2 < (((𝑇 / i) /
(2 · π)) − (1 / 2)))) |
129 | 121, 128 | mpbid 221 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 < (((𝑇 / i) / (2 · π)) − (1 /
2))) |
130 | 129, 104 | syl6breqr 4625 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 < 𝑁) |
131 | 34 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → π ∈
ℝ) |
132 | 73 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘(1
/ (1 − 𝐴)))) ≤
π) |
133 | 75 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘((𝐴 − 1) / 𝐴))) ≤ π) |
134 | 71, 72, 131, 131, 132, 133 | le2addd 10525 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
((ℑ‘(log‘(1 / (1 − 𝐴)))) + (ℑ‘(log‘((𝐴 − 1) / 𝐴)))) ≤ (π + π)) |
135 | 26 | 2timesi 11024 |
. . . . . . . . . . . 12
⊢ (2
· π) = (π + π) |
136 | 135 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) = (π +
π)) |
137 | 134, 81, 136 | 3brtr4d 4615 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ≤ (2 ·
π)) |
138 | 84 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘𝐴)) ≤ π) |
139 | 67, 70, 113, 131, 137, 138 | le2addd 10525 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))) ≤ ((2 · π) +
π)) |
140 | 108, 97 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) = ((ℑ‘((log‘(1 / (1
− 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) +
(ℑ‘(log‘𝐴)))) |
141 | 87 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ (3
· π) = ((2 + 1) · π) |
142 | 1, 9, 26 | adddiri 9930 |
. . . . . . . . . . 11
⊢ ((2 + 1)
· π) = ((2 · π) + (1 · π)) |
143 | 26 | mulid2i 9922 |
. . . . . . . . . . . 12
⊢ (1
· π) = π |
144 | 143 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ ((2
· π) + (1 · π)) = ((2 · π) +
π) |
145 | 141, 142,
144 | 3eqtri 2636 |
. . . . . . . . . 10
⊢ (3
· π) = ((2 · π) + π) |
146 | 145 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · π) = ((2
· π) + π)) |
147 | 139, 140,
146 | 3brtr4d 4615 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ≤ (3 ·
π)) |
148 | 36 | subid1i 10232 |
. . . . . . . . . 10
⊢ ((2
· π) − 0) = (2 · π) |
149 | 148, 125 | eqnetri 2852 |
. . . . . . . . 9
⊢ ((2
· π) − 0) ≠ 0 |
150 | | negsub 10208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 + -𝐴) = (1 − 𝐴)) |
151 | 9, 44, 150 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 + -𝐴) = (1 − 𝐴)) |
152 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 + -𝐴) = (1 − 𝐴)) |
153 | | 1rp 11712 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ+ |
154 | 146, 140 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) −
(𝑇 / i)) = (((2 ·
π) + π) − ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))))) |
155 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ∈
ℂ) |
156 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → π ∈
ℂ) |
157 | 67 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℂ) |
158 | 70 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
159 | 155, 156,
157, 158 | addsub4d 10318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((2 · π) + π)
− ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴)))) = (((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴))))) |
160 | 154, 159 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) −
(𝑇 / i)) = (((2 ·
π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴))))) |
161 | 160 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((3 · π)
− (𝑇 / i)) = (((2
· π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴))))) |
162 | 23, 34 | remulcli 9933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (3
· π) ∈ ℝ |
163 | 162 | recni 9931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (3
· π) ∈ ℂ |
164 | | ax-icn 9874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ i ∈
ℂ |
165 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → i ∈
ℂ) |
166 | | ine0 10344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ i ≠
0 |
167 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → i ≠ 0) |
168 | 100, 165,
167 | divcld 10680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ∈ ℂ) |
169 | | subeq0 10186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((3
· π) ∈ ℂ ∧ (𝑇 / i) ∈ ℂ) → (((3 ·
π) − (𝑇 / i)) = 0
↔ (3 · π) = (𝑇 / i))) |
170 | 163, 168,
169 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((3 · π) −
(𝑇 / i)) = 0 ↔ (3
· π) = (𝑇 /
i))) |
171 | 170 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((3 · π)
− (𝑇 / i)) =
0) |
172 | 161, 171 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (((2 ·
π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴)))) = 0) |
173 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((2
· π) ∈ ℝ ∧ (ℑ‘((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ) → ((2 ·
π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ∈ ℝ) |
174 | 35, 67, 173 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ∈ ℝ) |
175 | | subge0 10420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((2
· π) ∈ ℝ ∧ (ℑ‘((log‘(1 / (1 −
𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ) → (0 ≤ ((2
· π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ↔ (ℑ‘((log‘(1 /
(1 − 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) ≤ (2 ·
π))) |
176 | 35, 67, 175 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (0 ≤ ((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ↔ (ℑ‘((log‘(1 /
(1 − 𝐴))) +
(log‘((𝐴 − 1) /
𝐴)))) ≤ (2 ·
π))) |
177 | 137, 176 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 ≤ ((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))))) |
178 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (π −
(ℑ‘(log‘𝐴))) ∈ ℝ) |
179 | 34, 70, 178 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (π −
(ℑ‘(log‘𝐴))) ∈ ℝ) |
180 | | subge0 10420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (0 ≤ (π
− (ℑ‘(log‘𝐴))) ↔ (ℑ‘(log‘𝐴)) ≤ π)) |
181 | 34, 70, 180 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (0 ≤ (π −
(ℑ‘(log‘𝐴))) ↔ (ℑ‘(log‘𝐴)) ≤ π)) |
182 | 138, 181 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 ≤ (π −
(ℑ‘(log‘𝐴)))) |
183 | | add20 10419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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))) |
184 | 174, 177,
179, 182, 183 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴)))) = 0 ↔ (((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π −
(ℑ‘(log‘𝐴))) = 0))) |
185 | 184 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π −
(ℑ‘(log‘𝐴)))) = 0) → (((2 · π) −
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π −
(ℑ‘(log‘𝐴))) = 0)) |
186 | 172, 185 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (((2 ·
π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π −
(ℑ‘(log‘𝐴))) = 0)) |
187 | 186 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (π −
(ℑ‘(log‘𝐴))) = 0) |
188 | 158 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
189 | | subeq0 10186 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((π
∈ ℂ ∧ (ℑ‘(log‘𝐴)) ∈ ℂ) → ((π −
(ℑ‘(log‘𝐴))) = 0 ↔ π =
(ℑ‘(log‘𝐴)))) |
190 | 26, 188, 189 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((π −
(ℑ‘(log‘𝐴))) = 0 ↔ π =
(ℑ‘(log‘𝐴)))) |
191 | 187, 190 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → π =
(ℑ‘(log‘𝐴))) |
192 | 191 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) →
(ℑ‘(log‘𝐴)) = π) |
193 | | lognegb 24140 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) |
194 | 193 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-𝐴 ∈ ℝ+ ↔
(ℑ‘(log‘𝐴)) = π)) |
195 | 194 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (-𝐴 ∈ ℝ+
↔ (ℑ‘(log‘𝐴)) = π)) |
196 | 192, 195 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → -𝐴 ∈
ℝ+) |
197 | | rpaddcl 11730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ+ ∧ -𝐴 ∈ ℝ+) → (1 +
-𝐴) ∈
ℝ+) |
198 | 153, 196,
197 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 + -𝐴) ∈
ℝ+) |
199 | 152, 198 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 − 𝐴) ∈
ℝ+) |
200 | 199 | rpreccld 11758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 / (1 −
𝐴)) ∈
ℝ+) |
201 | 200 | relogcld 24173 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (log‘(1 / (1
− 𝐴))) ∈
ℝ) |
202 | | negsubdi2 10219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝐴 −
1) = (1 − 𝐴)) |
203 | 44, 9, 202 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(𝐴 − 1) = (1 − 𝐴)) |
204 | 203 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(𝐴 − 1) / -𝐴) = ((1 − 𝐴) / -𝐴)) |
205 | 57, 44, 58 | div2negd 10695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(𝐴 − 1) / -𝐴) = ((𝐴 − 1) / 𝐴)) |
206 | 204, 205 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) / -𝐴) = ((𝐴 − 1) / 𝐴)) |
207 | 206 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((1 − 𝐴) / -𝐴) = ((𝐴 − 1) / 𝐴)) |
208 | 199, 196 | rpdivcld 11765 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((1 − 𝐴) / -𝐴) ∈
ℝ+) |
209 | 207, 208 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((𝐴 − 1) / 𝐴) ∈
ℝ+) |
210 | 209 | relogcld 24173 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (log‘((𝐴 − 1) / 𝐴)) ∈ ℝ) |
211 | 201, 210 | readdcld 9948 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((log‘(1 /
(1 − 𝐴))) +
(log‘((𝐴 − 1) /
𝐴))) ∈
ℝ) |
212 | 211 | reim0d 13813 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) →
(ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) = 0) |
213 | 212 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = ((2 · π) −
0)) |
214 | 186 | simpld 474 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π)
− (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0) |
215 | 213, 214 | eqtr3d 2646 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π)
− 0) = 0) |
216 | 215 | ex 449 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) = (𝑇 / i) → ((2 · π)
− 0) = 0)) |
217 | 216 | necon3d 2803 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((2 · π) −
0) ≠ 0 → (3 · π) ≠ (𝑇 / i))) |
218 | 149, 217 | mpi 20 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · π) ≠
(𝑇 / i)) |
219 | | ltlen 10017 |
. . . . . . . . 9
⊢ (((𝑇 / i) ∈ ℝ ∧ (3
· π) ∈ ℝ) → ((𝑇 / i) < (3 · π) ↔ ((𝑇 / i) ≤ (3 · π)
∧ (3 · π) ≠ (𝑇 / i)))) |
220 | 106, 162,
219 | sylancl 693 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) < (3 · π) ↔ ((𝑇 / i) ≤ (3 · π)
∧ (3 · π) ≠ (𝑇 / i)))) |
221 | 147, 218,
220 | mpbir2and 959 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) < (3 ·
π)) |
222 | 221, 31 | syl6breqr 4625 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) < ((3 / 2) · (2 ·
π))) |
223 | 24 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 / 2) ∈
ℝ) |
224 | | ltdivmul2 10779 |
. . . . . . 7
⊢ (((𝑇 / i) ∈ ℝ ∧ (3 /
2) ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2
· π))) → (((𝑇 / i) / (2 · π)) < (3 / 2)
↔ (𝑇 / i) < ((3 /
2) · (2 · π)))) |
225 | 106, 223,
113, 117, 224 | syl112anc 1322 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((𝑇 / i) / (2 · π)) < (3 / 2)
↔ (𝑇 / i) < ((3 /
2) · (2 · π)))) |
226 | 222, 225 | mpbird 246 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) < (3 /
2)) |
227 | 87 | oveq1i 6559 |
. . . . . 6
⊢ (3 / 2) =
((2 + 1) / 2) |
228 | 1, 9, 1, 28 | divdiri 10661 |
. . . . . 6
⊢ ((2 + 1)
/ 2) = ((2 / 2) + (1 / 2)) |
229 | | 2div2e1 11027 |
. . . . . . 7
⊢ (2 / 2) =
1 |
230 | 229 | oveq1i 6559 |
. . . . . 6
⊢ ((2 / 2)
+ (1 / 2)) = (1 + (1 / 2)) |
231 | 227, 228,
230 | 3eqtri 2636 |
. . . . 5
⊢ (3 / 2) =
(1 + (1 / 2)) |
232 | 226, 231 | syl6breq 4624 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) < (1 + (1 /
2))) |
233 | 2 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ∈
ℝ) |
234 | 127, 124,
233 | ltsubaddd 10502 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((𝑇 / i) / (2 · π)) − (1 / 2))
< 1 ↔ ((𝑇 / i) / (2
· π)) < (1 + (1 / 2)))) |
235 | 232, 234 | mpbird 246 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((𝑇 / i) / (2 · π)) − (1 / 2))
< 1) |
236 | 104, 235 | syl5eqbr 4618 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑁 < 1) |
237 | 130, 236 | jca 553 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 < 𝑁 ∧ 𝑁 < 1)) |