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