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

Theorem logcnlem3 24604
Description: Lemma for logcn 24607. (Contributed by Mario Carneiro, 25-Feb-2015.)
Hypotheses
Ref Expression
logcn.d 𝐷 = (ℂ ∖ (-∞(,]0))
logcnlem.s 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴)))
logcnlem.t 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅)))
logcnlem.a (𝜑𝐴𝐷)
logcnlem.r (𝜑𝑅 ∈ ℝ+)
logcnlem.b (𝜑𝐵𝐷)
logcnlem.l (𝜑 → (abs‘(𝐴𝐵)) < if(𝑆𝑇, 𝑆, 𝑇))
Assertion
Ref Expression
logcnlem3 (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π))

Proof of Theorem logcnlem3
StepHypRef Expression
1 pire 24424 . . . . . 6 π ∈ ℝ
21renegcli 10542 . . . . 5 -π ∈ ℝ
32a1i 11 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -π ∈ ℝ)
4 logcnlem.b . . . . . . . 8 (𝜑𝐵𝐷)
5 logcn.d . . . . . . . . . 10 𝐷 = (ℂ ∖ (-∞(,]0))
65ellogdm 24599 . . . . . . . . 9 (𝐵𝐷 ↔ (𝐵 ∈ ℂ ∧ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ+)))
76simplbi 485 . . . . . . . 8 (𝐵𝐷𝐵 ∈ ℂ)
84, 7syl 17 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
95logdmn0 24600 . . . . . . . 8 (𝐵𝐷𝐵 ≠ 0)
104, 9syl 17 . . . . . . 7 (𝜑𝐵 ≠ 0)
118, 10logcld 24531 . . . . . 6 (𝜑 → (log‘𝐵) ∈ ℂ)
1211imcld 14136 . . . . 5 (𝜑 → (ℑ‘(log‘𝐵)) ∈ ℝ)
1312adantr 466 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) ∈ ℝ)
14 logcnlem.a . . . . . . . . 9 (𝜑𝐴𝐷)
155ellogdm 24599 . . . . . . . . . 10 (𝐴𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+)))
1615simplbi 485 . . . . . . . . 9 (𝐴𝐷𝐴 ∈ ℂ)
1714, 16syl 17 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
185logdmn0 24600 . . . . . . . . 9 (𝐴𝐷𝐴 ≠ 0)
1914, 18syl 17 . . . . . . . 8 (𝜑𝐴 ≠ 0)
2017, 19logcld 24531 . . . . . . 7 (𝜑 → (log‘𝐴) ∈ ℂ)
2120imcld 14136 . . . . . 6 (𝜑 → (ℑ‘(log‘𝐴)) ∈ ℝ)
2212, 21resubcld 10658 . . . . 5 (𝜑 → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∈ ℝ)
2322adantr 466 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∈ ℝ)
248, 10logimcld 24532 . . . . . 6 (𝜑 → (-π < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) ≤ π))
2524simpld 482 . . . . 5 (𝜑 → -π < (ℑ‘(log‘𝐵)))
2625adantr 466 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -π < (ℑ‘(log‘𝐵)))
2712recnd 10268 . . . . . . 7 (𝜑 → (ℑ‘(log‘𝐵)) ∈ ℂ)
2827adantr 466 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) ∈ ℂ)
2928subid1d 10581 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − 0) = (ℑ‘(log‘𝐵)))
3021adantr 466 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ ℝ)
31 0red 10241 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → 0 ∈ ℝ)
32 argimlt0 24573 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0))
3317, 32sylan 569 . . . . . . . 8 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0))
34 eliooord 12431 . . . . . . . 8 ((ℑ‘(log‘𝐴)) ∈ (-π(,)0) → (-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < 0))
3533, 34syl 17 . . . . . . 7 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < 0))
3635simprd 483 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) < 0)
3730, 31, 13, 36ltsub2dd 10840 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − 0) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
3829, 37eqbrtrrd 4810 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
393, 13, 23, 26, 38lttrd 10398 . . 3 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
4025adantr 466 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) = 0) → -π < (ℑ‘(log‘𝐵)))
41 reim0b 14060 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
4217, 41syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
4315simprbi 484 . . . . . . . . . . 11 (𝐴𝐷 → (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))
4414, 43syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))
4542, 44sylbird 250 . . . . . . . . 9 (𝜑 → ((ℑ‘𝐴) = 0 → 𝐴 ∈ ℝ+))
4645imp 393 . . . . . . . 8 ((𝜑 ∧ (ℑ‘𝐴) = 0) → 𝐴 ∈ ℝ+)
4746relogcld 24583 . . . . . . 7 ((𝜑 ∧ (ℑ‘𝐴) = 0) → (log‘𝐴) ∈ ℝ)
4847reim0d 14166 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) = 0) → (ℑ‘(log‘𝐴)) = 0)
4948oveq2d 6807 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) = 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) = ((ℑ‘(log‘𝐵)) − 0))
5027subid1d 10581 . . . . . 6 (𝜑 → ((ℑ‘(log‘𝐵)) − 0) = (ℑ‘(log‘𝐵)))
5150adantr 466 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) = 0) → ((ℑ‘(log‘𝐵)) − 0) = (ℑ‘(log‘𝐵)))
5249, 51eqtrd 2805 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) = 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) = (ℑ‘(log‘𝐵)))
5340, 52breqtrrd 4814 . . 3 ((𝜑 ∧ (ℑ‘𝐴) = 0) → -π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
542a1i 11 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -π ∈ ℝ)
5521renegcld 10657 . . . . 5 (𝜑 → -(ℑ‘(log‘𝐴)) ∈ ℝ)
5655adantr 466 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -(ℑ‘(log‘𝐴)) ∈ ℝ)
5722adantr 466 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∈ ℝ)
58 argimgt0 24572 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π))
5917, 58sylan 569 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π))
60 eliooord 12431 . . . . . . 7 ((ℑ‘(log‘𝐴)) ∈ (0(,)π) → (0 < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < π))
6159, 60syl 17 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < π))
6261simprd 483 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) < π)
63 ltneg 10728 . . . . . . 7 (((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘(log‘𝐴)) < π ↔ -π < -(ℑ‘(log‘𝐴))))
6421, 1, 63sylancl 574 . . . . . 6 (𝜑 → ((ℑ‘(log‘𝐴)) < π ↔ -π < -(ℑ‘(log‘𝐴))))
6564adantr 466 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐴)) < π ↔ -π < -(ℑ‘(log‘𝐴))))
6662, 65mpbid 222 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -π < -(ℑ‘(log‘𝐴)))
67 df-neg 10469 . . . . 5 -(ℑ‘(log‘𝐴)) = (0 − (ℑ‘(log‘𝐴)))
688adantr 466 . . . . . . . . 9 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 𝐵 ∈ ℂ)
6917, 8imsubd 14158 . . . . . . . . . . . . 13 (𝜑 → (ℑ‘(𝐴𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
7069adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(𝐴𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
7117, 8subcld 10592 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐵) ∈ ℂ)
7271imcld 14136 . . . . . . . . . . . . . 14 (𝜑 → (ℑ‘(𝐴𝐵)) ∈ ℝ)
7372adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(𝐴𝐵)) ∈ ℝ)
7471abscld 14376 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐴𝐵)) ∈ ℝ)
7574adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (abs‘(𝐴𝐵)) ∈ ℝ)
7617adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 𝐴 ∈ ℂ)
7776imcld 14136 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ∈ ℝ)
78 absimle 14250 . . . . . . . . . . . . . . . . 17 ((𝐴𝐵) ∈ ℂ → (abs‘(ℑ‘(𝐴𝐵))) ≤ (abs‘(𝐴𝐵)))
7971, 78syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘(ℑ‘(𝐴𝐵))) ≤ (abs‘(𝐴𝐵)))
8072, 74absled 14370 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(ℑ‘(𝐴𝐵))) ≤ (abs‘(𝐴𝐵)) ↔ (-(abs‘(𝐴𝐵)) ≤ (ℑ‘(𝐴𝐵)) ∧ (ℑ‘(𝐴𝐵)) ≤ (abs‘(𝐴𝐵)))))
8179, 80mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → (-(abs‘(𝐴𝐵)) ≤ (ℑ‘(𝐴𝐵)) ∧ (ℑ‘(𝐴𝐵)) ≤ (abs‘(𝐴𝐵))))
8281simprd 483 . . . . . . . . . . . . . 14 (𝜑 → (ℑ‘(𝐴𝐵)) ≤ (abs‘(𝐴𝐵)))
8382adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(𝐴𝐵)) ≤ (abs‘(𝐴𝐵)))
84 logcnlem.s . . . . . . . . . . . . . . . . . 18 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴)))
85 rpre 12035 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
8685adantl 467 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐴 ∈ ℝ+) → 𝐴 ∈ ℝ)
8717imcld 14136 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (ℑ‘𝐴) ∈ ℝ)
8887recnd 10268 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (ℑ‘𝐴) ∈ ℂ)
8988abscld 14376 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ)
9089adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ+) → (abs‘(ℑ‘𝐴)) ∈ ℝ)
9186, 90ifclda 4259 . . . . . . . . . . . . . . . . . 18 (𝜑 → if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) ∈ ℝ)
9284, 91syl5eqel 2854 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ ℝ)
93 logcnlem.t . . . . . . . . . . . . . . . . . 18 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅)))
9417abscld 14376 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘𝐴) ∈ ℝ)
95 logcnlem.r . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑅 ∈ ℝ+)
9695rpred 12068 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 ∈ ℝ)
97 1rp 12032 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ+
98 rpaddcl 12050 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ+𝑅 ∈ ℝ+) → (1 + 𝑅) ∈ ℝ+)
9997, 95, 98sylancr 575 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 + 𝑅) ∈ ℝ+)
10096, 99rerpdivcld 12099 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑅 / (1 + 𝑅)) ∈ ℝ)
10194, 100remulcld 10270 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) ∈ ℝ)
10293, 101syl5eqel 2854 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ ℝ)
10392, 102ifcld 4270 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑆𝑇, 𝑆, 𝑇) ∈ ℝ)
104 logcnlem.l . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘(𝐴𝐵)) < if(𝑆𝑇, 𝑆, 𝑇))
105 min1 12218 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ) → if(𝑆𝑇, 𝑆, 𝑇) ≤ 𝑆)
10692, 102, 105syl2anc 573 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑆𝑇, 𝑆, 𝑇) ≤ 𝑆)
10774, 103, 92, 104, 106ltletrd 10397 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝐴𝐵)) < 𝑆)
108107adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (abs‘(𝐴𝐵)) < 𝑆)
109 gt0ne0 10693 . . . . . . . . . . . . . . . . 17 (((ℑ‘𝐴) ∈ ℝ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ≠ 0)
11087, 109sylan 569 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ≠ 0)
11185, 42syl5ib 234 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 ∈ ℝ+ → (ℑ‘𝐴) = 0))
112111necon3ad 2956 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((ℑ‘𝐴) ≠ 0 → ¬ 𝐴 ∈ ℝ+))
113112imp 393 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (ℑ‘𝐴) ≠ 0) → ¬ 𝐴 ∈ ℝ+)
114 iffalse 4234 . . . . . . . . . . . . . . . . . 18 𝐴 ∈ ℝ+ → if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) = (abs‘(ℑ‘𝐴)))
11584, 114syl5eq 2817 . . . . . . . . . . . . . . . . 17 𝐴 ∈ ℝ+𝑆 = (abs‘(ℑ‘𝐴)))
116113, 115syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (ℑ‘𝐴) ≠ 0) → 𝑆 = (abs‘(ℑ‘𝐴)))
117110, 116syldan 579 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 𝑆 = (abs‘(ℑ‘𝐴)))
118 0re 10240 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
119 ltle 10326 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ ∧ (ℑ‘𝐴) ∈ ℝ) → (0 < (ℑ‘𝐴) → 0 ≤ (ℑ‘𝐴)))
120118, 87, 119sylancr 575 . . . . . . . . . . . . . . . . 17 (𝜑 → (0 < (ℑ‘𝐴) → 0 ≤ (ℑ‘𝐴)))
121120imp 393 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 ≤ (ℑ‘𝐴))
12277, 121absidd 14362 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (abs‘(ℑ‘𝐴)) = (ℑ‘𝐴))
123117, 122eqtrd 2805 . . . . . . . . . . . . . 14 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 𝑆 = (ℑ‘𝐴))
124108, 123breqtrd 4812 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (abs‘(𝐴𝐵)) < (ℑ‘𝐴))
12573, 75, 77, 83, 124lelttrd 10395 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(𝐴𝐵)) < (ℑ‘𝐴))
12670, 125eqbrtrrd 4810 . . . . . . . . . . 11 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘𝐴) − (ℑ‘𝐵)) < (ℑ‘𝐴))
12788adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ∈ ℂ)
128127subid1d 10581 . . . . . . . . . . 11 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘𝐴) − 0) = (ℑ‘𝐴))
129126, 128breqtrrd 4814 . . . . . . . . . 10 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘𝐴) − (ℑ‘𝐵)) < ((ℑ‘𝐴) − 0))
130 0red 10241 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℝ)
1318imcld 14136 . . . . . . . . . . . 12 (𝜑 → (ℑ‘𝐵) ∈ ℝ)
132130, 131, 87ltsub2d 10837 . . . . . . . . . . 11 (𝜑 → (0 < (ℑ‘𝐵) ↔ ((ℑ‘𝐴) − (ℑ‘𝐵)) < ((ℑ‘𝐴) − 0)))
133132adantr 466 . . . . . . . . . 10 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 < (ℑ‘𝐵) ↔ ((ℑ‘𝐴) − (ℑ‘𝐵)) < ((ℑ‘𝐴) − 0)))
134129, 133mpbird 247 . . . . . . . . 9 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 < (ℑ‘𝐵))
135 argimgt0 24572 . . . . . . . . 9 ((𝐵 ∈ ℂ ∧ 0 < (ℑ‘𝐵)) → (ℑ‘(log‘𝐵)) ∈ (0(,)π))
13668, 134, 135syl2anc 573 . . . . . . . 8 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐵)) ∈ (0(,)π))
137 eliooord 12431 . . . . . . . 8 ((ℑ‘(log‘𝐵)) ∈ (0(,)π) → (0 < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) < π))
138136, 137syl 17 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) < π))
139138simpld 482 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 < (ℑ‘(log‘𝐵)))
140130, 12, 21ltsub1d 10836 . . . . . . 7 (𝜑 → (0 < (ℑ‘(log‘𝐵)) ↔ (0 − (ℑ‘(log‘𝐴))) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴)))))
141140adantr 466 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 < (ℑ‘(log‘𝐵)) ↔ (0 − (ℑ‘(log‘𝐴))) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴)))))
142139, 141mpbid 222 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 − (ℑ‘(log‘𝐴))) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
14367, 142syl5eqbr 4821 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -(ℑ‘(log‘𝐴)) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
14454, 56, 57, 66, 143lttrd 10398 . . 3 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
145 lttri4 10322 . . . 4 (((ℑ‘𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℑ‘𝐴) < 0 ∨ (ℑ‘𝐴) = 0 ∨ 0 < (ℑ‘𝐴)))
14687, 118, 145sylancl 574 . . 3 (𝜑 → ((ℑ‘𝐴) < 0 ∨ (ℑ‘𝐴) = 0 ∨ 0 < (ℑ‘𝐴)))
14739, 53, 144, 146mpjao3dan 1543 . 2 (𝜑 → -π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
1481a1i 11 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → π ∈ ℝ)
14930renegcld 10657 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -(ℑ‘(log‘𝐴)) ∈ ℝ)
1508adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (ℑ‘𝐴) < 0) → 𝐵 ∈ ℂ)
15188adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) ∈ ℂ)
152151subid1d 10581 . . . . . . . . . . . 12 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘𝐴) − 0) = (ℑ‘𝐴))
15387adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) ∈ ℝ)
15474renegcld 10657 . . . . . . . . . . . . . . 15 (𝜑 → -(abs‘(𝐴𝐵)) ∈ ℝ)
155154adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -(abs‘(𝐴𝐵)) ∈ ℝ)
15672adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(𝐴𝐵)) ∈ ℝ)
15774adantr 466 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (abs‘(𝐴𝐵)) ∈ ℝ)
158107adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (abs‘(𝐴𝐵)) < 𝑆)
159118ltnri 10346 . . . . . . . . . . . . . . . . . . . 20 ¬ 0 < 0
160 breq1 4789 . . . . . . . . . . . . . . . . . . . 20 ((ℑ‘𝐴) = 0 → ((ℑ‘𝐴) < 0 ↔ 0 < 0))
161159, 160mtbiri 316 . . . . . . . . . . . . . . . . . . 19 ((ℑ‘𝐴) = 0 → ¬ (ℑ‘𝐴) < 0)
162161necon2ai 2972 . . . . . . . . . . . . . . . . . 18 ((ℑ‘𝐴) < 0 → (ℑ‘𝐴) ≠ 0)
163162, 116sylan2 580 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (ℑ‘𝐴) < 0) → 𝑆 = (abs‘(ℑ‘𝐴)))
164 ltle 10326 . . . . . . . . . . . . . . . . . . . 20 (((ℑ‘𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℑ‘𝐴) < 0 → (ℑ‘𝐴) ≤ 0))
16587, 118, 164sylancl 574 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℑ‘𝐴) < 0 → (ℑ‘𝐴) ≤ 0))
166165imp 393 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) ≤ 0)
167153, 166absnidd 14353 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (abs‘(ℑ‘𝐴)) = -(ℑ‘𝐴))
168163, 167eqtrd 2805 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (ℑ‘𝐴) < 0) → 𝑆 = -(ℑ‘𝐴))
169158, 168breqtrd 4812 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (abs‘(𝐴𝐵)) < -(ℑ‘𝐴))
170157, 153, 169ltnegcon2d 10808 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) < -(abs‘(𝐴𝐵)))
17181simpld 482 . . . . . . . . . . . . . . 15 (𝜑 → -(abs‘(𝐴𝐵)) ≤ (ℑ‘(𝐴𝐵)))
172171adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -(abs‘(𝐴𝐵)) ≤ (ℑ‘(𝐴𝐵)))
173153, 155, 156, 170, 172ltletrd 10397 . . . . . . . . . . . . 13 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) < (ℑ‘(𝐴𝐵)))
17469adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(𝐴𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
175173, 174breqtrd 4812 . . . . . . . . . . . 12 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) < ((ℑ‘𝐴) − (ℑ‘𝐵)))
176152, 175eqbrtrd 4808 . . . . . . . . . . 11 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘𝐴) − 0) < ((ℑ‘𝐴) − (ℑ‘𝐵)))
177150imcld 14136 . . . . . . . . . . . 12 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐵) ∈ ℝ)
178177, 31, 153ltsub2d 10837 . . . . . . . . . . 11 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘𝐵) < 0 ↔ ((ℑ‘𝐴) − 0) < ((ℑ‘𝐴) − (ℑ‘𝐵))))
179176, 178mpbird 247 . . . . . . . . . 10 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐵) < 0)
180 argimlt0 24573 . . . . . . . . . 10 ((𝐵 ∈ ℂ ∧ (ℑ‘𝐵) < 0) → (ℑ‘(log‘𝐵)) ∈ (-π(,)0))
181150, 179, 180syl2anc 573 . . . . . . . . 9 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) ∈ (-π(,)0))
182 eliooord 12431 . . . . . . . . 9 ((ℑ‘(log‘𝐵)) ∈ (-π(,)0) → (-π < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) < 0))
183181, 182syl 17 . . . . . . . 8 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (-π < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) < 0))
184183simprd 483 . . . . . . 7 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) < 0)
18513, 31, 30, 184ltsub1dd 10839 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < (0 − (ℑ‘(log‘𝐴))))
186185, 67syl6breqr 4828 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < -(ℑ‘(log‘𝐴)))
18735simpld 482 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -π < (ℑ‘(log‘𝐴)))
188 ltnegcon1 10729 . . . . . . 7 ((π ∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π < (ℑ‘(log‘𝐴)) ↔ -(ℑ‘(log‘𝐴)) < π))
1891, 30, 188sylancr 575 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (-π < (ℑ‘(log‘𝐴)) ↔ -(ℑ‘(log‘𝐴)) < π))
190187, 189mpbid 222 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -(ℑ‘(log‘𝐴)) < π)
19123, 149, 148, 186, 190lttrd 10398 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < π)
19223, 148, 191ltled 10385 . . 3 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)
19324simprd 483 . . . . 5 (𝜑 → (ℑ‘(log‘𝐵)) ≤ π)
194193adantr 466 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) = 0) → (ℑ‘(log‘𝐵)) ≤ π)
19552, 194eqbrtrd 4808 . . 3 ((𝜑 ∧ (ℑ‘𝐴) = 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)
1961a1i 11 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → π ∈ ℝ)
19712adantr 466 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐵)) ∈ ℝ)
198 0red 10241 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 ∈ ℝ)
19921adantr 466 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ ℝ)
20061simpld 482 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 < (ℑ‘(log‘𝐴)))
201198, 199, 197, 200ltsub2dd 10840 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < ((ℑ‘(log‘𝐵)) − 0))
20227adantr 466 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐵)) ∈ ℂ)
203202subid1d 10581 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − 0) = (ℑ‘(log‘𝐵)))
204201, 203breqtrd 4812 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < (ℑ‘(log‘𝐵)))
205138simprd 483 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐵)) < π)
20657, 197, 196, 204, 205lttrd 10398 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < π)
20757, 196, 206ltled 10385 . . 3 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)
208192, 195, 207, 146mpjao3dan 1543 . 2 (𝜑 → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)
209147, 208jca 501 1 (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3o 1070   = wceq 1631  wcel 2145  wne 2943  cdif 3720  ifcif 4225   class class class wbr 4786  cfv 6029  (class class class)co 6791  cc 10134  cr 10135  0cc0 10136  1c1 10137   + caddc 10139   · cmul 10141  -∞cmnf 10272   < clt 10274  cle 10275  cmin 10466  -cneg 10467   / cdiv 10884  +crp 12028  (,)cioo 12373  (,]cioc 12374  cim 14039  abscabs 14175  πcpi 14996  logclog 24515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-inf2 8700  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213  ax-pre-sup 10214  ax-addf 10215  ax-mulf 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-isom 6038  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-of 7042  df-om 7211  df-1st 7313  df-2nd 7314  df-supp 7445  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-2o 7712  df-oadd 7715  df-er 7894  df-map 8009  df-pm 8010  df-ixp 8061  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-fsupp 8430  df-fi 8471  df-sup 8502  df-inf 8503  df-oi 8569  df-card 8963  df-cda 9190  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-div 10885  df-nn 11221  df-2 11279  df-3 11280  df-4 11281  df-5 11282  df-6 11283  df-7 11284  df-8 11285  df-9 11286  df-n0 11493  df-z 11578  df-dec 11694  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12144  df-xadd 12145  df-xmul 12146  df-ioo 12377  df-ioc 12378  df-ico 12379  df-icc 12380  df-fz 12527  df-fzo 12667  df-fl 12794  df-mod 12870  df-seq 13002  df-exp 13061  df-fac 13258  df-bc 13287  df-hash 13315  df-shft 14008  df-cj 14040  df-re 14041  df-im 14042  df-sqrt 14176  df-abs 14177  df-limsup 14403  df-clim 14420  df-rlim 14421  df-sum 14618  df-ef 14997  df-sin 14999  df-cos 15000  df-pi 15002  df-struct 16059  df-ndx 16060  df-slot 16061  df-base 16063  df-sets 16064  df-ress 16065  df-plusg 16155  df-mulr 16156  df-starv 16157  df-sca 16158  df-vsca 16159  df-ip 16160  df-tset 16161  df-ple 16162  df-ds 16165  df-unif 16166  df-hom 16167  df-cco 16168  df-rest 16284  df-topn 16285  df-0g 16303  df-gsum 16304  df-topgen 16305  df-pt 16306  df-prds 16309  df-xrs 16363  df-qtop 16368  df-imas 16369  df-xps 16371  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19946  df-xmet 19947  df-met 19948  df-bl 19949  df-mopn 19950  df-fbas 19951  df-fg 19952  df-cnfld 19955  df-top 20912  df-topon 20929  df-topsp 20951  df-bases 20964  df-cld 21037  df-ntr 21038  df-cls 21039  df-nei 21116  df-lp 21154  df-perf 21155  df-cn 21245  df-cnp 21246  df-haus 21333  df-tx 21579  df-hmeo 21772  df-fil 21863  df-fm 21955  df-flim 21956  df-flf 21957  df-xms 22338  df-ms 22339  df-tms 22340  df-cncf 22894  df-limc 23843  df-dv 23844  df-log 24517
This theorem is referenced by:  logcnlem4  24605
  Copyright terms: Public domain W3C validator