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

Theorem lgamgulmlem2 24955
Description: Lemma for lgamgulm 24960. (Contributed by Mario Carneiro, 3-Jul-2017.)
Hypotheses
Ref Expression
lgamgulm.r (𝜑𝑅 ∈ ℕ)
lgamgulm.u 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}
lgamgulm.n (𝜑𝑁 ∈ ℕ)
lgamgulm.a (𝜑𝐴𝑈)
lgamgulm.l (𝜑 → (2 · 𝑅) ≤ 𝑁)
Assertion
Ref Expression
lgamgulmlem2 (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
Distinct variable groups:   𝑥,𝑁   𝑥,𝑘,𝑅   𝐴,𝑘,𝑥   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑘)   𝑈(𝑥,𝑘)   𝑁(𝑘)

Proof of Theorem lgamgulmlem2
Dummy variables 𝑦 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1elunit 12484 . . 3 1 ∈ (0[,]1)
2 0elunit 12483 . . 3 0 ∈ (0[,]1)
3 0red 10233 . . . 4 (𝜑 → 0 ∈ ℝ)
4 1red 10247 . . . 4 (𝜑 → 1 ∈ ℝ)
5 eqid 2760 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
65subcn 22870 . . . . . 6 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
76a1i 11 . . . . 5 (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
8 lgamgulm.r . . . . . . . . . . 11 (𝜑𝑅 ∈ ℕ)
9 lgamgulm.u . . . . . . . . . . 11 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}
108, 9lgamgulmlem1 24954 . . . . . . . . . 10 (𝜑𝑈 ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
11 lgamgulm.a . . . . . . . . . 10 (𝜑𝐴𝑈)
1210, 11sseldd 3745 . . . . . . . . 9 (𝜑𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
1312eldifad 3727 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
14 lgamgulm.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
1514nnred 11227 . . . . . . . . 9 (𝜑𝑁 ∈ ℝ)
1615recnd 10260 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
1714nnne0d 11257 . . . . . . . 8 (𝜑𝑁 ≠ 0)
1813, 16, 17divcld 10993 . . . . . . 7 (𝜑 → (𝐴 / 𝑁) ∈ ℂ)
19 unitssre 12512 . . . . . . . . 9 (0[,]1) ⊆ ℝ
20 ax-resscn 10185 . . . . . . . . 9 ℝ ⊆ ℂ
2119, 20sstri 3753 . . . . . . . 8 (0[,]1) ⊆ ℂ
2221a1i 11 . . . . . . 7 (𝜑 → (0[,]1) ⊆ ℂ)
23 ssid 3765 . . . . . . . 8 ℂ ⊆ ℂ
2423a1i 11 . . . . . . 7 (𝜑 → ℂ ⊆ ℂ)
25 cncfmptc 22915 . . . . . . 7 (((𝐴 / 𝑁) ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ (𝐴 / 𝑁)) ∈ ((0[,]1)–cn→ℂ))
2618, 22, 24, 25syl3anc 1477 . . . . . 6 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (𝐴 / 𝑁)) ∈ ((0[,]1)–cn→ℂ))
27 cncfmptid 22916 . . . . . . 7 (((0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
2821, 24, 27sylancr 698 . . . . . 6 (𝜑 → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
2926, 28mulcncf 23415 . . . . 5 (𝜑 → (𝑡 ∈ (0[,]1) ↦ ((𝐴 / 𝑁) · 𝑡)) ∈ ((0[,]1)–cn→ℂ))
3018adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0[,]1)) → (𝐴 / 𝑁) ∈ ℂ)
31 simpr 479 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
3219, 31sseldi 3742 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℝ)
3332recnd 10260 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ)
3430, 33mulcld 10252 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0[,]1)) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
35 1cnd 10248 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0[,]1)) → 1 ∈ ℂ)
3634, 35addcld 10251 . . . . . . . . 9 ((𝜑𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
37 rere 14061 . . . . . . . . . . . 12 ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) + 1))
3837adantl 473 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) + 1))
3936recld 14133 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ)
4034recld 14133 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ)
4140recnd 10260 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
4241abscld 14374 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ∈ ℝ)
4334abscld 14374 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ)
44 1red 10247 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → 1 ∈ ℝ)
45 absrele 14247 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 / 𝑁) · 𝑡) ∈ ℂ → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ≤ (abs‘((𝐴 / 𝑁) · 𝑡)))
4634, 45syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ≤ (abs‘((𝐴 / 𝑁) · 𝑡)))
4744rehalfcld 11471 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0[,]1)) → (1 / 2) ∈ ℝ)
488nnred 11227 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ∈ ℝ)
4948adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ)
5014adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → 𝑁 ∈ ℕ)
5149, 50nndivred 11261 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ∈ ℝ)
5218abscld 14374 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (abs‘(𝐴 / 𝑁)) ∈ ℝ)
5352adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(𝐴 / 𝑁)) ∈ ℝ)
5430absge0d 14382 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → 0 ≤ (abs‘(𝐴 / 𝑁)))
55 0re 10232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ ℝ
56 1re 10231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
5755, 56elicc2i 12432 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
5857simp2bi 1141 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ (0[,]1) → 0 ≤ 𝑡)
5958adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → 0 ≤ 𝑡)
6013, 16, 17absdivd 14393 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / (abs‘𝑁)))
6114nnrpd 12063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℝ+)
6261rpge0d 12069 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 ≤ 𝑁)
6315, 62absidd 14360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (abs‘𝑁) = 𝑁)
6463oveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((abs‘𝐴) / (abs‘𝑁)) = ((abs‘𝐴) / 𝑁))
6560, 64eqtr2d 2795 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((abs‘𝐴) / 𝑁) = (abs‘(𝐴 / 𝑁)))
6613abscld 14374 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (abs‘𝐴) ∈ ℝ)
67 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = 𝐴 → (abs‘𝑥) = (abs‘𝐴))
6867breq1d 4814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = 𝐴 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝐴) ≤ 𝑅))
69 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = 𝐴 → (𝑥 + 𝑘) = (𝐴 + 𝑘))
7069fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = 𝐴 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝐴 + 𝑘)))
7170breq2d 4816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = 𝐴 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
7271ralbidv 3124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = 𝐴 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
7368, 72anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = 𝐴 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))))
7473, 9elrab2 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴𝑈 ↔ (𝐴 ∈ ℂ ∧ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))))
7574simprbi 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴𝑈 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
7611, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
7776simpld 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (abs‘𝐴) ≤ 𝑅)
7866, 48, 61, 77lediv1dd 12123 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((abs‘𝐴) / 𝑁) ≤ (𝑅 / 𝑁))
7965, 78eqbrtrrd 4828 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (abs‘(𝐴 / 𝑁)) ≤ (𝑅 / 𝑁))
8079adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(𝐴 / 𝑁)) ≤ (𝑅 / 𝑁))
8157simp3bi 1142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ (0[,]1) → 𝑡 ≤ 1)
8281adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → 𝑡 ≤ 1)
8353, 51, 32, 44, 54, 59, 80, 82lemul12ad 11158 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · 𝑡) ≤ ((𝑅 / 𝑁) · 1))
8430, 33absmuld 14392 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) = ((abs‘(𝐴 / 𝑁)) · (abs‘𝑡)))
8532, 59absidd 14360 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘𝑡) = 𝑡)
8685oveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · (abs‘𝑡)) = ((abs‘(𝐴 / 𝑁)) · 𝑡))
8784, 86eqtr2d 2795 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · 𝑡) = (abs‘((𝐴 / 𝑁) · 𝑡)))
8851recnd 10260 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ∈ ℂ)
8988mulid1d 10249 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → ((𝑅 / 𝑁) · 1) = (𝑅 / 𝑁))
9083, 87, 893brtr3d 4835 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁))
91 lgamgulm.l . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (2 · 𝑅) ≤ 𝑁)
92 2rp 12030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ+
9392a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 2 ∈ ℝ+)
9448, 15, 93lemuldiv2d 12115 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((2 · 𝑅) ≤ 𝑁𝑅 ≤ (𝑁 / 2)))
9591, 94mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ≤ (𝑁 / 2))
96 2cnd 11285 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 2 ∈ ℂ)
97 2ne0 11305 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ≠ 0
9897a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 2 ≠ 0)
9916, 96, 98divrecd 10996 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
10095, 99breqtrd 4830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ≤ (𝑁 · (1 / 2)))
1014rehalfcld 11471 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1 / 2) ∈ ℝ)
10248, 101, 61ledivmuld 12118 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑅 / 𝑁) ≤ (1 / 2) ↔ 𝑅 ≤ (𝑁 · (1 / 2))))
103100, 102mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑅 / 𝑁) ≤ (1 / 2))
104103adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ≤ (1 / 2))
10543, 51, 47, 90, 104letrd 10386 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (1 / 2))
106 halflt1 11442 . . . . . . . . . . . . . . . . . . . . 21 (1 / 2) < 1
107106a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0[,]1)) → (1 / 2) < 1)
10843, 47, 44, 105, 107lelttrd 10387 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) < 1)
10942, 43, 44, 46, 108lelttrd 10387 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) < 1)
11040, 44absltd 14367 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0[,]1)) → ((abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) < 1 ↔ (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∧ (ℜ‘((𝐴 / 𝑁) · 𝑡)) < 1)))
111109, 110mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0[,]1)) → (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∧ (ℜ‘((𝐴 / 𝑁) · 𝑡)) < 1))
112111simpld 477 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0[,]1)) → -1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)))
11344renegcld 10649 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0[,]1)) → -1 ∈ ℝ)
114113, 40posdifd 10806 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0[,]1)) → (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ↔ 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1)))
115112, 114mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0[,]1)) → 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1))
11641, 35subnegd 10591 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0[,]1)) → ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
117115, 116breqtrd 4830 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0[,]1)) → 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
11834, 35readdd 14153 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + (ℜ‘1)))
119 re1 14093 . . . . . . . . . . . . . . . 16 (ℜ‘1) = 1
120119oveq2i 6824 . . . . . . . . . . . . . . 15 ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + (ℜ‘1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1)
121118, 120syl6eq 2810 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
122117, 121breqtrrd 4832 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0[,]1)) → 0 < (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)))
12339, 122elrpd 12062 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ+)
124123adantr 472 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ+)
12538, 124eqeltrrd 2840 . . . . . . . . . 10 (((𝜑𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ+)
126125ex 449 . . . . . . . . 9 ((𝜑𝑡 ∈ (0[,]1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ+))
127 eqid 2760 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
128127ellogdm 24584 . . . . . . . . 9 ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) ↔ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ ∧ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ+)))
12936, 126, 128sylanbrc 701 . . . . . . . 8 ((𝜑𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)))
130 eqidd 2761 . . . . . . . 8 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)))
131127logcn 24592 . . . . . . . . . . 11 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
132131a1i 11 . . . . . . . . . 10 (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
133 cncff 22897 . . . . . . . . . 10 ((log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ) → (log ↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖ (-∞(,]0))⟶ℂ)
134132, 133syl 17 . . . . . . . . 9 (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖ (-∞(,]0))⟶ℂ)
135134feqmptd 6411 . . . . . . . 8 (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦)))
136 fveq2 6352 . . . . . . . 8 (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦) = ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)))
137129, 130, 135, 136fmptco 6559 . . . . . . 7 (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1))))
138 fvres 6368 . . . . . . . . 9 ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
139129, 138syl 17 . . . . . . . 8 ((𝜑𝑡 ∈ (0[,]1)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
140139mpteq2dva 4896 . . . . . . 7 (𝜑 → (𝑡 ∈ (0[,]1) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))
141137, 140eqtrd 2794 . . . . . 6 (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))
142 eqid 2760 . . . . . . . . 9 (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))
143129, 142fmptd 6548 . . . . . . . 8 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0)))
144 difss 3880 . . . . . . . . 9 (ℂ ∖ (-∞(,]0)) ⊆ ℂ
1455addcn 22869 . . . . . . . . . . 11 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
146145a1i 11 . . . . . . . . . 10 (𝜑 → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
147 1cnd 10248 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
148 cncfmptc 22915 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
149147, 22, 24, 148syl3anc 1477 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
1505, 146, 29, 149cncfmpt2f 22918 . . . . . . . . 9 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→ℂ))
151 cncffvrn 22902 . . . . . . . . 9 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0))))
152144, 150, 151sylancr 698 . . . . . . . 8 (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0))))
153143, 152mpbird 247 . . . . . . 7 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))))
154153, 132cncfco 22911 . . . . . 6 (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ((0[,]1)–cn→ℂ))
155141, 154eqeltrrd 2840 . . . . 5 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ((0[,]1)–cn→ℂ))
1565, 7, 29, 155cncfmpt2f 22918 . . . 4 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ((0[,]1)–cn→ℂ))
15720a1i 11 . . . . . . . 8 (𝜑 → ℝ ⊆ ℂ)
15819a1i 11 . . . . . . . 8 (𝜑 → (0[,]1) ⊆ ℝ)
159127logdmn0 24585 . . . . . . . . . . 11 ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
160129, 159syl 17 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
16136, 160logcld 24516 . . . . . . . . 9 ((𝜑𝑡 ∈ (0[,]1)) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
16234, 161subcld 10584 . . . . . . . 8 ((𝜑𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ℂ)
1635tgioo2 22807 . . . . . . . 8 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
164 iccntr 22825 . . . . . . . . 9 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
16555, 4, 164sylancr 698 . . . . . . . 8 (𝜑 → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
166157, 158, 162, 163, 5, 165dvmptntr 23933 . . . . . . 7 (𝜑 → (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))))
167 reelprrecn 10220 . . . . . . . . 9 ℝ ∈ {ℝ, ℂ}
168167a1i 11 . . . . . . . 8 (𝜑 → ℝ ∈ {ℝ, ℂ})
16913adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝐴 ∈ ℂ)
17016adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℂ)
17117adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝑁 ≠ 0)
172169, 170, 171divcld 10993 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (𝐴 / 𝑁) ∈ ℂ)
173 ioossicc 12452 . . . . . . . . . . 11 (0(,)1) ⊆ (0[,]1)
174173sseli 3740 . . . . . . . . . 10 (𝑡 ∈ (0(,)1) → 𝑡 ∈ (0[,]1))
175174, 33sylan2 492 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
176172, 175mulcld 10252 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
17713adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ) → 𝐴 ∈ ℂ)
17816adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ) → 𝑁 ∈ ℂ)
17917adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ) → 𝑁 ≠ 0)
180177, 178, 179divcld 10993 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (𝐴 / 𝑁) ∈ ℂ)
181157sselda 3744 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
182180, 181mulcld 10252 . . . . . . . . 9 ((𝜑𝑡 ∈ ℝ) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
183 1cnd 10248 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ) → 1 ∈ ℂ)
184168dvmptid 23919 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
185168, 181, 183, 184, 18dvmptcmul 23926 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 1)))
18618mulid1d 10249 . . . . . . . . . . 11 (𝜑 → ((𝐴 / 𝑁) · 1) = (𝐴 / 𝑁))
187186mpteq2dv 4897 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 1)) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
188185, 187eqtrd 2794 . . . . . . . . 9 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
189173, 158syl5ss 3755 . . . . . . . . 9 (𝜑 → (0(,)1) ⊆ ℝ)
190 retop 22766 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
191 iooretop 22770 . . . . . . . . . . 11 (0(,)1) ∈ (topGen‘ran (,))
192 isopn3i 21088 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (0(,)1) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1))
193190, 191, 192mp2an 710 . . . . . . . . . 10 ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1)
194193a1i 11 . . . . . . . . 9 (𝜑 → ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1))
195168, 182, 180, 188, 189, 163, 5, 194dvmptres2 23924 . . . . . . . 8 (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝐴 / 𝑁)))
196174, 161sylan2 492 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
197 1cnd 10248 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → 1 ∈ ℂ)
198176, 197addcld 10251 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
199174, 160sylan2 492 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
200198, 199reccld 10986 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
201200, 172mulcld 10252 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)) ∈ ℂ)
202 cnelprrecn 10221 . . . . . . . . . 10 ℂ ∈ {ℝ, ℂ}
203202a1i 11 . . . . . . . . 9 (𝜑 → ℂ ∈ {ℝ, ℂ})
204174, 129sylan2 492 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)))
205 eldifi 3875 . . . . . . . . . . 11 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
206205adantl 473 . . . . . . . . . 10 ((𝜑𝑦 ∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ∈ ℂ)
207127logdmn0 24585 . . . . . . . . . . 11 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
208207adantl 473 . . . . . . . . . 10 ((𝜑𝑦 ∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ≠ 0)
209206, 208logcld 24516 . . . . . . . . 9 ((𝜑𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
210206, 208reccld 10986 . . . . . . . . 9 ((𝜑𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ ℂ)
211182, 183addcld 10251 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
212 0cnd 10225 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ℝ) → 0 ∈ ℂ)
213168, 147dvmptc 23920 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 1)) = (𝑡 ∈ ℝ ↦ 0))
214168, 182, 180, 188, 183, 212, 213dvmptadd 23922 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) + 0)))
21518addid1d 10428 . . . . . . . . . . . 12 (𝜑 → ((𝐴 / 𝑁) + 0) = (𝐴 / 𝑁))
216215mpteq2dv 4897 . . . . . . . . . . 11 (𝜑 → (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) + 0)) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
217214, 216eqtrd 2794 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
218168, 211, 180, 217, 189, 163, 5, 194dvmptres2 23924 . . . . . . . . 9 (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0(,)1) ↦ (𝐴 / 𝑁)))
219 fvres 6368 . . . . . . . . . . . . 13 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦) = (log‘𝑦))
220219mpteq2ia 4892 . . . . . . . . . . . 12 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦)) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))
221135, 220syl6req 2811 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)) = (log ↾ (ℂ ∖ (-∞(,]0))))
222221oveq2d 6829 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))))
223127dvlog 24596 . . . . . . . . . 10 (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
224222, 223syl6eq 2810 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
225 fveq2 6352 . . . . . . . . 9 (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → (log‘𝑦) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
226 oveq2 6821 . . . . . . . . 9 (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → (1 / 𝑦) = (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))
227168, 203, 204, 172, 209, 210, 218, 224, 225, 226dvmptco 23934 . . . . . . . 8 (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) = (𝑡 ∈ (0(,)1) ↦ ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
228168, 176, 172, 195, 196, 201, 227dvmptsub 23929 . . . . . . 7 (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
229166, 228eqtrd 2794 . . . . . 6 (𝜑 → (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
230229dmeqd 5481 . . . . 5 (𝜑 → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = dom (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
231 ovex 6841 . . . . . 6 ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) ∈ V
232 eqid 2760 . . . . . 6 (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
233231, 232dmmpti 6184 . . . . 5 dom (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (0(,)1)
234230, 233syl6eq 2810 . . . 4 (𝜑 → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (0(,)1))
235 2re 11282 . . . . . . . . . . 11 2 ∈ ℝ
236235a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ)
237236, 48remulcld 10262 . . . . . . . . 9 (𝜑 → (2 · 𝑅) ∈ ℝ)
2388nnrpd 12063 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℝ+)
23948, 238ltaddrpd 12098 . . . . . . . . . 10 (𝜑𝑅 < (𝑅 + 𝑅))
24048recnd 10260 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
2412402timesd 11467 . . . . . . . . . 10 (𝜑 → (2 · 𝑅) = (𝑅 + 𝑅))
242239, 241breqtrrd 4832 . . . . . . . . 9 (𝜑𝑅 < (2 · 𝑅))
24348, 237, 15, 242, 91ltletrd 10389 . . . . . . . 8 (𝜑𝑅 < 𝑁)
244 difrp 12061 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑅 < 𝑁 ↔ (𝑁𝑅) ∈ ℝ+))
24548, 15, 244syl2anc 696 . . . . . . . 8 (𝜑 → (𝑅 < 𝑁 ↔ (𝑁𝑅) ∈ ℝ+))
246243, 245mpbid 222 . . . . . . 7 (𝜑 → (𝑁𝑅) ∈ ℝ+)
247246rprecred 12076 . . . . . 6 (𝜑 → (1 / (𝑁𝑅)) ∈ ℝ)
24814nnrecred 11258 . . . . . 6 (𝜑 → (1 / 𝑁) ∈ ℝ)
249247, 248resubcld 10650 . . . . 5 (𝜑 → ((1 / (𝑁𝑅)) − (1 / 𝑁)) ∈ ℝ)
25048, 249remulcld 10262 . . . 4 (𝜑 → (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ∈ ℝ)
251229fveq1d 6354 . . . . . . 7 (𝜑 → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦) = ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))
252251fveq2d 6356 . . . . . 6 (𝜑 → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
253252adantr 472 . . . . 5 ((𝜑𝑦 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
254 nfv 1992 . . . . . . 7 𝑡(𝜑𝑦 ∈ (0(,)1))
255 nfcv 2902 . . . . . . . . 9 𝑡abs
256 nffvmpt1 6360 . . . . . . . . 9 𝑡((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)
257255, 256nffv 6359 . . . . . . . 8 𝑡(abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))
258 nfcv 2902 . . . . . . . 8 𝑡
259 nfcv 2902 . . . . . . . 8 𝑡(𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))
260257, 258, 259nfbr 4851 . . . . . . 7 𝑡(abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))
261254, 260nfim 1974 . . . . . 6 𝑡((𝜑𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
262 eleq1w 2822 . . . . . . . 8 (𝑡 = 𝑦 → (𝑡 ∈ (0(,)1) ↔ 𝑦 ∈ (0(,)1)))
263262anbi2d 742 . . . . . . 7 (𝑡 = 𝑦 → ((𝜑𝑡 ∈ (0(,)1)) ↔ (𝜑𝑦 ∈ (0(,)1))))
264 fveq2 6352 . . . . . . . . 9 (𝑡 = 𝑦 → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))
265264fveq2d 6356 . . . . . . . 8 (𝑡 = 𝑦 → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
266265breq1d 4814 . . . . . . 7 (𝑡 = 𝑦 → ((abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ↔ (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))))
267263, 266imbi12d 333 . . . . . 6 (𝑡 = 𝑦 → (((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))) ↔ ((𝜑𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))))
268 simpr 479 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1))
269232fvmpt2 6453 . . . . . . . . . 10 ((𝑡 ∈ (0(,)1) ∧ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
270268, 231, 269sylancl 697 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
271270fveq2d 6356 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (abs‘((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
272172, 197, 200subdid 10678 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (((𝐴 / 𝑁) · 1) − ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
273172mulid1d 10249 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 1) = (𝐴 / 𝑁))
274172, 200mulcomd 10253 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))
275273, 274oveq12d 6831 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 1) − ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
276272, 275eqtr2d 2795 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) = ((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
277276fveq2d 6356 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
278169, 170, 171absdivd 14393 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / (abs‘𝑁)))
27915adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℝ)
28062adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → 0 ≤ 𝑁)
281279, 280absidd 14360 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘𝑁) = 𝑁)
282281oveq2d 6829 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘𝐴) / (abs‘𝑁)) = ((abs‘𝐴) / 𝑁))
283278, 282eqtrd 2794 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / 𝑁))
284283oveq1d 6828 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘(𝐴 / 𝑁)) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = (((abs‘𝐴) / 𝑁) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
285197, 200subcld 10584 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ℂ)
286172, 285absmuld 14392 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = ((abs‘(𝐴 / 𝑁)) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
28766adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘𝐴) ∈ ℝ)
288287recnd 10260 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘𝐴) ∈ ℂ)
289285abscld 14374 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ℝ)
290289recnd 10260 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ℂ)
291288, 290, 170, 171div23d 11030 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) = (((abs‘𝐴) / 𝑁) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
292284, 286, 2913eqtr4d 2804 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁))
293271, 277, 2923eqtrd 2798 . . . . . . 7 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁))
29448adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℝ)
295247adantr 472 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (𝑁𝑅)) ∈ ℝ)
296248adantr 472 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (1 / 𝑁) ∈ ℝ)
297295, 296resubcld 10650 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → ((1 / (𝑁𝑅)) − (1 / 𝑁)) ∈ ℝ)
298279, 297remulcld 10262 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ∈ ℝ)
29913absge0d 14382 . . . . . . . . . . 11 (𝜑 → 0 ≤ (abs‘𝐴))
300299adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘𝐴))
301285absge0d 14382 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
30277adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘𝐴) ≤ 𝑅)
303246adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁𝑅) ∈ ℝ+)
304238adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℝ+)
305303, 304rpdivcld 12082 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) ∈ ℝ+)
30612dmgmn0 24951 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ≠ 0)
307306adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → 𝐴 ≠ 0)
308169, 170, 307, 171divne0d 11009 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (𝐴 / 𝑁) ≠ 0)
309 eliooord 12426 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
310309adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → (0 < 𝑡𝑡 < 1))
311310simpld 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → 0 < 𝑡)
312311gt0ne0d 10784 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → 𝑡 ≠ 0)
313172, 175, 308, 312mulne0d 10871 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 𝑡) ≠ 0)
314176, 313reccld 10986 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
315197, 314addcld 10251 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) ∈ ℂ)
316176, 197, 176, 313divdird 11031 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) = ((((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) + (1 / ((𝐴 / 𝑁) · 𝑡))))
317176, 313dividd 10991 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) = 1)
318317oveq1d 6828 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) + (1 / ((𝐴 / 𝑁) · 𝑡))) = (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))
319316, 318eqtrd 2794 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) = (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))
320198, 176, 199, 313divne0d 11009 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) ≠ 0)
321319, 320eqnetrrd 3000 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) ≠ 0)
322315, 321absrpcld 14386 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) ∈ ℝ+)
323 1red 10247 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → 1 ∈ ℝ)
324 0le1 10743 . . . . . . . . . . . . . 14 0 ≤ 1
325324a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → 0 ≤ 1)
326305rpred 12065 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) ∈ ℝ)
327314negcld 10571 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → -(1 / ((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
328327abscld 14374 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) ∈ ℝ)
329328, 323resubcld 10650 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ∈ ℝ)
330315abscld 14374 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) ∈ ℝ)
331240adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℂ)
332304rpne0d 12070 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → 𝑅 ≠ 0)
333170, 331, 331, 332divsubdird 11032 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) = ((𝑁 / 𝑅) − (𝑅 / 𝑅)))
334331, 332dividd 10991 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 / 𝑅) = 1)
335334oveq2d 6829 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 / 𝑅) − (𝑅 / 𝑅)) = ((𝑁 / 𝑅) − 1))
336333, 335eqtrd 2794 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) = ((𝑁 / 𝑅) − 1))
337279, 304rerpdivcld 12096 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ∈ ℝ)
338331, 170, 332, 171recdivd 11010 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (𝑅 / 𝑁)) = (𝑁 / 𝑅))
339174, 90sylan2 492 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁))
340176, 313absrpcld 14386 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ+)
34161adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℝ+)
342304, 341rpdivcld 12082 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 / 𝑁) ∈ ℝ+)
343340, 342lerecd 12084 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁) ↔ (1 / (𝑅 / 𝑁)) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))))
344339, 343mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (𝑅 / 𝑁)) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
345338, 344eqbrtrrd 4828 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
346314absnegd 14387 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) = (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))))
347197, 176, 313absdivd 14393 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))) = ((abs‘1) / (abs‘((𝐴 / 𝑁) · 𝑡))))
348 abs1 14236 . . . . . . . . . . . . . . . . . . . 20 (abs‘1) = 1
349348oveq1i 6823 . . . . . . . . . . . . . . . . . . 19 ((abs‘1) / (abs‘((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))
350347, 349syl6eq 2810 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
351346, 350eqtrd 2794 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
352345, 351breqtrrd 4832 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ≤ (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))))
353337, 328, 323, 352lesub1dd 10835 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 / 𝑅) − 1) ≤ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1))
354336, 353eqbrtrd 4826 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) ≤ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1))
355348oveq2i 6824 . . . . . . . . . . . . . . . 16 ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − (abs‘1)) = ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1)
356327, 197abs2difd 14395 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − (abs‘1)) ≤ (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
357355, 356syl5eqbrr 4840 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ≤ (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
358197, 314addcomd 10430 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = ((1 / ((𝐴 / 𝑁) · 𝑡)) + 1))
359358negeqd 10467 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → -(1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = -((1 / ((𝐴 / 𝑁) · 𝑡)) + 1))
360314, 197negdi2d 10598 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → -((1 / ((𝐴 / 𝑁) · 𝑡)) + 1) = (-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1))
361359, 360eqtrd 2794 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → -(1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = (-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1))
362361fveq2d 6356 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) = (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
363315absnegd 14387 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) = (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
364362, 363eqtr3d 2796 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)) = (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
365357, 364breqtrd 4830 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ≤ (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
366326, 329, 330, 354, 365letrd 10386 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) ≤ (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
367305, 322, 323, 325, 366lediv2ad 12087 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) ≤ (1 / ((𝑁𝑅) / 𝑅)))
36816, 240subcld 10584 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁𝑅) ∈ ℂ)
369368adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁𝑅) ∈ ℂ)
37048, 243gtned 10364 . . . . . . . . . . . . . . . 16 (𝜑𝑁𝑅)
37116, 240, 370subne0d 10593 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁𝑅) ≠ 0)
372371adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁𝑅) ≠ 0)
373369, 331, 372, 332recdivd 11010 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((𝑁𝑅) / 𝑅)) = (𝑅 / (𝑁𝑅)))
374170, 331nncand 10589 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 − (𝑁𝑅)) = 𝑅)
375374oveq1d 6828 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 − (𝑁𝑅)) / (𝑁𝑅)) = (𝑅 / (𝑁𝑅)))
376170, 369, 369, 372divsubdird 11032 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 − (𝑁𝑅)) / (𝑁𝑅)) = ((𝑁 / (𝑁𝑅)) − ((𝑁𝑅) / (𝑁𝑅))))
377375, 376eqtr3d 2796 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 / (𝑁𝑅)) = ((𝑁 / (𝑁𝑅)) − ((𝑁𝑅) / (𝑁𝑅))))
378369, 372dividd 10991 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / (𝑁𝑅)) = 1)
379378oveq2d 6829 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 / (𝑁𝑅)) − ((𝑁𝑅) / (𝑁𝑅))) = ((𝑁 / (𝑁𝑅)) − 1))
380373, 377, 3793eqtrd 2798 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((𝑁𝑅) / 𝑅)) = ((𝑁 / (𝑁𝑅)) − 1))
381367, 380breqtrd 4830 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) ≤ ((𝑁 / (𝑁𝑅)) − 1))
382198, 197, 198, 199divsubdird 11032 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) − 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = (((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))
383176, 197pncand 10585 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) − 1) = ((𝐴 / 𝑁) · 𝑡))
384383oveq1d 6828 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) − 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
385198, 199dividd 10991 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = 1)
386385oveq1d 6828 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))
387382, 384, 3863eqtr3rd 2803 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
388198, 176, 199, 313recdivd 11010 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡))) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
389319oveq2d 6829 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡))) = (1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
390387, 388, 3893eqtr2d 2800 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
391390fveq2d 6356 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
392197, 315, 321absdivd 14393 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = ((abs‘1) / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
393348oveq1i 6823 . . . . . . . . . . . . 13 ((abs‘1) / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
394392, 393syl6eq 2810 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
395391, 394eqtrd 2794 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
396368, 371reccld 10986 . . . . . . . . . . . . . 14 (𝜑 → (1 / (𝑁𝑅)) ∈ ℂ)
397396adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (𝑁𝑅)) ∈ ℂ)
398248recnd 10260 . . . . . . . . . . . . . 14 (𝜑 → (1 / 𝑁) ∈ ℂ)
399398adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (1 / 𝑁) ∈ ℂ)
400170, 397, 399subdid 10678 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) = ((𝑁 · (1 / (𝑁𝑅))) − (𝑁 · (1 / 𝑁))))
401170, 369, 372divrecd 10996 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 / (𝑁𝑅)) = (𝑁 · (1 / (𝑁𝑅))))
402401eqcomd 2766 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · (1 / (𝑁𝑅))) = (𝑁 / (𝑁𝑅)))
403170, 171recidd 10988 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · (1 / 𝑁)) = 1)
404402, 403oveq12d 6831 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 · (1 / (𝑁𝑅))) − (𝑁 · (1 / 𝑁))) = ((𝑁 / (𝑁𝑅)) − 1))
405400, 404eqtrd 2794 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) = ((𝑁 / (𝑁𝑅)) − 1))
406381, 395, 4053brtr4d 4836 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ≤ (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
407287, 294, 289, 298, 300, 301, 302, 406lemul12ad 11158 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑅 · (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))))
408249recnd 10260 . . . . . . . . . . 11 (𝜑 → ((1 / (𝑁𝑅)) − (1 / 𝑁)) ∈ ℂ)
409408adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → ((1 / (𝑁𝑅)) − (1 / 𝑁)) ∈ ℂ)
410331, 170, 409mul12d 10437 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 · (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))) = (𝑁 · (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))))
411407, 410breqtrd 4830 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑁 · (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))))
412287, 289remulcld 10262 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ∈ ℝ)
413250adantr 472 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ∈ ℝ)
414412, 413, 341ledivmuld 12118 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → ((((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ↔ ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑁 · (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))))
415411, 414mpbird 247 . . . . . . 7 ((𝜑𝑡 ∈ (0(,)1)) → (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
416293, 415eqbrtrd 4826 . . . . . 6 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
417261, 267, 416chvar 2407 . . . . 5 ((𝜑𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
418253, 417eqbrtrd 4826 . . . 4 ((𝜑𝑦 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
4193, 4, 156, 234, 250, 418dvlip 23955 . . 3 ((𝜑 ∧ (1 ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) ≤ ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
4201, 2, 419mpanr12 723 . 2 (𝜑 → (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) ≤ ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
421 eqidd 2761 . . . . . 6 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))
422 oveq2 6821 . . . . . . . 8 (𝑡 = 1 → ((𝐴 / 𝑁) · 𝑡) = ((𝐴 / 𝑁) · 1))
423422, 186sylan9eqr 2816 . . . . . . 7 ((𝜑𝑡 = 1) → ((𝐴 / 𝑁) · 𝑡) = (𝐴 / 𝑁))
424423oveq1d 6828 . . . . . . . 8 ((𝜑𝑡 = 1) → (((𝐴 / 𝑁) · 𝑡) + 1) = ((𝐴 / 𝑁) + 1))
425424fveq2d 6356 . . . . . . 7 ((𝜑𝑡 = 1) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘((𝐴 / 𝑁) + 1)))
426423, 425oveq12d 6831 . . . . . 6 ((𝜑𝑡 = 1) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
4271a1i 11 . . . . . 6 (𝜑 → 1 ∈ (0[,]1))
428 ovexd 6843 . . . . . 6 (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ V)
429421, 426, 427, 428fvmptd 6450 . . . . 5 (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
430 oveq2 6821 . . . . . . . . 9 (𝑡 = 0 → ((𝐴 / 𝑁) · 𝑡) = ((𝐴 / 𝑁) · 0))
43118mul01d 10427 . . . . . . . . 9 (𝜑 → ((𝐴 / 𝑁) · 0) = 0)
432430, 431sylan9eqr 2816 . . . . . . . 8 ((𝜑𝑡 = 0) → ((𝐴 / 𝑁) · 𝑡) = 0)
433432oveq1d 6828 . . . . . . . . . . 11 ((𝜑𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) + 1) = (0 + 1))
434 0p1e1 11324 . . . . . . . . . . 11 (0 + 1) = 1
435433, 434syl6eq 2810 . . . . . . . . . 10 ((𝜑𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) + 1) = 1)
436435fveq2d 6356 . . . . . . . . 9 ((𝜑𝑡 = 0) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘1))
437 log1 24531 . . . . . . . . 9 (log‘1) = 0
438436, 437syl6eq 2810 . . . . . . . 8 ((𝜑𝑡 = 0) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = 0)
439432, 438oveq12d 6831 . . . . . . 7 ((𝜑𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = (0 − 0))
440 0m0e0 11322 . . . . . . 7 (0 − 0) = 0
441439, 440syl6eq 2810 . . . . . 6 ((𝜑𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = 0)
4422a1i 11 . . . . . 6 (𝜑 → 0 ∈ (0[,]1))
443421, 441, 442, 442fvmptd 6450 . . . . 5 (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0) = 0)
444429, 443oveq12d 6831 . . . 4 (𝜑 → (((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0)) = (((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) − 0))
44518, 147addcld 10251 . . . . . . 7 (𝜑 → ((𝐴 / 𝑁) + 1) ∈ ℂ)
44612, 14dmgmdivn0 24953 . . . . . . 7 (𝜑 → ((𝐴 / 𝑁) + 1) ≠ 0)
447445, 446logcld 24516 . . . . . 6 (𝜑 → (log‘((𝐴 / 𝑁) + 1)) ∈ ℂ)
44818, 447subcld 10584 . . . . 5 (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ ℂ)
449448subid1d 10573 . . . 4 (𝜑 → (((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) − 0) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
450444, 449eqtr2d 2795 . . 3 (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) = (((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0)))
451450fveq2d 6356 . 2 (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) = (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))))
452 1m0e1 11323 . . . . . 6 (1 − 0) = 1
453452fveq2i 6355 . . . . 5 (abs‘(1 − 0)) = (abs‘1)
454453, 348eqtri 2782 . . . 4 (abs‘(1 − 0)) = 1
455454oveq2i 6824 . . 3 ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))) = ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · 1)
456240, 408mulcld 10252 . . . 4 (𝜑 → (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ∈ ℂ)
457456mulid1d 10249 . . 3 (𝜑 → ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · 1) = (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
458455, 457syl5req 2807 . 2 (𝜑 → (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) = ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
459420, 451, 4583brtr4d 4836 1 (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  wne 2932  wral 3050  {crab 3054  Vcvv 3340  cdif 3712  wss 3715  {cpr 4323   class class class wbr 4804  cmpt 4881  dom cdm 5266  ran crn 5267  cres 5268  ccom 5270  wf 6045  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133  -∞cmnf 10264   < clt 10266  cle 10267  cmin 10458  -cneg 10459   / cdiv 10876  cn 11212  2c2 11262  0cn0 11484  cz 11569  +crp 12025  (,)cioo 12368  (,]cioc 12369  [,]cicc 12371  cre 14036  abscabs 14173  TopOpenctopn 16284  topGenctg 16300  fldccnfld 19948  Topctop 20900  intcnt 21023   Cn ccn 21230   ×t ctx 21565  cnccncf 22880   D cdv 23826  logclog 24500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ioc 12373  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-shft 14006  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-limsup 14401  df-clim 14418  df-rlim 14419  df-sum 14616  df-ef 14997  df-sin 14999  df-cos 15000  df-tan 15001  df-pi 15002  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-rest 16285  df-topn 16286  df-0g 16304  df-gsum 16305  df-topgen 16306  df-pt 16307  df-prds 16310  df-xrs 16364  df-qtop 16369  df-imas 16370  df-xps 16372  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20901  df-topon 20918  df-topsp 20939  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-nei 21104  df-lp 21142  df-perf 21143  df-cn 21233  df-cnp 21234  df-haus 21321  df-cmp 21392  df-tx 21567  df-hmeo 21760  df-fil 21851  df-fm 21943  df-flim 21944  df-flf 21945  df-xms 22326  df-ms 22327  df-tms 22328  df-cncf 22882  df-limc 23829  df-dv 23830  df-log 24502
This theorem is referenced by:  lgamgulmlem3  24956
  Copyright terms: Public domain W3C validator