MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ang180lem2 Structured version   Visualization version   GIF version

Theorem ang180lem2 24257
Description: Lemma for ang180 24261. Show that the revolution number 𝑁 is strictly between -2 and 1. Both bounds are established by iterating using the bounds on the imaginary part of the logarithm, logimcl 24037, but the resulting bound gives only 𝑁 ≤ 1 for the upper bound. The case 𝑁 = 1 is not ruled out here, but it is in some sense an "edge case" that can only happen under very specific conditions; in particular we show that all the angle arguments 𝐴, 1 / (1 − 𝐴), (𝐴 − 1) / 𝐴 must lie on the negative real axis, which is a contradiction because clearly if 𝐴 is negative then the other two are positive real. (Contributed by Mario Carneiro, 23-Sep-2014.)
Hypotheses
Ref Expression
ang.1 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
ang180lem1.2 𝑇 = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))
ang180lem1.3 𝑁 = (((𝑇 / i) / (2 · π)) − (1 / 2))
Assertion
Ref Expression
ang180lem2 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 < 𝑁𝑁 < 1))
Distinct variable group:   𝑥,𝑦,𝐴
Allowed substitution hints:   𝑇(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑁(𝑥,𝑦)

Proof of Theorem ang180lem2
StepHypRef Expression
1 2cn 10938 . . . . . . 7 2 ∈ ℂ
2 1re 9895 . . . . . . . . 9 1 ∈ ℝ
32rehalfcli 11128 . . . . . . . 8 (1 / 2) ∈ ℝ
43recni 9908 . . . . . . 7 (1 / 2) ∈ ℂ
51, 4negsubdii 10217 . . . . . 6 -(2 − (1 / 2)) = (-2 + (1 / 2))
6 4d2e2 11031 . . . . . . . . 9 (4 / 2) = 2
76oveq1i 6537 . . . . . . . 8 ((4 / 2) − (1 / 2)) = (2 − (1 / 2))
8 4cn 10945 . . . . . . . . . 10 4 ∈ ℂ
9 ax-1cn 9850 . . . . . . . . . 10 1 ∈ ℂ
10 2cnne0 11089 . . . . . . . . . 10 (2 ∈ ℂ ∧ 2 ≠ 0)
11 divsubdir 10570 . . . . . . . . . 10 ((4 ∈ ℂ ∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((4 − 1) / 2) = ((4 / 2) − (1 / 2)))
128, 9, 10, 11mp3an 1415 . . . . . . . . 9 ((4 − 1) / 2) = ((4 / 2) − (1 / 2))
13 3cn 10942 . . . . . . . . . . 11 3 ∈ ℂ
149, 13addcomi 10078 . . . . . . . . . . . 12 (1 + 3) = (3 + 1)
15 df-4 10928 . . . . . . . . . . . 12 4 = (3 + 1)
1614, 15eqtr4i 2634 . . . . . . . . . . 11 (1 + 3) = 4
178, 9, 13, 16subaddrii 10221 . . . . . . . . . 10 (4 − 1) = 3
1817oveq1i 6537 . . . . . . . . 9 ((4 − 1) / 2) = (3 / 2)
1912, 18eqtr3i 2633 . . . . . . . 8 ((4 / 2) − (1 / 2)) = (3 / 2)
207, 19eqtr3i 2633 . . . . . . 7 (2 − (1 / 2)) = (3 / 2)
2120negeqi 10125 . . . . . 6 -(2 − (1 / 2)) = -(3 / 2)
225, 21eqtr3i 2633 . . . . 5 (-2 + (1 / 2)) = -(3 / 2)
23 3re 10941 . . . . . . . . . . . . 13 3 ∈ ℝ
2423rehalfcli 11128 . . . . . . . . . . . 12 (3 / 2) ∈ ℝ
2524recni 9908 . . . . . . . . . . 11 (3 / 2) ∈ ℂ
26 picn 23932 . . . . . . . . . . 11 π ∈ ℂ
2725, 1, 26mulassi 9905 . . . . . . . . . 10 (((3 / 2) · 2) · π) = ((3 / 2) · (2 · π))
28 2ne0 10960 . . . . . . . . . . . 12 2 ≠ 0
2913, 1, 28divcan1i 10618 . . . . . . . . . . 11 ((3 / 2) · 2) = 3
3029oveq1i 6537 . . . . . . . . . 10 (((3 / 2) · 2) · π) = (3 · π)
3127, 30eqtr3i 2633 . . . . . . . . 9 ((3 / 2) · (2 · π)) = (3 · π)
3231negeqi 10125 . . . . . . . 8 -((3 / 2) · (2 · π)) = -(3 · π)
33 2re 10937 . . . . . . . . . . 11 2 ∈ ℝ
34 pire 23931 . . . . . . . . . . 11 π ∈ ℝ
3533, 34remulcli 9910 . . . . . . . . . 10 (2 · π) ∈ ℝ
3635recni 9908 . . . . . . . . 9 (2 · π) ∈ ℂ
3725, 36mulneg1i 10326 . . . . . . . 8 (-(3 / 2) · (2 · π)) = -((3 / 2) · (2 · π))
3813, 26mulneg2i 10327 . . . . . . . 8 (3 · -π) = -(3 · π)
3932, 37, 383eqtr4i 2641 . . . . . . 7 (-(3 / 2) · (2 · π)) = (3 · -π)
4034renegcli 10193 . . . . . . . . . . . 12 -π ∈ ℝ
4133, 40remulcli 9910 . . . . . . . . . . 11 (2 · -π) ∈ ℝ
4241a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) ∈ ℝ)
4340a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π ∈ ℝ)
44 simp1 1053 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ∈ ℂ)
45 subcl 10131 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 − 𝐴) ∈ ℂ)
469, 44, 45sylancr 693 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ∈ ℂ)
47 simp3 1055 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 1)
4847necomd 2836 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ≠ 𝐴)
49 subeq0 10158 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴))
509, 44, 49sylancr 693 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴))
5150necon3bid 2825 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) ≠ 0 ↔ 1 ≠ 𝐴))
5248, 51mpbird 245 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 − 𝐴) ≠ 0)
5346, 52reccld 10643 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ∈ ℂ)
5446, 52recne0d 10644 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / (1 − 𝐴)) ≠ 0)
5553, 54logcld 24038 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘(1 / (1 − 𝐴))) ∈ ℂ)
56 subcl 10131 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 − 1) ∈ ℂ)
5744, 9, 56sylancl 692 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ∈ ℂ)
58 simp2 1054 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝐴 ≠ 0)
5957, 44, 58divcld 10650 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ∈ ℂ)
60 subeq0 10158 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 − 1) = 0 ↔ 𝐴 = 1))
6144, 9, 60sylancl 692 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) = 0 ↔ 𝐴 = 1))
6261necon3bid 2825 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) ≠ 0 ↔ 𝐴 ≠ 1))
6347, 62mpbird 245 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 − 1) ≠ 0)
6457, 44, 63, 58divne0d 10666 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝐴 − 1) / 𝐴) ≠ 0)
6559, 64logcld 24038 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘((𝐴 − 1) / 𝐴)) ∈ ℂ)
6655, 65addcld 9915 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) ∈ ℂ)
6766imcld 13729 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ)
68 logcl 24036 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ)
69683adant3 1073 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘𝐴) ∈ ℂ)
7069imcld 13729 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘𝐴)) ∈ ℝ)
7155imcld 13729 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘(1 / (1 − 𝐴)))) ∈ ℝ)
7265imcld 13729 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘((𝐴 − 1) / 𝐴))) ∈ ℝ)
7353, 54logimcld 24039 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π < (ℑ‘(log‘(1 / (1 − 𝐴)))) ∧ (ℑ‘(log‘(1 / (1 − 𝐴)))) ≤ π))
7473simpld 473 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π < (ℑ‘(log‘(1 / (1 − 𝐴)))))
7559, 64logimcld 24039 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π < (ℑ‘(log‘((𝐴 − 1) / 𝐴))) ∧ (ℑ‘(log‘((𝐴 − 1) / 𝐴))) ≤ π))
7675simpld 473 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π < (ℑ‘(log‘((𝐴 − 1) / 𝐴))))
7743, 43, 71, 72, 74, 76lt2addd 10499 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π + -π) < ((ℑ‘(log‘(1 / (1 − 𝐴)))) + (ℑ‘(log‘((𝐴 − 1) / 𝐴)))))
78 negpicn 23935 . . . . . . . . . . . . 13 -π ∈ ℂ
79782timesi 10994 . . . . . . . . . . . 12 (2 · -π) = (-π + -π)
8079a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) = (-π + -π))
8155, 65imaddd 13749 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) = ((ℑ‘(log‘(1 / (1 − 𝐴)))) + (ℑ‘(log‘((𝐴 − 1) / 𝐴)))))
8277, 80, 813brtr4d 4609 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · -π) < (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))))
83 logimcl 24037 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))
84833adant3 1073 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))
8584simpld 473 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -π < (ℑ‘(log‘𝐴)))
8642, 43, 67, 70, 82, 85lt2addd 10499 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((2 · -π) + -π) < ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))))
87 df-3 10927 . . . . . . . . . . . 12 3 = (2 + 1)
8887oveq1i 6537 . . . . . . . . . . 11 (3 · -π) = ((2 + 1) · -π)
891, 9, 78adddiri 9907 . . . . . . . . . . 11 ((2 + 1) · -π) = ((2 · -π) + (1 · -π))
9078mulid2i 9899 . . . . . . . . . . . 12 (1 · -π) = -π
9190oveq2i 6538 . . . . . . . . . . 11 ((2 · -π) + (1 · -π)) = ((2 · -π) + -π)
9288, 89, 913eqtri 2635 . . . . . . . . . 10 (3 · -π) = ((2 · -π) + -π)
9392a1i 11 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) = ((2 · -π) + -π))
94 ang180lem1.2 . . . . . . . . . . 11 𝑇 = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))
9594fveq2i 6091 . . . . . . . . . 10 (ℑ‘𝑇) = (ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)))
9666, 69imaddd 13749 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))) = ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))))
9795, 96syl5eq 2655 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) = ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))))
9886, 93, 973brtr4d 4609 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) < (ℑ‘𝑇))
9966, 69addcld 9915 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴)) ∈ ℂ)
10094, 99syl5eqel 2691 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑇 ∈ ℂ)
101 imval 13641 . . . . . . . . . 10 (𝑇 ∈ ℂ → (ℑ‘𝑇) = (ℜ‘(𝑇 / i)))
102100, 101syl 17 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) = (ℜ‘(𝑇 / i)))
103 ang.1 . . . . . . . . . . . 12 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
104 ang180lem1.3 . . . . . . . . . . . 12 𝑁 = (((𝑇 / i) / (2 · π)) − (1 / 2))
105103, 94, 104ang180lem1 24256 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑁 ∈ ℤ ∧ (𝑇 / i) ∈ ℝ))
106105simprd 477 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ∈ ℝ)
107106rered 13758 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℜ‘(𝑇 / i)) = (𝑇 / i))
108102, 107eqtrd 2643 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘𝑇) = (𝑇 / i))
10998, 108breqtrd 4603 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · -π) < (𝑇 / i))
11039, 109syl5eqbr 4612 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(3 / 2) · (2 · π)) < (𝑇 / i))
11124renegcli 10193 . . . . . . . 8 -(3 / 2) ∈ ℝ
112111a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(3 / 2) ∈ ℝ)
11335a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ∈ ℝ)
114 2pos 10959 . . . . . . . . 9 0 < 2
115 pipos 23933 . . . . . . . . 9 0 < π
11633, 34, 114, 115mulgt0ii 10021 . . . . . . . 8 0 < (2 · π)
117116a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 < (2 · π))
118 ltmuldiv 10745 . . . . . . 7 ((-(3 / 2) ∈ ℝ ∧ (𝑇 / i) ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2 · π))) → ((-(3 / 2) · (2 · π)) < (𝑇 / i) ↔ -(3 / 2) < ((𝑇 / i) / (2 · π))))
119112, 106, 113, 117, 118syl112anc 1321 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((-(3 / 2) · (2 · π)) < (𝑇 / i) ↔ -(3 / 2) < ((𝑇 / i) / (2 · π))))
120110, 119mpbid 220 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(3 / 2) < ((𝑇 / i) / (2 · π)))
12122, 120syl5eqbr 4612 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 + (1 / 2)) < ((𝑇 / i) / (2 · π)))
12233renegcli 10193 . . . . . 6 -2 ∈ ℝ
123122a1i 11 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 ∈ ℝ)
1243a1i 11 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 / 2) ∈ ℝ)
12535, 116gt0ne0ii 10413 . . . . . . 7 (2 · π) ≠ 0
126125a1i 11 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ≠ 0)
127106, 113, 126redivcld 10702 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) ∈ ℝ)
128123, 124, 127ltaddsubd 10476 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((-2 + (1 / 2)) < ((𝑇 / i) / (2 · π)) ↔ -2 < (((𝑇 / i) / (2 · π)) − (1 / 2))))
129121, 128mpbid 220 . . 3 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 < (((𝑇 / i) / (2 · π)) − (1 / 2)))
130129, 104syl6breqr 4619 . 2 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -2 < 𝑁)
13134a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → π ∈ ℝ)
13273simprd 477 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘(1 / (1 − 𝐴)))) ≤ π)
13375simprd 477 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘((𝐴 − 1) / 𝐴))) ≤ π)
13471, 72, 131, 131, 132, 133le2addd 10495 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((ℑ‘(log‘(1 / (1 − 𝐴)))) + (ℑ‘(log‘((𝐴 − 1) / 𝐴)))) ≤ (π + π))
135262timesi 10994 . . . . . . . . . . . 12 (2 · π) = (π + π)
136135a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) = (π + π))
137134, 81, 1363brtr4d 4609 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ≤ (2 · π))
13884simprd 477 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘𝐴)) ≤ π)
13967, 70, 113, 131, 137, 138le2addd 10495 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))) ≤ ((2 · π) + π))
140108, 97eqtr3d 2645 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) = ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴))))
14187oveq1i 6537 . . . . . . . . . . 11 (3 · π) = ((2 + 1) · π)
1421, 9, 26adddiri 9907 . . . . . . . . . . 11 ((2 + 1) · π) = ((2 · π) + (1 · π))
14326mulid2i 9899 . . . . . . . . . . . 12 (1 · π) = π
144143oveq2i 6538 . . . . . . . . . . 11 ((2 · π) + (1 · π)) = ((2 · π) + π)
145141, 142, 1443eqtri 2635 . . . . . . . . . 10 (3 · π) = ((2 · π) + π)
146145a1i 11 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · π) = ((2 · π) + π))
147139, 140, 1463brtr4d 4609 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ≤ (3 · π))
14836subid1i 10204 . . . . . . . . . 10 ((2 · π) − 0) = (2 · π)
149148, 125eqnetri 2851 . . . . . . . . 9 ((2 · π) − 0) ≠ 0
150 negsub 10180 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 + -𝐴) = (1 − 𝐴))
1519, 44, 150sylancr 693 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (1 + -𝐴) = (1 − 𝐴))
152151adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 + -𝐴) = (1 − 𝐴))
153 1rp 11668 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ+
154146, 140oveq12d 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) − (𝑇 / i)) = (((2 · π) + π) − ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴)))))
15536a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (2 · π) ∈ ℂ)
15626a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → π ∈ ℂ)
15767recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℂ)
15870recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (ℑ‘(log‘𝐴)) ∈ ℂ)
159155, 156, 157, 158addsub4d 10290 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((2 · π) + π) − ((ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) + (ℑ‘(log‘𝐴)))) = (((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π − (ℑ‘(log‘𝐴)))))
160154, 159eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) − (𝑇 / i)) = (((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π − (ℑ‘(log‘𝐴)))))
161160adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((3 · π) − (𝑇 / i)) = (((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π − (ℑ‘(log‘𝐴)))))
16223, 34remulcli 9910 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (3 · π) ∈ ℝ
163162recni 9908 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (3 · π) ∈ ℂ
164 ax-icn 9851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 i ∈ ℂ
165164a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → i ∈ ℂ)
166 ine0 10316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 i ≠ 0
167166a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → i ≠ 0)
168100, 165, 167divcld 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) ∈ ℂ)
169 subeq0 10158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((3 · π) ∈ ℂ ∧ (𝑇 / i) ∈ ℂ) → (((3 · π) − (𝑇 / i)) = 0 ↔ (3 · π) = (𝑇 / i)))
170163, 168, 169sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((3 · π) − (𝑇 / i)) = 0 ↔ (3 · π) = (𝑇 / i)))
171170biimpar 500 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((3 · π) − (𝑇 / i)) = 0)
172161, 171eqtr3d 2645 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π − (ℑ‘(log‘𝐴)))) = 0)
173 resubcl 10196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2 · π) ∈ ℝ ∧ (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ) → ((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ∈ ℝ)
17435, 67, 173sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ∈ ℝ)
175 subge0 10390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((2 · π) ∈ ℝ ∧ (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ∈ ℝ) → (0 ≤ ((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ↔ (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ≤ (2 · π)))
17635, 67, 175sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (0 ≤ ((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) ↔ (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) ≤ (2 · π)))
177137, 176mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 ≤ ((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))))
178 resubcl 10196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π ∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (π − (ℑ‘(log‘𝐴))) ∈ ℝ)
17934, 70, 178sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (π − (ℑ‘(log‘𝐴))) ∈ ℝ)
180 subge0 10390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π ∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (0 ≤ (π − (ℑ‘(log‘𝐴))) ↔ (ℑ‘(log‘𝐴)) ≤ π))
18134, 70, 180sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (0 ≤ (π − (ℑ‘(log‘𝐴))) ↔ (ℑ‘(log‘𝐴)) ≤ π))
182138, 181mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 0 ≤ (π − (ℑ‘(log‘𝐴))))
183 add20 10389 . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
184174, 177, 179, 182, 183syl22anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π − (ℑ‘(log‘𝐴)))) = 0 ↔ (((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π − (ℑ‘(log‘𝐴))) = 0)))
185184biimpa 499 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) + (π − (ℑ‘(log‘𝐴)))) = 0) → (((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π − (ℑ‘(log‘𝐴))) = 0))
186172, 185syldan 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0 ∧ (π − (ℑ‘(log‘𝐴))) = 0))
187186simprd 477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (π − (ℑ‘(log‘𝐴))) = 0)
188158adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (ℑ‘(log‘𝐴)) ∈ ℂ)
189 subeq0 10158 . . . . . . . . . . . . . . . . . . . . . . 23 ((π ∈ ℂ ∧ (ℑ‘(log‘𝐴)) ∈ ℂ) → ((π − (ℑ‘(log‘𝐴))) = 0 ↔ π = (ℑ‘(log‘𝐴))))
19026, 188, 189sylancr 693 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((π − (ℑ‘(log‘𝐴))) = 0 ↔ π = (ℑ‘(log‘𝐴))))
191187, 190mpbid 220 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → π = (ℑ‘(log‘𝐴)))
192191eqcomd 2615 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (ℑ‘(log‘𝐴)) = π)
193 lognegb 24057 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+ ↔ (ℑ‘(log‘𝐴)) = π))
1941933adant3 1073 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-𝐴 ∈ ℝ+ ↔ (ℑ‘(log‘𝐴)) = π))
195194adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (-𝐴 ∈ ℝ+ ↔ (ℑ‘(log‘𝐴)) = π))
196192, 195mpbird 245 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → -𝐴 ∈ ℝ+)
197 rpaddcl 11686 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ+ ∧ -𝐴 ∈ ℝ+) → (1 + -𝐴) ∈ ℝ+)
198153, 196, 197sylancr 693 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 + -𝐴) ∈ ℝ+)
199152, 198eqeltrrd 2688 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 − 𝐴) ∈ ℝ+)
200199rpreccld 11714 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (1 / (1 − 𝐴)) ∈ ℝ+)
201200relogcld 24090 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (log‘(1 / (1 − 𝐴))) ∈ ℝ)
202 negsubdi2 10191 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → -(𝐴 − 1) = (1 − 𝐴))
20344, 9, 202sylancl 692 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → -(𝐴 − 1) = (1 − 𝐴))
204203oveq1d 6542 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(𝐴 − 1) / -𝐴) = ((1 − 𝐴) / -𝐴))
20557, 44, 58div2negd 10665 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-(𝐴 − 1) / -𝐴) = ((𝐴 − 1) / 𝐴))
206204, 205eqtr3d 2645 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((1 − 𝐴) / -𝐴) = ((𝐴 − 1) / 𝐴))
207206adantr 479 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((1 − 𝐴) / -𝐴) = ((𝐴 − 1) / 𝐴))
208199, 196rpdivcld 11721 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((1 − 𝐴) / -𝐴) ∈ ℝ+)
209207, 208eqeltrrd 2688 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((𝐴 − 1) / 𝐴) ∈ ℝ+)
210209relogcld 24090 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (log‘((𝐴 − 1) / 𝐴)) ∈ ℝ)
211201, 210readdcld 9925 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) ∈ ℝ)
212211reim0d 13759 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴)))) = 0)
213212oveq2d 6543 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = ((2 · π) − 0))
214186simpld 473 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π) − (ℑ‘((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))))) = 0)
215213, 214eqtr3d 2645 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (3 · π) = (𝑇 / i)) → ((2 · π) − 0) = 0)
216215ex 448 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((3 · π) = (𝑇 / i) → ((2 · π) − 0) = 0))
217216necon3d 2802 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((2 · π) − 0) ≠ 0 → (3 · π) ≠ (𝑇 / i)))
218149, 217mpi 20 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 · π) ≠ (𝑇 / i))
219 ltlen 9989 . . . . . . . . 9 (((𝑇 / i) ∈ ℝ ∧ (3 · π) ∈ ℝ) → ((𝑇 / i) < (3 · π) ↔ ((𝑇 / i) ≤ (3 · π) ∧ (3 · π) ≠ (𝑇 / i))))
220106, 162, 219sylancl 692 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) < (3 · π) ↔ ((𝑇 / i) ≤ (3 · π) ∧ (3 · π) ≠ (𝑇 / i))))
221147, 218, 220mpbir2and 958 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) < (3 · π))
222221, 31syl6breqr 4619 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑇 / i) < ((3 / 2) · (2 · π)))
22324a1i 11 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (3 / 2) ∈ ℝ)
224 ltdivmul2 10749 . . . . . . 7 (((𝑇 / i) ∈ ℝ ∧ (3 / 2) ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2 · π))) → (((𝑇 / i) / (2 · π)) < (3 / 2) ↔ (𝑇 / i) < ((3 / 2) · (2 · π))))
225106, 223, 113, 117, 224syl112anc 1321 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((𝑇 / i) / (2 · π)) < (3 / 2) ↔ (𝑇 / i) < ((3 / 2) · (2 · π))))
226222, 225mpbird 245 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) < (3 / 2))
22787oveq1i 6537 . . . . . 6 (3 / 2) = ((2 + 1) / 2)
2281, 9, 1, 28divdiri 10631 . . . . . 6 ((2 + 1) / 2) = ((2 / 2) + (1 / 2))
229 2div2e1 10997 . . . . . . 7 (2 / 2) = 1
230229oveq1i 6537 . . . . . 6 ((2 / 2) + (1 / 2)) = (1 + (1 / 2))
231227, 228, 2303eqtri 2635 . . . . 5 (3 / 2) = (1 + (1 / 2))
232226, 231syl6breq 4618 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((𝑇 / i) / (2 · π)) < (1 + (1 / 2)))
2332a1i 11 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 1 ∈ ℝ)
234127, 124, 233ltsubaddd 10472 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((𝑇 / i) / (2 · π)) − (1 / 2)) < 1 ↔ ((𝑇 / i) / (2 · π)) < (1 + (1 / 2))))
235232, 234mpbird 245 . . 3 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (((𝑇 / i) / (2 · π)) − (1 / 2)) < 1)
236104, 235syl5eqbr 4612 . 2 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑁 < 1)
237130, 236jca 552 1 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 < 𝑁𝑁 < 1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  cdif 3536  {csn 4124   class class class wbr 4577  cfv 5790  (class class class)co 6527  cmpt2 6529  cc 9790  cr 9791  0cc0 9792  1c1 9793  ici 9794   + caddc 9795   · cmul 9797   < clt 9930  cle 9931  cmin 10117  -cneg 10118   / cdiv 10533  2c2 10917  3c3 10918  4c4 10919  cz 11210  +crp 11664  cre 13631  cim 13632  πcpi 14582  logclog 24022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-ioc 12007  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-fac 12878  df-bc 12907  df-hash 12935  df-shft 13601  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-limsup 13996  df-clim 14013  df-rlim 14014  df-sum 14211  df-ef 14583  df-sin 14585  df-cos 14586  df-pi 14588  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-sca 15730  df-vsca 15731  df-ip 15732  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-hom 15739  df-cco 15740  df-rest 15852  df-topn 15853  df-0g 15871  df-gsum 15872  df-topgen 15873  df-pt 15874  df-prds 15877  df-xrs 15931  df-qtop 15936  df-imas 15937  df-xps 15939  df-mre 16015  df-mrc 16016  df-acs 16018  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-submnd 17105  df-mulg 17310  df-cntz 17519  df-cmn 17964  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-fbas 19510  df-fg 19511  df-cnfld 19514  df-top 20463  df-bases 20464  df-topon 20465  df-topsp 20466  df-cld 20575  df-ntr 20576  df-cls 20577  df-nei 20654  df-lp 20692  df-perf 20693  df-cn 20783  df-cnp 20784  df-haus 20871  df-tx 21117  df-hmeo 21310  df-fil 21402  df-fm 21494  df-flim 21495  df-flf 21496  df-xms 21876  df-ms 21877  df-tms 21878  df-cncf 22420  df-limc 23353  df-dv 23354  df-log 24024
This theorem is referenced by:  ang180lem3  24258
  Copyright terms: Public domain W3C validator