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

Theorem lgamgulmlem2 24970
Description: Lemma for lgamgulm 24975. (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 12512 . . 3 1 ∈ (0[,]1)
2 0elunit 12511 . . 3 0 ∈ (0[,]1)
3 0red 10328 . . . 4 (𝜑 → 0 ∈ ℝ)
4 1red 10326 . . . 4 (𝜑 → 1 ∈ ℝ)
5 eqid 2806 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
65subcn 22882 . . . . . 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 24969 . . . . . . . . . 10 (𝜑𝑈 ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
11 lgamgulm.a . . . . . . . . . 10 (𝜑𝐴𝑈)
1210, 11sseldd 3799 . . . . . . . . 9 (𝜑𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
1312eldifad 3781 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
14 lgamgulm.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
1514nnred 11320 . . . . . . . . 9 (𝜑𝑁 ∈ ℝ)
1615recnd 10353 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
1714nnne0d 11351 . . . . . . . 8 (𝜑𝑁 ≠ 0)
1813, 16, 17divcld 11086 . . . . . . 7 (𝜑 → (𝐴 / 𝑁) ∈ ℂ)
19 unitssre 12542 . . . . . . . . 9 (0[,]1) ⊆ ℝ
20 ax-resscn 10278 . . . . . . . . 9 ℝ ⊆ ℂ
2119, 20sstri 3807 . . . . . . . 8 (0[,]1) ⊆ ℂ
2221a1i 11 . . . . . . 7 (𝜑 → (0[,]1) ⊆ ℂ)
23 ssidd 3821 . . . . . . 7 (𝜑 → ℂ ⊆ ℂ)
24 cncfmptc 22927 . . . . . . 7 (((𝐴 / 𝑁) ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ (𝐴 / 𝑁)) ∈ ((0[,]1)–cn→ℂ))
2518, 22, 23, 24syl3anc 1483 . . . . . 6 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (𝐴 / 𝑁)) ∈ ((0[,]1)–cn→ℂ))
26 cncfmptid 22928 . . . . . . 7 (((0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
2721, 23, 26sylancr 577 . . . . . 6 (𝜑 → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
2825, 27mulcncf 23427 . . . . 5 (𝜑 → (𝑡 ∈ (0[,]1) ↦ ((𝐴 / 𝑁) · 𝑡)) ∈ ((0[,]1)–cn→ℂ))
2918adantr 468 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0[,]1)) → (𝐴 / 𝑁) ∈ ℂ)
30 simpr 473 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
3119, 30sseldi 3796 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℝ)
3231recnd 10353 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ)
3329, 32mulcld 10345 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0[,]1)) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
34 1cnd 10320 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0[,]1)) → 1 ∈ ℂ)
3533, 34addcld 10344 . . . . . . . . 9 ((𝜑𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
36 rere 14085 . . . . . . . . . . . 12 ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) + 1))
3736adantl 469 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) + 1))
3835recld 14157 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ)
3933recld 14157 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ)
4039recnd 10353 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
4140abscld 14398 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ∈ ℝ)
4233abscld 14398 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ)
43 1red 10326 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → 1 ∈ ℝ)
44 absrele 14271 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 / 𝑁) · 𝑡) ∈ ℂ → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ≤ (abs‘((𝐴 / 𝑁) · 𝑡)))
4533, 44syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ≤ (abs‘((𝐴 / 𝑁) · 𝑡)))
4643rehalfcld 11546 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0[,]1)) → (1 / 2) ∈ ℝ)
478nnred 11320 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ∈ ℝ)
4847adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ)
4914adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → 𝑁 ∈ ℕ)
5048, 49nndivred 11355 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ∈ ℝ)
5118abscld 14398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (abs‘(𝐴 / 𝑁)) ∈ ℝ)
5251adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(𝐴 / 𝑁)) ∈ ℝ)
5329absge0d 14406 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → 0 ≤ (abs‘(𝐴 / 𝑁)))
54 elicc01 12510 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
5554simp2bi 1169 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ (0[,]1) → 0 ≤ 𝑡)
5655adantl 469 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → 0 ≤ 𝑡)
5713, 16, 17absdivd 14417 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / (abs‘𝑁)))
5814nnrpd 12084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℝ+)
5958rpge0d 12090 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 ≤ 𝑁)
6015, 59absidd 14384 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (abs‘𝑁) = 𝑁)
6160oveq2d 6890 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((abs‘𝐴) / (abs‘𝑁)) = ((abs‘𝐴) / 𝑁))
6257, 61eqtr2d 2841 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((abs‘𝐴) / 𝑁) = (abs‘(𝐴 / 𝑁)))
6313abscld 14398 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (abs‘𝐴) ∈ ℝ)
64 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = 𝐴 → (abs‘𝑥) = (abs‘𝐴))
6564breq1d 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = 𝐴 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝐴) ≤ 𝑅))
66 fvoveq1 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = 𝐴 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝐴 + 𝑘)))
6766breq2d 4856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = 𝐴 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
6867ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = 𝐴 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
6965, 68anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = 𝐴 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))))
7069, 9elrab2 3562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴𝑈 ↔ (𝐴 ∈ ℂ ∧ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))))
7170simprbi 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴𝑈 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
7211, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
7372simpld 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (abs‘𝐴) ≤ 𝑅)
7463, 47, 58, 73lediv1dd 12144 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((abs‘𝐴) / 𝑁) ≤ (𝑅 / 𝑁))
7562, 74eqbrtrrd 4868 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (abs‘(𝐴 / 𝑁)) ≤ (𝑅 / 𝑁))
7675adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(𝐴 / 𝑁)) ≤ (𝑅 / 𝑁))
7754simp3bi 1170 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ (0[,]1) → 𝑡 ≤ 1)
7877adantl 469 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → 𝑡 ≤ 1)
7952, 50, 31, 43, 53, 56, 76, 78lemul12ad 11251 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · 𝑡) ≤ ((𝑅 / 𝑁) · 1))
8029, 32absmuld 14416 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) = ((abs‘(𝐴 / 𝑁)) · (abs‘𝑡)))
8131, 56absidd 14384 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘𝑡) = 𝑡)
8281oveq2d 6890 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · (abs‘𝑡)) = ((abs‘(𝐴 / 𝑁)) · 𝑡))
8380, 82eqtr2d 2841 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · 𝑡) = (abs‘((𝐴 / 𝑁) · 𝑡)))
8450recnd 10353 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ∈ ℂ)
8584mulid1d 10342 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ (0[,]1)) → ((𝑅 / 𝑁) · 1) = (𝑅 / 𝑁))
8679, 83, 853brtr3d 4875 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁))
87 lgamgulm.l . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (2 · 𝑅) ≤ 𝑁)
88 2rp 12051 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ+
8988a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 2 ∈ ℝ+)
9047, 15, 89lemuldiv2d 12136 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((2 · 𝑅) ≤ 𝑁𝑅 ≤ (𝑁 / 2)))
9187, 90mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ≤ (𝑁 / 2))
92 2cnd 11377 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 2 ∈ ℂ)
93 2ne0 11396 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ≠ 0
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 2 ≠ 0)
9516, 92, 94divrecd 11089 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
9691, 95breqtrd 4870 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ≤ (𝑁 · (1 / 2)))
974rehalfcld 11546 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1 / 2) ∈ ℝ)
9847, 97, 58ledivmuld 12139 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑅 / 𝑁) ≤ (1 / 2) ↔ 𝑅 ≤ (𝑁 · (1 / 2))))
9996, 98mpbird 248 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑅 / 𝑁) ≤ (1 / 2))
10099adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ≤ (1 / 2))
10142, 50, 46, 86, 100letrd 10479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (1 / 2))
102 halflt1 11517 . . . . . . . . . . . . . . . . . . . . 21 (1 / 2) < 1
103102a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0[,]1)) → (1 / 2) < 1)
10442, 46, 43, 101, 103lelttrd 10480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) < 1)
10541, 42, 43, 45, 104lelttrd 10480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) < 1)
10639, 43absltd 14391 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0[,]1)) → ((abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) < 1 ↔ (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∧ (ℜ‘((𝐴 / 𝑁) · 𝑡)) < 1)))
107105, 106mpbid 223 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0[,]1)) → (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∧ (ℜ‘((𝐴 / 𝑁) · 𝑡)) < 1))
108107simpld 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0[,]1)) → -1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)))
10943renegcld 10742 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0[,]1)) → -1 ∈ ℝ)
110109, 39posdifd 10899 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0[,]1)) → (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ↔ 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1)))
111108, 110mpbid 223 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0[,]1)) → 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1))
11240, 34subnegd 10684 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0[,]1)) → ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
113111, 112breqtrd 4870 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0[,]1)) → 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
11433, 34readdd 14177 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + (ℜ‘1)))
115 re1 14117 . . . . . . . . . . . . . . . 16 (ℜ‘1) = 1
116115oveq2i 6885 . . . . . . . . . . . . . . 15 ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + (ℜ‘1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1)
117114, 116syl6eq 2856 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
118113, 117breqtrrd 4872 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0[,]1)) → 0 < (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)))
11938, 118elrpd 12083 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ+)
120119adantr 468 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ+)
12137, 120eqeltrrd 2886 . . . . . . . . . 10 (((𝜑𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ+)
122121ex 399 . . . . . . . . 9 ((𝜑𝑡 ∈ (0[,]1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ+))
123 eqid 2806 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
124123ellogdm 24599 . . . . . . . . 9 ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) ↔ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ ∧ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ+)))
12535, 122, 124sylanbrc 574 . . . . . . . 8 ((𝜑𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)))
126 eqidd 2807 . . . . . . . 8 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)))
127123logcn 24607 . . . . . . . . . . 11 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
128127a1i 11 . . . . . . . . . 10 (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
129 cncff 22909 . . . . . . . . . 10 ((log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ) → (log ↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖ (-∞(,]0))⟶ℂ)
130128, 129syl 17 . . . . . . . . 9 (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖ (-∞(,]0))⟶ℂ)
131130feqmptd 6470 . . . . . . . 8 (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦)))
132 fveq2 6408 . . . . . . . 8 (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦) = ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)))
133125, 126, 131, 132fmptco 6619 . . . . . . 7 (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1))))
134 fvres 6427 . . . . . . . . 9 ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
135125, 134syl 17 . . . . . . . 8 ((𝜑𝑡 ∈ (0[,]1)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
136135mpteq2dva 4938 . . . . . . 7 (𝜑 → (𝑡 ∈ (0[,]1) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))
137133, 136eqtrd 2840 . . . . . 6 (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))
138125fmpttd 6607 . . . . . . . 8 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0)))
139 difss 3936 . . . . . . . . 9 (ℂ ∖ (-∞(,]0)) ⊆ ℂ
1405addcn 22881 . . . . . . . . . . 11 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
141140a1i 11 . . . . . . . . . 10 (𝜑 → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
142 1cnd 10320 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
143 cncfmptc 22927 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
144142, 22, 23, 143syl3anc 1483 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
1455, 141, 28, 144cncfmpt2f 22930 . . . . . . . . 9 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→ℂ))
146 cncffvrn 22914 . . . . . . . . 9 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0))))
147139, 145, 146sylancr 577 . . . . . . . 8 (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0))))
148138, 147mpbird 248 . . . . . . 7 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))))
149148, 128cncfco 22923 . . . . . 6 (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ((0[,]1)–cn→ℂ))
150137, 149eqeltrrd 2886 . . . . 5 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ((0[,]1)–cn→ℂ))
1515, 7, 28, 150cncfmpt2f 22930 . . . 4 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ((0[,]1)–cn→ℂ))
15220a1i 11 . . . . . . . 8 (𝜑 → ℝ ⊆ ℂ)
15319a1i 11 . . . . . . . 8 (𝜑 → (0[,]1) ⊆ ℝ)
154123logdmn0 24600 . . . . . . . . . . 11 ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
155125, 154syl 17 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
15635, 155logcld 24531 . . . . . . . . 9 ((𝜑𝑡 ∈ (0[,]1)) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
15733, 156subcld 10677 . . . . . . . 8 ((𝜑𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ℂ)
1585tgioo2 22819 . . . . . . . 8 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
159 0re 10327 . . . . . . . . 9 0 ∈ ℝ
160 iccntr 22837 . . . . . . . . 9 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
161159, 4, 160sylancr 577 . . . . . . . 8 (𝜑 → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
162152, 153, 157, 158, 5, 161dvmptntr 23948 . . . . . . 7 (𝜑 → (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))))
163 reelprrecn 10313 . . . . . . . . 9 ℝ ∈ {ℝ, ℂ}
164163a1i 11 . . . . . . . 8 (𝜑 → ℝ ∈ {ℝ, ℂ})
16513adantr 468 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝐴 ∈ ℂ)
16616adantr 468 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℂ)
16717adantr 468 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝑁 ≠ 0)
168165, 166, 167divcld 11086 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (𝐴 / 𝑁) ∈ ℂ)
169 ioossicc 12477 . . . . . . . . . . 11 (0(,)1) ⊆ (0[,]1)
170169sseli 3794 . . . . . . . . . 10 (𝑡 ∈ (0(,)1) → 𝑡 ∈ (0[,]1))
171170, 32sylan2 582 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
172168, 171mulcld 10345 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
17313adantr 468 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ) → 𝐴 ∈ ℂ)
17416adantr 468 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ) → 𝑁 ∈ ℂ)
17517adantr 468 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ) → 𝑁 ≠ 0)
176173, 174, 175divcld 11086 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (𝐴 / 𝑁) ∈ ℂ)
177152sselda 3798 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
178176, 177mulcld 10345 . . . . . . . . 9 ((𝜑𝑡 ∈ ℝ) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
179 1cnd 10320 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ) → 1 ∈ ℂ)
180164dvmptid 23934 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
181164, 177, 179, 180, 18dvmptcmul 23941 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 1)))
18218mulid1d 10342 . . . . . . . . . . 11 (𝜑 → ((𝐴 / 𝑁) · 1) = (𝐴 / 𝑁))
183182mpteq2dv 4939 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 1)) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
184181, 183eqtrd 2840 . . . . . . . . 9 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
185169, 153syl5ss 3809 . . . . . . . . 9 (𝜑 → (0(,)1) ⊆ ℝ)
186 retop 22778 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
187 iooretop 22782 . . . . . . . . . . 11 (0(,)1) ∈ (topGen‘ran (,))
188 isopn3i 21100 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (0(,)1) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1))
189186, 187, 188mp2an 675 . . . . . . . . . 10 ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1)
190189a1i 11 . . . . . . . . 9 (𝜑 → ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1))
191164, 178, 176, 184, 185, 158, 5, 190dvmptres2 23939 . . . . . . . 8 (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝐴 / 𝑁)))
192170, 156sylan2 582 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
193 1cnd 10320 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → 1 ∈ ℂ)
194172, 193addcld 10344 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
195170, 155sylan2 582 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
196194, 195reccld 11079 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
197196, 168mulcld 10345 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)) ∈ ℂ)
198 cnelprrecn 10314 . . . . . . . . . 10 ℂ ∈ {ℝ, ℂ}
199198a1i 11 . . . . . . . . 9 (𝜑 → ℂ ∈ {ℝ, ℂ})
200170, 125sylan2 582 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)))
201 eldifi 3931 . . . . . . . . . . 11 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
202201adantl 469 . . . . . . . . . 10 ((𝜑𝑦 ∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ∈ ℂ)
203123logdmn0 24600 . . . . . . . . . . 11 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
204203adantl 469 . . . . . . . . . 10 ((𝜑𝑦 ∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ≠ 0)
205202, 204logcld 24531 . . . . . . . . 9 ((𝜑𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
206202, 204reccld 11079 . . . . . . . . 9 ((𝜑𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ ℂ)
207178, 179addcld 10344 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
208 0cnd 10318 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ℝ) → 0 ∈ ℂ)
209164, 142dvmptc 23935 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 1)) = (𝑡 ∈ ℝ ↦ 0))
210164, 178, 176, 184, 179, 208, 209dvmptadd 23937 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) + 0)))
21118addid1d 10521 . . . . . . . . . . . 12 (𝜑 → ((𝐴 / 𝑁) + 0) = (𝐴 / 𝑁))
212211mpteq2dv 4939 . . . . . . . . . . 11 (𝜑 → (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) + 0)) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
213210, 212eqtrd 2840 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
214164, 207, 176, 213, 185, 158, 5, 190dvmptres2 23939 . . . . . . . . 9 (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0(,)1) ↦ (𝐴 / 𝑁)))
215 fvres 6427 . . . . . . . . . . . . 13 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦) = (log‘𝑦))
216215mpteq2ia 4934 . . . . . . . . . . . 12 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦)) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))
217131, 216syl6req 2857 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)) = (log ↾ (ℂ ∖ (-∞(,]0))))
218217oveq2d 6890 . . . . . . . . . 10 (𝜑 → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))))
219123dvlog 24611 . . . . . . . . . 10 (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
220218, 219syl6eq 2856 . . . . . . . . 9 (𝜑 → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
221 fveq2 6408 . . . . . . . . 9 (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → (log‘𝑦) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
222 oveq2 6882 . . . . . . . . 9 (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → (1 / 𝑦) = (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))
223164, 199, 200, 168, 205, 206, 214, 220, 221, 222dvmptco 23949 . . . . . . . 8 (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) = (𝑡 ∈ (0(,)1) ↦ ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
224164, 172, 168, 191, 192, 197, 223dvmptsub 23944 . . . . . . 7 (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
225162, 224eqtrd 2840 . . . . . 6 (𝜑 → (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
226225dmeqd 5527 . . . . 5 (𝜑 → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = dom (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
227 ovex 6906 . . . . . 6 ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) ∈ V
228 eqid 2806 . . . . . 6 (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
229227, 228dmmpti 6234 . . . . 5 dom (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (0(,)1)
230226, 229syl6eq 2856 . . . 4 (𝜑 → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (0(,)1))
231 2re 11374 . . . . . . . . . . 11 2 ∈ ℝ
232231a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ)
233232, 47remulcld 10355 . . . . . . . . 9 (𝜑 → (2 · 𝑅) ∈ ℝ)
2348nnrpd 12084 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℝ+)
23547, 234ltaddrpd 12119 . . . . . . . . . 10 (𝜑𝑅 < (𝑅 + 𝑅))
23647recnd 10353 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
2372362timesd 11542 . . . . . . . . . 10 (𝜑 → (2 · 𝑅) = (𝑅 + 𝑅))
238235, 237breqtrrd 4872 . . . . . . . . 9 (𝜑𝑅 < (2 · 𝑅))
23947, 233, 15, 238, 87ltletrd 10482 . . . . . . . 8 (𝜑𝑅 < 𝑁)
240 difrp 12082 . . . . . . . . 9 ((𝑅 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑅 < 𝑁 ↔ (𝑁𝑅) ∈ ℝ+))
24147, 15, 240syl2anc 575 . . . . . . . 8 (𝜑 → (𝑅 < 𝑁 ↔ (𝑁𝑅) ∈ ℝ+))
242239, 241mpbid 223 . . . . . . 7 (𝜑 → (𝑁𝑅) ∈ ℝ+)
243242rprecred 12097 . . . . . 6 (𝜑 → (1 / (𝑁𝑅)) ∈ ℝ)
24414nnrecred 11352 . . . . . 6 (𝜑 → (1 / 𝑁) ∈ ℝ)
245243, 244resubcld 10743 . . . . 5 (𝜑 → ((1 / (𝑁𝑅)) − (1 / 𝑁)) ∈ ℝ)
24647, 245remulcld 10355 . . . 4 (𝜑 → (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ∈ ℝ)
247225fveq1d 6410 . . . . . . 7 (𝜑 → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦) = ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))
248247fveq2d 6412 . . . . . 6 (𝜑 → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
249248adantr 468 . . . . 5 ((𝜑𝑦 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
250 nfv 2005 . . . . . . 7 𝑡(𝜑𝑦 ∈ (0(,)1))
251 nfcv 2948 . . . . . . . . 9 𝑡abs
252 nffvmpt1 6419 . . . . . . . . 9 𝑡((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)
253251, 252nffv 6418 . . . . . . . 8 𝑡(abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))
254 nfcv 2948 . . . . . . . 8 𝑡
255 nfcv 2948 . . . . . . . 8 𝑡(𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))
256253, 254, 255nfbr 4891 . . . . . . 7 𝑡(abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))
257250, 256nfim 1987 . . . . . 6 𝑡((𝜑𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
258 eleq1w 2868 . . . . . . . 8 (𝑡 = 𝑦 → (𝑡 ∈ (0(,)1) ↔ 𝑦 ∈ (0(,)1)))
259258anbi2d 616 . . . . . . 7 (𝑡 = 𝑦 → ((𝜑𝑡 ∈ (0(,)1)) ↔ (𝜑𝑦 ∈ (0(,)1))))
260 2fveq3 6413 . . . . . . . 8 (𝑡 = 𝑦 → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
261260breq1d 4854 . . . . . . 7 (𝑡 = 𝑦 → ((abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ↔ (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))))
262259, 261imbi12d 335 . . . . . 6 (𝑡 = 𝑦 → (((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))) ↔ ((𝜑𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))))
263 simpr 473 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1))
264228fvmpt2 6512 . . . . . . . . . 10 ((𝑡 ∈ (0(,)1) ∧ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
265263, 227, 264sylancl 576 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
266265fveq2d 6412 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (abs‘((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
267168, 193, 196subdid 10771 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (((𝐴 / 𝑁) · 1) − ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
268168mulid1d 10342 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 1) = (𝐴 / 𝑁))
269168, 196mulcomd 10346 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))
270268, 269oveq12d 6892 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 1) − ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
271267, 270eqtr2d 2841 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) = ((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
272271fveq2d 6412 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
273165, 166, 167absdivd 14417 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / (abs‘𝑁)))
27415adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℝ)
27559adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → 0 ≤ 𝑁)
276274, 275absidd 14384 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘𝑁) = 𝑁)
277276oveq2d 6890 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘𝐴) / (abs‘𝑁)) = ((abs‘𝐴) / 𝑁))
278273, 277eqtrd 2840 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / 𝑁))
279278oveq1d 6889 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘(𝐴 / 𝑁)) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = (((abs‘𝐴) / 𝑁) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
280193, 196subcld 10677 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ℂ)
281168, 280absmuld 14416 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = ((abs‘(𝐴 / 𝑁)) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
28263adantr 468 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘𝐴) ∈ ℝ)
283282recnd 10353 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘𝐴) ∈ ℂ)
284280abscld 14398 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ℝ)
285284recnd 10353 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ℂ)
286283, 285, 166, 167div23d 11123 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) = (((abs‘𝐴) / 𝑁) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
287279, 281, 2863eqtr4d 2850 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁))
288266, 272, 2873eqtrd 2844 . . . . . . 7 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁))
28947adantr 468 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℝ)
290243adantr 468 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (𝑁𝑅)) ∈ ℝ)
291244adantr 468 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (1 / 𝑁) ∈ ℝ)
292290, 291resubcld 10743 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → ((1 / (𝑁𝑅)) − (1 / 𝑁)) ∈ ℝ)
293274, 292remulcld 10355 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ∈ ℝ)
29413absge0d 14406 . . . . . . . . . . 11 (𝜑 → 0 ≤ (abs‘𝐴))
295294adantr 468 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘𝐴))
296280absge0d 14406 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
29773adantr 468 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘𝐴) ≤ 𝑅)
298242adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁𝑅) ∈ ℝ+)
299234adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℝ+)
300298, 299rpdivcld 12103 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) ∈ ℝ+)
30112dmgmn0 24966 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ≠ 0)
302301adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → 𝐴 ≠ 0)
303165, 166, 302, 167divne0d 11102 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (𝐴 / 𝑁) ≠ 0)
304 eliooord 12451 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
305304adantl 469 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → (0 < 𝑡𝑡 < 1))
306305simpld 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → 0 < 𝑡)
307306gt0ne0d 10877 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → 𝑡 ≠ 0)
308168, 171, 303, 307mulne0d 10964 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 𝑡) ≠ 0)
309172, 308reccld 11079 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
310193, 309addcld 10344 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) ∈ ℂ)
311172, 193, 172, 308divdird 11124 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) = ((((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) + (1 / ((𝐴 / 𝑁) · 𝑡))))
312172, 308dividd 11084 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) = 1)
313312oveq1d 6889 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) + (1 / ((𝐴 / 𝑁) · 𝑡))) = (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))
314311, 313eqtrd 2840 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) = (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))
315194, 172, 195, 308divne0d 11102 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) ≠ 0)
316314, 315eqnetrrd 3046 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) ≠ 0)
317310, 316absrpcld 14410 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) ∈ ℝ+)
318 1red 10326 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → 1 ∈ ℝ)
319 0le1 10836 . . . . . . . . . . . . . 14 0 ≤ 1
320319a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → 0 ≤ 1)
321300rpred 12086 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) ∈ ℝ)
322309negcld 10664 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → -(1 / ((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
323322abscld 14398 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) ∈ ℝ)
324323, 318resubcld 10743 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ∈ ℝ)
325310abscld 14398 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) ∈ ℝ)
326236adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℂ)
327299rpne0d 12091 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → 𝑅 ≠ 0)
328166, 326, 326, 327divsubdird 11125 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) = ((𝑁 / 𝑅) − (𝑅 / 𝑅)))
329326, 327dividd 11084 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 / 𝑅) = 1)
330329oveq2d 6890 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 / 𝑅) − (𝑅 / 𝑅)) = ((𝑁 / 𝑅) − 1))
331328, 330eqtrd 2840 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) = ((𝑁 / 𝑅) − 1))
332274, 299rerpdivcld 12117 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ∈ ℝ)
333326, 166, 327, 167recdivd 11103 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (𝑅 / 𝑁)) = (𝑁 / 𝑅))
334170, 86sylan2 582 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁))
335172, 308absrpcld 14410 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ+)
33658adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℝ+)
337299, 336rpdivcld 12103 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 / 𝑁) ∈ ℝ+)
338335, 337lerecd 12105 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁) ↔ (1 / (𝑅 / 𝑁)) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))))
339334, 338mpbid 223 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (𝑅 / 𝑁)) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
340333, 339eqbrtrrd 4868 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
341309absnegd 14411 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) = (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))))
342193, 172, 308absdivd 14417 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))) = ((abs‘1) / (abs‘((𝐴 / 𝑁) · 𝑡))))
343 abs1 14260 . . . . . . . . . . . . . . . . . . . 20 (abs‘1) = 1
344343oveq1i 6884 . . . . . . . . . . . . . . . . . . 19 ((abs‘1) / (abs‘((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))
345342, 344syl6eq 2856 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
346341, 345eqtrd 2840 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
347340, 346breqtrrd 4872 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ≤ (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))))
348332, 323, 318, 347lesub1dd 10928 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 / 𝑅) − 1) ≤ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1))
349331, 348eqbrtrd 4866 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) ≤ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1))
350343oveq2i 6885 . . . . . . . . . . . . . . . 16 ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − (abs‘1)) = ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1)
351322, 193abs2difd 14419 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − (abs‘1)) ≤ (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
352350, 351syl5eqbrr 4880 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ≤ (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
353193, 309addcomd 10523 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = ((1 / ((𝐴 / 𝑁) · 𝑡)) + 1))
354353negeqd 10560 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → -(1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = -((1 / ((𝐴 / 𝑁) · 𝑡)) + 1))
355309, 193negdi2d 10691 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0(,)1)) → -((1 / ((𝐴 / 𝑁) · 𝑡)) + 1) = (-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1))
356354, 355eqtrd 2840 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0(,)1)) → -(1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = (-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1))
357356fveq2d 6412 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) = (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
358310absnegd 14411 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘-(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) = (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
359357, 358eqtr3d 2842 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)) = (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
360352, 359breqtrd 4870 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ≤ (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
361321, 324, 325, 349, 360letrd 10479 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / 𝑅) ≤ (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
362300, 317, 318, 320, 361lediv2ad 12108 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) ≤ (1 / ((𝑁𝑅) / 𝑅)))
36316, 236subcld 10677 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁𝑅) ∈ ℂ)
364363adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁𝑅) ∈ ℂ)
36547, 239gtned 10457 . . . . . . . . . . . . . . . 16 (𝜑𝑁𝑅)
36616, 236, 365subne0d 10686 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁𝑅) ≠ 0)
367366adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁𝑅) ≠ 0)
368364, 326, 367, 327recdivd 11103 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((𝑁𝑅) / 𝑅)) = (𝑅 / (𝑁𝑅)))
369166, 326nncand 10682 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 − (𝑁𝑅)) = 𝑅)
370369oveq1d 6889 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 − (𝑁𝑅)) / (𝑁𝑅)) = (𝑅 / (𝑁𝑅)))
371166, 364, 364, 367divsubdird 11125 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 − (𝑁𝑅)) / (𝑁𝑅)) = ((𝑁 / (𝑁𝑅)) − ((𝑁𝑅) / (𝑁𝑅))))
372370, 371eqtr3d 2842 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 / (𝑁𝑅)) = ((𝑁 / (𝑁𝑅)) − ((𝑁𝑅) / (𝑁𝑅))))
373364, 367dividd 11084 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁𝑅) / (𝑁𝑅)) = 1)
374373oveq2d 6890 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 / (𝑁𝑅)) − ((𝑁𝑅) / (𝑁𝑅))) = ((𝑁 / (𝑁𝑅)) − 1))
375368, 372, 3743eqtrd 2844 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((𝑁𝑅) / 𝑅)) = ((𝑁 / (𝑁𝑅)) − 1))
376362, 375breqtrd 4870 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) ≤ ((𝑁 / (𝑁𝑅)) − 1))
377194, 193, 194, 195divsubdird 11125 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) − 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = (((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))
378172, 193pncand 10678 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) − 1) = ((𝐴 / 𝑁) · 𝑡))
379378oveq1d 6889 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) − 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
380194, 195dividd 11084 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = 1)
381380oveq1d 6889 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))
382377, 379, 3813eqtr3rd 2849 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
383194, 172, 195, 308recdivd 11103 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡))) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
384314oveq2d 6890 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (1 / ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡))) = (1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
385382, 383, 3843eqtr2d 2846 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
386385fveq2d 6412 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
387193, 310, 316absdivd 14417 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = ((abs‘1) / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
388343oveq1i 6884 . . . . . . . . . . . . 13 ((abs‘1) / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
389387, 388syl6eq 2856 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
390386, 389eqtrd 2840 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
391363, 366reccld 11079 . . . . . . . . . . . . . 14 (𝜑 → (1 / (𝑁𝑅)) ∈ ℂ)
392391adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (1 / (𝑁𝑅)) ∈ ℂ)
393244recnd 10353 . . . . . . . . . . . . . 14 (𝜑 → (1 / 𝑁) ∈ ℂ)
394393adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (1 / 𝑁) ∈ ℂ)
395166, 392, 394subdid 10771 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) = ((𝑁 · (1 / (𝑁𝑅))) − (𝑁 · (1 / 𝑁))))
396166, 364, 367divrecd 11089 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 / (𝑁𝑅)) = (𝑁 · (1 / (𝑁𝑅))))
397396eqcomd 2812 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · (1 / (𝑁𝑅))) = (𝑁 / (𝑁𝑅)))
398166, 167recidd 11081 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · (1 / 𝑁)) = 1)
399397, 398oveq12d 6892 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (0(,)1)) → ((𝑁 · (1 / (𝑁𝑅))) − (𝑁 · (1 / 𝑁))) = ((𝑁 / (𝑁𝑅)) − 1))
400395, 399eqtrd 2840 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) = ((𝑁 / (𝑁𝑅)) − 1))
401376, 390, 4003brtr4d 4876 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ≤ (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
402282, 289, 284, 293, 295, 296, 297, 401lemul12ad 11251 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑅 · (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))))
403245recnd 10353 . . . . . . . . . . 11 (𝜑 → ((1 / (𝑁𝑅)) − (1 / 𝑁)) ∈ ℂ)
404403adantr 468 . . . . . . . . . 10 ((𝜑𝑡 ∈ (0(,)1)) → ((1 / (𝑁𝑅)) − (1 / 𝑁)) ∈ ℂ)
405326, 166, 404mul12d 10530 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 · (𝑁 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))) = (𝑁 · (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))))
406402, 405breqtrd 4870 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑁 · (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁)))))
407282, 284remulcld 10355 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ∈ ℝ)
408246adantr 468 . . . . . . . . 9 ((𝜑𝑡 ∈ (0(,)1)) → (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ∈ ℝ)
409407, 408, 336ledivmuld 12139 . . . . . . . 8 ((𝜑𝑡 ∈ (0(,)1)) → ((((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ↔ ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑁 · (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))))
410406, 409mpbird 248 . . . . . . 7 ((𝜑𝑡 ∈ (0(,)1)) → (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
411288, 410eqbrtrd 4866 . . . . . 6 ((𝜑𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
412257, 262, 411chvar 2436 . . . . 5 ((𝜑𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
413249, 412eqbrtrd 4866 . . . 4 ((𝜑𝑦 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
4143, 4, 151, 230, 246, 413dvlip 23970 . . 3 ((𝜑 ∧ (1 ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) ≤ ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
4151, 2, 414mpanr12 688 . 2 (𝜑 → (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) ≤ ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
416 eqidd 2807 . . . . . 6 (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))
417 oveq2 6882 . . . . . . . 8 (𝑡 = 1 → ((𝐴 / 𝑁) · 𝑡) = ((𝐴 / 𝑁) · 1))
418417, 182sylan9eqr 2862 . . . . . . 7 ((𝜑𝑡 = 1) → ((𝐴 / 𝑁) · 𝑡) = (𝐴 / 𝑁))
419418fvoveq1d 6896 . . . . . . 7 ((𝜑𝑡 = 1) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘((𝐴 / 𝑁) + 1)))
420418, 419oveq12d 6892 . . . . . 6 ((𝜑𝑡 = 1) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
4211a1i 11 . . . . . 6 (𝜑 → 1 ∈ (0[,]1))
422 ovexd 6908 . . . . . 6 (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ V)
423416, 420, 421, 422fvmptd 6509 . . . . 5 (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
424 oveq2 6882 . . . . . . . . 9 (𝑡 = 0 → ((𝐴 / 𝑁) · 𝑡) = ((𝐴 / 𝑁) · 0))
42518mul01d 10520 . . . . . . . . 9 (𝜑 → ((𝐴 / 𝑁) · 0) = 0)
426424, 425sylan9eqr 2862 . . . . . . . 8 ((𝜑𝑡 = 0) → ((𝐴 / 𝑁) · 𝑡) = 0)
427426oveq1d 6889 . . . . . . . . . . 11 ((𝜑𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) + 1) = (0 + 1))
428 0p1e1 11414 . . . . . . . . . . 11 (0 + 1) = 1
429427, 428syl6eq 2856 . . . . . . . . . 10 ((𝜑𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) + 1) = 1)
430429fveq2d 6412 . . . . . . . . 9 ((𝜑𝑡 = 0) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘1))
431 log1 24546 . . . . . . . . 9 (log‘1) = 0
432430, 431syl6eq 2856 . . . . . . . 8 ((𝜑𝑡 = 0) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = 0)
433426, 432oveq12d 6892 . . . . . . 7 ((𝜑𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = (0 − 0))
434 0m0e0 11412 . . . . . . 7 (0 − 0) = 0
435433, 434syl6eq 2856 . . . . . 6 ((𝜑𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = 0)
4362a1i 11 . . . . . 6 (𝜑 → 0 ∈ (0[,]1))
437416, 435, 436, 436fvmptd 6509 . . . . 5 (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0) = 0)
438423, 437oveq12d 6892 . . . 4 (𝜑 → (((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0)) = (((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) − 0))
43918, 142addcld 10344 . . . . . . 7 (𝜑 → ((𝐴 / 𝑁) + 1) ∈ ℂ)
44012, 14dmgmdivn0 24968 . . . . . . 7 (𝜑 → ((𝐴 / 𝑁) + 1) ≠ 0)
441439, 440logcld 24531 . . . . . 6 (𝜑 → (log‘((𝐴 / 𝑁) + 1)) ∈ ℂ)
44218, 441subcld 10677 . . . . 5 (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ ℂ)
443442subid1d 10666 . . . 4 (𝜑 → (((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) − 0) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
444438, 443eqtr2d 2841 . . 3 (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) = (((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0)))
445444fveq2d 6412 . 2 (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) = (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))))
446 1m0e1 11413 . . . . . 6 (1 − 0) = 1
447446fveq2i 6411 . . . . 5 (abs‘(1 − 0)) = (abs‘1)
448447, 343eqtri 2828 . . . 4 (abs‘(1 − 0)) = 1
449448oveq2i 6885 . . 3 ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))) = ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · 1)
450236, 403mulcld 10345 . . . 4 (𝜑 → (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) ∈ ℂ)
451450mulid1d 10342 . . 3 (𝜑 → ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · 1) = (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
452449, 451syl5req 2853 . 2 (𝜑 → (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) = ((𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
453415, 445, 4523brtr4d 4876 1 (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁𝑅)) − (1 / 𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wne 2978  wral 3096  {crab 3100  Vcvv 3391  cdif 3766  wss 3769  {cpr 4372   class class class wbr 4844  cmpt 4923  dom cdm 5311  ran crn 5312  cres 5313  ccom 5315  wf 6097  cfv 6101  (class class class)co 6874  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226  -∞cmnf 10357   < clt 10359  cle 10360  cmin 10551  -cneg 10552   / cdiv 10969  cn 11305  2c2 11356  0cn0 11559  cz 11643  +crp 12046  (,)cioo 12393  (,]cioc 12394  [,]cicc 12396  cre 14060  abscabs 14197  TopOpenctopn 16287  topGenctg 16303  fldccnfld 19954  Topctop 20911  intcnt 21035   Cn ccn 21242   ×t ctx 21577  cnccncf 22892   D cdv 23841  logclog 24515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299  ax-addf 10300  ax-mulf 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-om 7296  df-1st 7398  df-2nd 7399  df-supp 7530  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-pm 8095  df-ixp 8146  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fsupp 8515  df-fi 8556  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-4 11366  df-5 11367  df-6 11368  df-7 11369  df-8 11370  df-9 11371  df-n0 11560  df-z 11644  df-dec 11760  df-uz 11905  df-q 12008  df-rp 12047  df-xneg 12162  df-xadd 12163  df-xmul 12164  df-ioo 12397  df-ioc 12398  df-ico 12399  df-icc 12400  df-fz 12550  df-fzo 12690  df-fl 12817  df-mod 12893  df-seq 13025  df-exp 13084  df-fac 13281  df-bc 13310  df-hash 13338  df-shft 14030  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-limsup 14425  df-clim 14442  df-rlim 14443  df-sum 14640  df-ef 15018  df-sin 15020  df-cos 15021  df-tan 15022  df-pi 15023  df-struct 16070  df-ndx 16071  df-slot 16072  df-base 16074  df-sets 16075  df-ress 16076  df-plusg 16166  df-mulr 16167  df-starv 16168  df-sca 16169  df-vsca 16170  df-ip 16171  df-tset 16172  df-ple 16173  df-ds 16175  df-unif 16176  df-hom 16177  df-cco 16178  df-rest 16288  df-topn 16289  df-0g 16307  df-gsum 16308  df-topgen 16309  df-pt 16310  df-prds 16313  df-xrs 16367  df-qtop 16372  df-imas 16373  df-xps 16375  df-mre 16451  df-mrc 16452  df-acs 16454  df-mgm 17447  df-sgrp 17489  df-mnd 17500  df-submnd 17541  df-mulg 17746  df-cntz 17951  df-cmn 18396  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-cmp 21404  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 23844  df-dv 23845  df-log 24517
This theorem is referenced by:  lgamgulmlem3  24971
  Copyright terms: Public domain W3C validator