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

Theorem logcnlem3 25238
Description: Lemma for logcn 25241. (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 25054 . . . . . 6 π ∈ ℝ
21renegcli 10940 . . . . 5 -π ∈ ℝ
32a1i 11 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -π ∈ ℝ)
4 logcnlem.b . . . . . . . 8 (𝜑𝐵𝐷)
5 logcn.d . . . . . . . . . 10 𝐷 = (ℂ ∖ (-∞(,]0))
65ellogdm 25233 . . . . . . . . 9 (𝐵𝐷 ↔ (𝐵 ∈ ℂ ∧ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ+)))
76simplbi 501 . . . . . . . 8 (𝐵𝐷𝐵 ∈ ℂ)
84, 7syl 17 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
95logdmn0 25234 . . . . . . . 8 (𝐵𝐷𝐵 ≠ 0)
104, 9syl 17 . . . . . . 7 (𝜑𝐵 ≠ 0)
118, 10logcld 25165 . . . . . 6 (𝜑 → (log‘𝐵) ∈ ℂ)
1211imcld 14549 . . . . 5 (𝜑 → (ℑ‘(log‘𝐵)) ∈ ℝ)
1312adantr 484 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) ∈ ℝ)
14 logcnlem.a . . . . . . . . 9 (𝜑𝐴𝐷)
155ellogdm 25233 . . . . . . . . . 10 (𝐴𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+)))
1615simplbi 501 . . . . . . . . 9 (𝐴𝐷𝐴 ∈ ℂ)
1714, 16syl 17 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
185logdmn0 25234 . . . . . . . . 9 (𝐴𝐷𝐴 ≠ 0)
1914, 18syl 17 . . . . . . . 8 (𝜑𝐴 ≠ 0)
2017, 19logcld 25165 . . . . . . 7 (𝜑 → (log‘𝐴) ∈ ℂ)
2120imcld 14549 . . . . . 6 (𝜑 → (ℑ‘(log‘𝐴)) ∈ ℝ)
2212, 21resubcld 11061 . . . . 5 (𝜑 → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∈ ℝ)
2322adantr 484 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∈ ℝ)
248, 10logimcld 25166 . . . . . 6 (𝜑 → (-π < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) ≤ π))
2524simpld 498 . . . . 5 (𝜑 → -π < (ℑ‘(log‘𝐵)))
2625adantr 484 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -π < (ℑ‘(log‘𝐵)))
2712recnd 10662 . . . . . . 7 (𝜑 → (ℑ‘(log‘𝐵)) ∈ ℂ)
2827adantr 484 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) ∈ ℂ)
2928subid1d 10979 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − 0) = (ℑ‘(log‘𝐵)))
3021adantr 484 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ ℝ)
31 0red 10637 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → 0 ∈ ℝ)
32 argimlt0 25207 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0))
3317, 32sylan 583 . . . . . . . 8 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0))
34 eliooord 12788 . . . . . . . 8 ((ℑ‘(log‘𝐴)) ∈ (-π(,)0) → (-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < 0))
3533, 34syl 17 . . . . . . 7 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < 0))
3635simprd 499 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) < 0)
3730, 31, 13, 36ltsub2dd 11246 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − 0) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
3829, 37eqbrtrrd 5057 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
393, 13, 23, 26, 38lttrd 10794 . . 3 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
4025adantr 484 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) = 0) → -π < (ℑ‘(log‘𝐵)))
41 reim0b 14473 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
4217, 41syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
4315simprbi 500 . . . . . . . . . . 11 (𝐴𝐷 → (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))
4414, 43syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))
4542, 44sylbird 263 . . . . . . . . 9 (𝜑 → ((ℑ‘𝐴) = 0 → 𝐴 ∈ ℝ+))
4645imp 410 . . . . . . . 8 ((𝜑 ∧ (ℑ‘𝐴) = 0) → 𝐴 ∈ ℝ+)
4746relogcld 25217 . . . . . . 7 ((𝜑 ∧ (ℑ‘𝐴) = 0) → (log‘𝐴) ∈ ℝ)
4847reim0d 14579 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) = 0) → (ℑ‘(log‘𝐴)) = 0)
4948oveq2d 7155 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) = 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) = ((ℑ‘(log‘𝐵)) − 0))
5027subid1d 10979 . . . . . 6 (𝜑 → ((ℑ‘(log‘𝐵)) − 0) = (ℑ‘(log‘𝐵)))
5150adantr 484 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) = 0) → ((ℑ‘(log‘𝐵)) − 0) = (ℑ‘(log‘𝐵)))
5249, 51eqtrd 2836 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) = 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) = (ℑ‘(log‘𝐵)))
5340, 52breqtrrd 5061 . . 3 ((𝜑 ∧ (ℑ‘𝐴) = 0) → -π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
542a1i 11 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -π ∈ ℝ)
5521renegcld 11060 . . . . 5 (𝜑 → -(ℑ‘(log‘𝐴)) ∈ ℝ)
5655adantr 484 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -(ℑ‘(log‘𝐴)) ∈ ℝ)
5722adantr 484 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∈ ℝ)
58 argimgt0 25206 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π))
5917, 58sylan 583 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π))
60 eliooord 12788 . . . . . . 7 ((ℑ‘(log‘𝐴)) ∈ (0(,)π) → (0 < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < π))
6159, 60syl 17 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) < π))
6261simprd 499 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) < π)
63 ltneg 11133 . . . . . . 7 (((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘(log‘𝐴)) < π ↔ -π < -(ℑ‘(log‘𝐴))))
6421, 1, 63sylancl 589 . . . . . 6 (𝜑 → ((ℑ‘(log‘𝐴)) < π ↔ -π < -(ℑ‘(log‘𝐴))))
6564adantr 484 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐴)) < π ↔ -π < -(ℑ‘(log‘𝐴))))
6662, 65mpbid 235 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -π < -(ℑ‘(log‘𝐴)))
67 df-neg 10866 . . . . 5 -(ℑ‘(log‘𝐴)) = (0 − (ℑ‘(log‘𝐴)))
688adantr 484 . . . . . . . . 9 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 𝐵 ∈ ℂ)
6917, 8imsubd 14571 . . . . . . . . . . . . 13 (𝜑 → (ℑ‘(𝐴𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
7069adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(𝐴𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
7117, 8subcld 10990 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐵) ∈ ℂ)
7271imcld 14549 . . . . . . . . . . . . . 14 (𝜑 → (ℑ‘(𝐴𝐵)) ∈ ℝ)
7372adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(𝐴𝐵)) ∈ ℝ)
7471abscld 14791 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝐴𝐵)) ∈ ℝ)
7574adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (abs‘(𝐴𝐵)) ∈ ℝ)
7617adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 𝐴 ∈ ℂ)
7776imcld 14549 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ∈ ℝ)
78 absimle 14664 . . . . . . . . . . . . . . . . 17 ((𝐴𝐵) ∈ ℂ → (abs‘(ℑ‘(𝐴𝐵))) ≤ (abs‘(𝐴𝐵)))
7971, 78syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘(ℑ‘(𝐴𝐵))) ≤ (abs‘(𝐴𝐵)))
8072, 74absled 14785 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(ℑ‘(𝐴𝐵))) ≤ (abs‘(𝐴𝐵)) ↔ (-(abs‘(𝐴𝐵)) ≤ (ℑ‘(𝐴𝐵)) ∧ (ℑ‘(𝐴𝐵)) ≤ (abs‘(𝐴𝐵)))))
8179, 80mpbid 235 . . . . . . . . . . . . . . 15 (𝜑 → (-(abs‘(𝐴𝐵)) ≤ (ℑ‘(𝐴𝐵)) ∧ (ℑ‘(𝐴𝐵)) ≤ (abs‘(𝐴𝐵))))
8281simprd 499 . . . . . . . . . . . . . 14 (𝜑 → (ℑ‘(𝐴𝐵)) ≤ (abs‘(𝐴𝐵)))
8382adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(𝐴𝐵)) ≤ (abs‘(𝐴𝐵)))
84 logcnlem.s . . . . . . . . . . . . . . . . . 18 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴)))
85 rpre 12389 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
8685adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐴 ∈ ℝ+) → 𝐴 ∈ ℝ)
8717imcld 14549 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (ℑ‘𝐴) ∈ ℝ)
8887recnd 10662 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (ℑ‘𝐴) ∈ ℂ)
8988abscld 14791 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ)
9089adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ+) → (abs‘(ℑ‘𝐴)) ∈ ℝ)
9186, 90ifclda 4462 . . . . . . . . . . . . . . . . . 18 (𝜑 → if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) ∈ ℝ)
9284, 91eqeltrid 2897 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ ℝ)
93 logcnlem.t . . . . . . . . . . . . . . . . . 18 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅)))
9417abscld 14791 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘𝐴) ∈ ℝ)
95 logcnlem.r . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑅 ∈ ℝ+)
9695rpred 12423 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 ∈ ℝ)
97 1rp 12385 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ+
98 rpaddcl 12403 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ+𝑅 ∈ ℝ+) → (1 + 𝑅) ∈ ℝ+)
9997, 95, 98sylancr 590 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 + 𝑅) ∈ ℝ+)
10096, 99rerpdivcld 12454 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑅 / (1 + 𝑅)) ∈ ℝ)
10194, 100remulcld 10664 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) ∈ ℝ)
10293, 101eqeltrid 2897 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ ℝ)
10392, 102ifcld 4473 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑆𝑇, 𝑆, 𝑇) ∈ ℝ)
104 logcnlem.l . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘(𝐴𝐵)) < if(𝑆𝑇, 𝑆, 𝑇))
105 min1 12574 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ) → if(𝑆𝑇, 𝑆, 𝑇) ≤ 𝑆)
10692, 102, 105syl2anc 587 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑆𝑇, 𝑆, 𝑇) ≤ 𝑆)
10774, 103, 92, 104, 106ltletrd 10793 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝐴𝐵)) < 𝑆)
108107adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (abs‘(𝐴𝐵)) < 𝑆)
109 gt0ne0 11098 . . . . . . . . . . . . . . . . 17 (((ℑ‘𝐴) ∈ ℝ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ≠ 0)
11087, 109sylan 583 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ≠ 0)
11185, 42syl5ib 247 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 ∈ ℝ+ → (ℑ‘𝐴) = 0))
112111necon3ad 3003 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((ℑ‘𝐴) ≠ 0 → ¬ 𝐴 ∈ ℝ+))
113112imp 410 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (ℑ‘𝐴) ≠ 0) → ¬ 𝐴 ∈ ℝ+)
114 iffalse 4437 . . . . . . . . . . . . . . . . . 18 𝐴 ∈ ℝ+ → if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) = (abs‘(ℑ‘𝐴)))
11584, 114syl5eq 2848 . . . . . . . . . . . . . . . . 17 𝐴 ∈ ℝ+𝑆 = (abs‘(ℑ‘𝐴)))
116113, 115syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (ℑ‘𝐴) ≠ 0) → 𝑆 = (abs‘(ℑ‘𝐴)))
117110, 116syldan 594 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 𝑆 = (abs‘(ℑ‘𝐴)))
118 0re 10636 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
119 ltle 10722 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ ∧ (ℑ‘𝐴) ∈ ℝ) → (0 < (ℑ‘𝐴) → 0 ≤ (ℑ‘𝐴)))
120118, 87, 119sylancr 590 . . . . . . . . . . . . . . . . 17 (𝜑 → (0 < (ℑ‘𝐴) → 0 ≤ (ℑ‘𝐴)))
121120imp 410 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 ≤ (ℑ‘𝐴))
12277, 121absidd 14777 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (abs‘(ℑ‘𝐴)) = (ℑ‘𝐴))
123117, 122eqtrd 2836 . . . . . . . . . . . . . 14 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 𝑆 = (ℑ‘𝐴))
124108, 123breqtrd 5059 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (abs‘(𝐴𝐵)) < (ℑ‘𝐴))
12573, 75, 77, 83, 124lelttrd 10791 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(𝐴𝐵)) < (ℑ‘𝐴))
12670, 125eqbrtrrd 5057 . . . . . . . . . . 11 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘𝐴) − (ℑ‘𝐵)) < (ℑ‘𝐴))
12788adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘𝐴) ∈ ℂ)
128127subid1d 10979 . . . . . . . . . . 11 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘𝐴) − 0) = (ℑ‘𝐴))
129126, 128breqtrrd 5061 . . . . . . . . . 10 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘𝐴) − (ℑ‘𝐵)) < ((ℑ‘𝐴) − 0))
130 0red 10637 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℝ)
1318imcld 14549 . . . . . . . . . . . 12 (𝜑 → (ℑ‘𝐵) ∈ ℝ)
132130, 131, 87ltsub2d 11243 . . . . . . . . . . 11 (𝜑 → (0 < (ℑ‘𝐵) ↔ ((ℑ‘𝐴) − (ℑ‘𝐵)) < ((ℑ‘𝐴) − 0)))
133132adantr 484 . . . . . . . . . 10 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 < (ℑ‘𝐵) ↔ ((ℑ‘𝐴) − (ℑ‘𝐵)) < ((ℑ‘𝐴) − 0)))
134129, 133mpbird 260 . . . . . . . . 9 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 < (ℑ‘𝐵))
135 argimgt0 25206 . . . . . . . . 9 ((𝐵 ∈ ℂ ∧ 0 < (ℑ‘𝐵)) → (ℑ‘(log‘𝐵)) ∈ (0(,)π))
13668, 134, 135syl2anc 587 . . . . . . . 8 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐵)) ∈ (0(,)π))
137 eliooord 12788 . . . . . . . 8 ((ℑ‘(log‘𝐵)) ∈ (0(,)π) → (0 < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) < π))
138136, 137syl 17 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) < π))
139138simpld 498 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 < (ℑ‘(log‘𝐵)))
140130, 12, 21ltsub1d 11242 . . . . . . 7 (𝜑 → (0 < (ℑ‘(log‘𝐵)) ↔ (0 − (ℑ‘(log‘𝐴))) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴)))))
141140adantr 484 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 < (ℑ‘(log‘𝐵)) ↔ (0 − (ℑ‘(log‘𝐴))) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴)))))
142139, 141mpbid 235 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (0 − (ℑ‘(log‘𝐴))) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
14367, 142eqbrtrid 5068 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -(ℑ‘(log‘𝐴)) < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
14454, 56, 57, 66, 143lttrd 10794 . . 3 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → -π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
145 lttri4 10718 . . . 4 (((ℑ‘𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℑ‘𝐴) < 0 ∨ (ℑ‘𝐴) = 0 ∨ 0 < (ℑ‘𝐴)))
14687, 118, 145sylancl 589 . . 3 (𝜑 → ((ℑ‘𝐴) < 0 ∨ (ℑ‘𝐴) = 0 ∨ 0 < (ℑ‘𝐴)))
14739, 53, 144, 146mpjao3dan 1428 . 2 (𝜑 → -π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))))
1481a1i 11 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → π ∈ ℝ)
14930renegcld 11060 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -(ℑ‘(log‘𝐴)) ∈ ℝ)
1508adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (ℑ‘𝐴) < 0) → 𝐵 ∈ ℂ)
15188adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) ∈ ℂ)
152151subid1d 10979 . . . . . . . . . . . 12 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘𝐴) − 0) = (ℑ‘𝐴))
15387adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) ∈ ℝ)
15474renegcld 11060 . . . . . . . . . . . . . . 15 (𝜑 → -(abs‘(𝐴𝐵)) ∈ ℝ)
155154adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -(abs‘(𝐴𝐵)) ∈ ℝ)
15672adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(𝐴𝐵)) ∈ ℝ)
15774adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (abs‘(𝐴𝐵)) ∈ ℝ)
158107adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (abs‘(𝐴𝐵)) < 𝑆)
159118ltnri 10742 . . . . . . . . . . . . . . . . . . . 20 ¬ 0 < 0
160 breq1 5036 . . . . . . . . . . . . . . . . . . . 20 ((ℑ‘𝐴) = 0 → ((ℑ‘𝐴) < 0 ↔ 0 < 0))
161159, 160mtbiri 330 . . . . . . . . . . . . . . . . . . 19 ((ℑ‘𝐴) = 0 → ¬ (ℑ‘𝐴) < 0)
162161necon2ai 3019 . . . . . . . . . . . . . . . . . 18 ((ℑ‘𝐴) < 0 → (ℑ‘𝐴) ≠ 0)
163162, 116sylan2 595 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (ℑ‘𝐴) < 0) → 𝑆 = (abs‘(ℑ‘𝐴)))
164 ltle 10722 . . . . . . . . . . . . . . . . . . . 20 (((ℑ‘𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℑ‘𝐴) < 0 → (ℑ‘𝐴) ≤ 0))
16587, 118, 164sylancl 589 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℑ‘𝐴) < 0 → (ℑ‘𝐴) ≤ 0))
166165imp 410 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) ≤ 0)
167153, 166absnidd 14768 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (abs‘(ℑ‘𝐴)) = -(ℑ‘𝐴))
168163, 167eqtrd 2836 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (ℑ‘𝐴) < 0) → 𝑆 = -(ℑ‘𝐴))
169158, 168breqtrd 5059 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (abs‘(𝐴𝐵)) < -(ℑ‘𝐴))
170157, 153, 169ltnegcon2d 11214 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) < -(abs‘(𝐴𝐵)))
17181simpld 498 . . . . . . . . . . . . . . 15 (𝜑 → -(abs‘(𝐴𝐵)) ≤ (ℑ‘(𝐴𝐵)))
172171adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -(abs‘(𝐴𝐵)) ≤ (ℑ‘(𝐴𝐵)))
173153, 155, 156, 170, 172ltletrd 10793 . . . . . . . . . . . . 13 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) < (ℑ‘(𝐴𝐵)))
17469adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(𝐴𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
175173, 174breqtrd 5059 . . . . . . . . . . . 12 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐴) < ((ℑ‘𝐴) − (ℑ‘𝐵)))
176152, 175eqbrtrd 5055 . . . . . . . . . . 11 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘𝐴) − 0) < ((ℑ‘𝐴) − (ℑ‘𝐵)))
177150imcld 14549 . . . . . . . . . . . 12 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐵) ∈ ℝ)
178177, 31, 153ltsub2d 11243 . . . . . . . . . . 11 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘𝐵) < 0 ↔ ((ℑ‘𝐴) − 0) < ((ℑ‘𝐴) − (ℑ‘𝐵))))
179176, 178mpbird 260 . . . . . . . . . 10 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘𝐵) < 0)
180 argimlt0 25207 . . . . . . . . . 10 ((𝐵 ∈ ℂ ∧ (ℑ‘𝐵) < 0) → (ℑ‘(log‘𝐵)) ∈ (-π(,)0))
181150, 179, 180syl2anc 587 . . . . . . . . 9 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) ∈ (-π(,)0))
182 eliooord 12788 . . . . . . . . 9 ((ℑ‘(log‘𝐵)) ∈ (-π(,)0) → (-π < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) < 0))
183181, 182syl 17 . . . . . . . 8 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (-π < (ℑ‘(log‘𝐵)) ∧ (ℑ‘(log‘𝐵)) < 0))
184183simprd 499 . . . . . . 7 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐵)) < 0)
18513, 31, 30, 184ltsub1dd 11245 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < (0 − (ℑ‘(log‘𝐴))))
186185, 67breqtrrdi 5075 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < -(ℑ‘(log‘𝐴)))
18735simpld 498 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -π < (ℑ‘(log‘𝐴)))
188 ltnegcon1 11134 . . . . . . 7 ((π ∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π < (ℑ‘(log‘𝐴)) ↔ -(ℑ‘(log‘𝐴)) < π))
1891, 30, 188sylancr 590 . . . . . 6 ((𝜑 ∧ (ℑ‘𝐴) < 0) → (-π < (ℑ‘(log‘𝐴)) ↔ -(ℑ‘(log‘𝐴)) < π))
190187, 189mpbid 235 . . . . 5 ((𝜑 ∧ (ℑ‘𝐴) < 0) → -(ℑ‘(log‘𝐴)) < π)
19123, 149, 148, 186, 190lttrd 10794 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < π)
19223, 148, 191ltled 10781 . . 3 ((𝜑 ∧ (ℑ‘𝐴) < 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)
19324simprd 499 . . . . 5 (𝜑 → (ℑ‘(log‘𝐵)) ≤ π)
194193adantr 484 . . . 4 ((𝜑 ∧ (ℑ‘𝐴) = 0) → (ℑ‘(log‘𝐵)) ≤ π)
19552, 194eqbrtrd 5055 . . 3 ((𝜑 ∧ (ℑ‘𝐴) = 0) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)
1961a1i 11 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → π ∈ ℝ)
19712adantr 484 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐵)) ∈ ℝ)
198 0red 10637 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 ∈ ℝ)
19921adantr 484 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ ℝ)
20061simpld 498 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → 0 < (ℑ‘(log‘𝐴)))
201198, 199, 197, 200ltsub2dd 11246 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < ((ℑ‘(log‘𝐵)) − 0))
20227adantr 484 . . . . . . 7 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐵)) ∈ ℂ)
203202subid1d 10979 . . . . . 6 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − 0) = (ℑ‘(log‘𝐵)))
204201, 203breqtrd 5059 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < (ℑ‘(log‘𝐵)))
205138simprd 499 . . . . 5 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐵)) < π)
20657, 197, 196, 204, 205lttrd 10794 . . . 4 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) < π)
20757, 196, 206ltled 10781 . . 3 ((𝜑 ∧ 0 < (ℑ‘𝐴)) → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)
208192, 195, 207, 146mpjao3dan 1428 . 2 (𝜑 → ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)
209147, 208jca 515 1 (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3o 1083   = wceq 1538  wcel 2112  wne 2990  cdif 3881  ifcif 4428   class class class wbr 5033  cfv 6328  (class class class)co 7139  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  -∞cmnf 10666   < clt 10668  cle 10669  cmin 10863  -cneg 10864   / cdiv 11290  +crp 12381  (,)cioo 12730  (,]cioc 12731  cim 14452  abscabs 14588  πcpi 15415  logclog 25149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609  ax-mulf 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ioc 12735  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-mod 13237  df-seq 13369  df-exp 13430  df-fac 13634  df-bc 13663  df-hash 13691  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-ef 15416  df-sin 15418  df-cos 15419  df-pi 15421  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18220  df-cntz 18442  df-cmn 18903  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-mopn 20090  df-fbas 20091  df-fg 20092  df-cnfld 20095  df-top 21502  df-topon 21519  df-topsp 21541  df-bases 21554  df-cld 21627  df-ntr 21628  df-cls 21629  df-nei 21706  df-lp 21744  df-perf 21745  df-cn 21835  df-cnp 21836  df-haus 21923  df-tx 22170  df-hmeo 22363  df-fil 22454  df-fm 22546  df-flim 22547  df-flf 22548  df-xms 22930  df-ms 22931  df-tms 22932  df-cncf 23486  df-limc 24472  df-dv 24473  df-log 25151
This theorem is referenced by:  logcnlem4  25239
  Copyright terms: Public domain W3C validator