Metamath Proof Explorer

Theorem logreclem

Description: Symmetry of the natural logarithm range by negation. Lemma for logrec . (Contributed by Saveliy Skresanov, 27-Dec-2016)

Ref Expression
Assertion logreclem ⊢ A ∈ ran ⁡ log ∧ ¬ ℑ ⁡ A = π → − A ∈ ran ⁡ log

Proof

Step Hyp Ref Expression
1 logrncn ⊢ A ∈ ran ⁡ log → A ∈ ℂ
2 1 adantr ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → A ∈ ℂ
3 2 negcld ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − A ∈ ℂ
4 ellogrn ⊢ A ∈ ran ⁡ log ↔ A ∈ ℂ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
5 4 biimpi ⊢ A ∈ ran ⁡ log → A ∈ ℂ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
6 5 simp3d ⊢ A ∈ ran ⁡ log → ℑ ⁡ A ≤ π
7 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
8 pire ⊢ π ∈ ℝ
9 leneg ⊢ ℑ ⁡ A ∈ ℝ ∧ π ∈ ℝ → ℑ ⁡ A ≤ π ↔ − π ≤ − ℑ ⁡ A
10 9 biimpd ⊢ ℑ ⁡ A ∈ ℝ ∧ π ∈ ℝ → ℑ ⁡ A ≤ π → − π ≤ − ℑ ⁡ A
11 7 8 10 sylancl ⊢ A ∈ ℂ → ℑ ⁡ A ≤ π → − π ≤ − ℑ ⁡ A
12 1 6 11 sylc ⊢ A ∈ ran ⁡ log → − π ≤ − ℑ ⁡ A
13 8 renegcli ⊢ − π ∈ ℝ
14 13 a1i ⊢ A ∈ ℂ → − π ∈ ℝ
15 7 renegcld ⊢ A ∈ ℂ → − ℑ ⁡ A ∈ ℝ
16 14 15 leloed ⊢ A ∈ ℂ → − π ≤ − ℑ ⁡ A ↔ − π < − ℑ ⁡ A ∨ − π = − ℑ ⁡ A
17 16 biimpd ⊢ A ∈ ℂ → − π ≤ − ℑ ⁡ A → − π < − ℑ ⁡ A ∨ − π = − ℑ ⁡ A
18 1 12 17 sylc ⊢ A ∈ ran ⁡ log → − π < − ℑ ⁡ A ∨ − π = − ℑ ⁡ A
19 18 orcomd ⊢ A ∈ ran ⁡ log → − π = − ℑ ⁡ A ∨ − π < − ℑ ⁡ A
20 19 orcanai ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − π < − ℑ ⁡ A
21 5 simp2d ⊢ A ∈ ran ⁡ log → − π < ℑ ⁡ A
22 ltnegcon1 ⊢ π ∈ ℝ ∧ ℑ ⁡ A ∈ ℝ → − π < ℑ ⁡ A ↔ − ℑ ⁡ A < π
23 22 biimpd ⊢ π ∈ ℝ ∧ ℑ ⁡ A ∈ ℝ → − π < ℑ ⁡ A → − ℑ ⁡ A < π
24 8 7 23 sylancr ⊢ A ∈ ℂ → − π < ℑ ⁡ A → − ℑ ⁡ A < π
25 1 21 24 sylc ⊢ A ∈ ran ⁡ log → − ℑ ⁡ A < π
26 25 adantr ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − ℑ ⁡ A < π
27 ltle ⊢ − ℑ ⁡ A ∈ ℝ ∧ π ∈ ℝ → − ℑ ⁡ A < π → − ℑ ⁡ A ≤ π
28 15 8 27 sylancl ⊢ A ∈ ℂ → − ℑ ⁡ A < π → − ℑ ⁡ A ≤ π
29 1 28 syl ⊢ A ∈ ran ⁡ log → − ℑ ⁡ A < π → − ℑ ⁡ A ≤ π
30 29 adantr ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − ℑ ⁡ A < π → − ℑ ⁡ A ≤ π
31 26 30 mpd ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − ℑ ⁡ A ≤ π
32 imneg ⊢ A ∈ ℂ → ℑ ⁡ − A = − ℑ ⁡ A
33 32 breq2d ⊢ A ∈ ℂ → − π < ℑ ⁡ − A ↔ − π < − ℑ ⁡ A
34 2 33 syl ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − π < ℑ ⁡ − A ↔ − π < − ℑ ⁡ A
35 32 breq1d ⊢ A ∈ ℂ → ℑ ⁡ − A ≤ π ↔ − ℑ ⁡ A ≤ π
36 2 35 syl ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → ℑ ⁡ − A ≤ π ↔ − ℑ ⁡ A ≤ π
37 34 36 anbi12d ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − π < ℑ ⁡ − A ∧ ℑ ⁡ − A ≤ π ↔ − π < − ℑ ⁡ A ∧ − ℑ ⁡ A ≤ π
38 20 31 37 mpbir2and ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − π < ℑ ⁡ − A ∧ ℑ ⁡ − A ≤ π
39 3anass ⊢ − A ∈ ℂ ∧ − π < ℑ ⁡ − A ∧ ℑ ⁡ − A ≤ π ↔ − A ∈ ℂ ∧ − π < ℑ ⁡ − A ∧ ℑ ⁡ − A ≤ π
40 3 38 39 sylanbrc ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − A ∈ ℂ ∧ − π < ℑ ⁡ − A ∧ ℑ ⁡ − A ≤ π
41 ellogrn ⊢ − A ∈ ran ⁡ log ↔ − A ∈ ℂ ∧ − π < ℑ ⁡ − A ∧ ℑ ⁡ − A ≤ π
42 40 41 sylibr ⊢ A ∈ ran ⁡ log ∧ ¬ − π = − ℑ ⁡ A → − A ∈ ran ⁡ log
43 42 ex ⊢ A ∈ ran ⁡ log → ¬ − π = − ℑ ⁡ A → − A ∈ ran ⁡ log
44 43 orrd ⊢ A ∈ ran ⁡ log → − π = − ℑ ⁡ A ∨ − A ∈ ran ⁡ log
45 recn ⊢ π ∈ ℝ → π ∈ ℂ
46 recn ⊢ ℑ ⁡ A ∈ ℝ → ℑ ⁡ A ∈ ℂ
47 45 46 anim12i ⊢ π ∈ ℝ ∧ ℑ ⁡ A ∈ ℝ → π ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ
48 8 7 47 sylancr ⊢ A ∈ ℂ → π ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ
49 1 48 syl ⊢ A ∈ ran ⁡ log → π ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ
50 neg11 ⊢ π ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → − π = − ℑ ⁡ A ↔ π = ℑ ⁡ A
51 eqcom ⊢ π = ℑ ⁡ A ↔ ℑ ⁡ A = π
52 50 51 bitrdi ⊢ π ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → − π = − ℑ ⁡ A ↔ ℑ ⁡ A = π
53 49 52 syl ⊢ A ∈ ran ⁡ log → − π = − ℑ ⁡ A ↔ ℑ ⁡ A = π
54 53 orbi1d ⊢ A ∈ ran ⁡ log → − π = − ℑ ⁡ A ∨ − A ∈ ran ⁡ log ↔ ℑ ⁡ A = π ∨ − A ∈ ran ⁡ log
55 44 54 mpbid ⊢ A ∈ ran ⁡ log → ℑ ⁡ A = π ∨ − A ∈ ran ⁡ log
56 55 orcanai ⊢ A ∈ ran ⁡ log ∧ ¬ ℑ ⁡ A = π → − A ∈ ran ⁡ log