Proof of Theorem logreclem
Step | Hyp | Ref
| Expression |
1 | | logrncn 25298 |
. . . . . . . . 9
⊢ (𝐴 ∈ ran log → 𝐴 ∈
ℂ) |
2 | 1 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ 𝐴 ∈
ℂ) |
3 | 2 | negcld 11055 |
. . . . . . 7
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ -𝐴 ∈
ℂ) |
4 | | ellogrn 25295 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π <
(ℑ‘𝐴) ∧
(ℑ‘𝐴) ≤
π)) |
5 | 4 | biimpi 219 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ran log → (𝐴 ∈ ℂ ∧ -π <
(ℑ‘𝐴) ∧
(ℑ‘𝐴) ≤
π)) |
6 | 5 | simp3d 1145 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ran log →
(ℑ‘𝐴) ≤
π) |
7 | | imcl 14553 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
8 | | pire 25195 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ |
9 | | leneg 11214 |
. . . . . . . . . . . . . 14
⊢
(((ℑ‘𝐴)
∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘𝐴) ≤ π ↔ -π ≤
-(ℑ‘𝐴))) |
10 | 9 | biimpd 232 |
. . . . . . . . . . . . 13
⊢
(((ℑ‘𝐴)
∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘𝐴) ≤ π → -π ≤
-(ℑ‘𝐴))) |
11 | 7, 8, 10 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴) ≤
π → -π ≤ -(ℑ‘𝐴))) |
12 | 1, 6, 11 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ran log → -π
≤ -(ℑ‘𝐴)) |
13 | 8 | renegcli 11018 |
. . . . . . . . . . . . . 14
⊢ -π
∈ ℝ |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → -π
∈ ℝ) |
15 | 7 | renegcld 11138 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) |
16 | 14, 15 | leloed 10854 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (-π
≤ -(ℑ‘𝐴)
↔ (-π < -(ℑ‘𝐴) ∨ -π = -(ℑ‘𝐴)))) |
17 | 16 | biimpd 232 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-π
≤ -(ℑ‘𝐴)
→ (-π < -(ℑ‘𝐴) ∨ -π = -(ℑ‘𝐴)))) |
18 | 1, 12, 17 | sylc 65 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ran log → (-π
< -(ℑ‘𝐴)
∨ -π = -(ℑ‘𝐴))) |
19 | 18 | orcomd 870 |
. . . . . . . . 9
⊢ (𝐴 ∈ ran log → (-π =
-(ℑ‘𝐴) ∨
-π < -(ℑ‘𝐴))) |
20 | 19 | orcanai 1002 |
. . . . . . . 8
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ -π < -(ℑ‘𝐴)) |
21 | 5 | simp2d 1144 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ran log → -π
< (ℑ‘𝐴)) |
22 | | ltnegcon1 11212 |
. . . . . . . . . . . . 13
⊢ ((π
∈ ℝ ∧ (ℑ‘𝐴) ∈ ℝ) → (-π <
(ℑ‘𝐴) ↔
-(ℑ‘𝐴) <
π)) |
23 | 22 | biimpd 232 |
. . . . . . . . . . . 12
⊢ ((π
∈ ℝ ∧ (ℑ‘𝐴) ∈ ℝ) → (-π <
(ℑ‘𝐴) →
-(ℑ‘𝐴) <
π)) |
24 | 8, 7, 23 | sylancr 590 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-π
< (ℑ‘𝐴)
→ -(ℑ‘𝐴)
< π)) |
25 | 1, 21, 24 | sylc 65 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ran log →
-(ℑ‘𝐴) <
π) |
26 | 25 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ -(ℑ‘𝐴)
< π) |
27 | | ltle 10800 |
. . . . . . . . . . . 12
⊢
((-(ℑ‘𝐴)
∈ ℝ ∧ π ∈ ℝ) → (-(ℑ‘𝐴) < π →
-(ℑ‘𝐴) ≤
π)) |
28 | 15, 8, 27 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(-(ℑ‘𝐴) <
π → -(ℑ‘𝐴) ≤ π)) |
29 | 1, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ran log →
(-(ℑ‘𝐴) <
π → -(ℑ‘𝐴) ≤ π)) |
30 | 29 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ (-(ℑ‘𝐴)
< π → -(ℑ‘𝐴) ≤ π)) |
31 | 26, 30 | mpd 15 |
. . . . . . . 8
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ -(ℑ‘𝐴)
≤ π) |
32 | | imneg 14575 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℑ‘-𝐴) =
-(ℑ‘𝐴)) |
33 | 32 | breq2d 5039 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (-π
< (ℑ‘-𝐴)
↔ -π < -(ℑ‘𝐴))) |
34 | 2, 33 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ (-π < (ℑ‘-𝐴) ↔ -π < -(ℑ‘𝐴))) |
35 | 32 | breq1d 5037 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((ℑ‘-𝐴) ≤
π ↔ -(ℑ‘𝐴) ≤ π)) |
36 | 2, 35 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ ((ℑ‘-𝐴)
≤ π ↔ -(ℑ‘𝐴) ≤ π)) |
37 | 34, 36 | anbi12d 634 |
. . . . . . . 8
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ ((-π < (ℑ‘-𝐴) ∧ (ℑ‘-𝐴) ≤ π) ↔ (-π <
-(ℑ‘𝐴) ∧
-(ℑ‘𝐴) ≤
π))) |
38 | 20, 31, 37 | mpbir2and 713 |
. . . . . . 7
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ (-π < (ℑ‘-𝐴) ∧ (ℑ‘-𝐴) ≤ π)) |
39 | | 3anass 1096 |
. . . . . . 7
⊢ ((-𝐴 ∈ ℂ ∧ -π <
(ℑ‘-𝐴) ∧
(ℑ‘-𝐴) ≤
π) ↔ (-𝐴 ∈
ℂ ∧ (-π < (ℑ‘-𝐴) ∧ (ℑ‘-𝐴) ≤ π))) |
40 | 3, 38, 39 | sylanbrc 586 |
. . . . . 6
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ (-𝐴 ∈ ℂ
∧ -π < (ℑ‘-𝐴) ∧ (ℑ‘-𝐴) ≤ π)) |
41 | | ellogrn 25295 |
. . . . . 6
⊢ (-𝐴 ∈ ran log ↔ (-𝐴 ∈ ℂ ∧ -π <
(ℑ‘-𝐴) ∧
(ℑ‘-𝐴) ≤
π)) |
42 | 40, 41 | sylibr 237 |
. . . . 5
⊢ ((𝐴 ∈ ran log ∧ ¬
-π = -(ℑ‘𝐴))
→ -𝐴 ∈ ran
log) |
43 | 42 | ex 416 |
. . . 4
⊢ (𝐴 ∈ ran log → (¬
-π = -(ℑ‘𝐴)
→ -𝐴 ∈ ran
log)) |
44 | 43 | orrd 862 |
. . 3
⊢ (𝐴 ∈ ran log → (-π =
-(ℑ‘𝐴) ∨
-𝐴 ∈ ran
log)) |
45 | | recn 10698 |
. . . . . . . 8
⊢ (π
∈ ℝ → π ∈ ℂ) |
46 | | recn 10698 |
. . . . . . . 8
⊢
((ℑ‘𝐴)
∈ ℝ → (ℑ‘𝐴) ∈ ℂ) |
47 | 45, 46 | anim12i 616 |
. . . . . . 7
⊢ ((π
∈ ℝ ∧ (ℑ‘𝐴) ∈ ℝ) → (π ∈
ℂ ∧ (ℑ‘𝐴) ∈ ℂ)) |
48 | 8, 7, 47 | sylancr 590 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (π
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ)) |
49 | 1, 48 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ran log → (π
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ)) |
50 | | neg11 11008 |
. . . . . 6
⊢ ((π
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (-π =
-(ℑ‘𝐴) ↔
π = (ℑ‘𝐴))) |
51 | | eqcom 2745 |
. . . . . 6
⊢ (π =
(ℑ‘𝐴) ↔
(ℑ‘𝐴) =
π) |
52 | 50, 51 | bitrdi 290 |
. . . . 5
⊢ ((π
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (-π =
-(ℑ‘𝐴) ↔
(ℑ‘𝐴) =
π)) |
53 | 49, 52 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ran log → (-π =
-(ℑ‘𝐴) ↔
(ℑ‘𝐴) =
π)) |
54 | 53 | orbi1d 916 |
. . 3
⊢ (𝐴 ∈ ran log → ((-π =
-(ℑ‘𝐴) ∨
-𝐴 ∈ ran log) ↔
((ℑ‘𝐴) = π
∨ -𝐴 ∈ ran
log))) |
55 | 44, 54 | mpbid 235 |
. 2
⊢ (𝐴 ∈ ran log →
((ℑ‘𝐴) = π
∨ -𝐴 ∈ ran
log)) |
56 | 55 | orcanai 1002 |
1
⊢ ((𝐴 ∈ ran log ∧ ¬
(ℑ‘𝐴) = π)
→ -𝐴 ∈ ran
log) |