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 ( ( 𝐴 ∈ ran log ∧ ¬ ( ℑ ‘ 𝐴 ) = π ) → - 𝐴 ∈ ran log )

Proof

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