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

Theorem pntibndlem2 26955
Description: Lemma for pntibnd 26957. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
Hypotheses
Ref Expression
pntibnd.r 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
pntibndlem1.1 (πœ‘ β†’ 𝐴 ∈ ℝ+)
pntibndlem1.l 𝐿 = ((1 / 4) / (𝐴 + 3))
pntibndlem3.2 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ (absβ€˜((π‘…β€˜π‘₯) / π‘₯)) ≀ 𝐴)
pntibndlem3.3 (πœ‘ β†’ 𝐡 ∈ ℝ+)
pntibndlem3.k 𝐾 = (expβ€˜(𝐡 / (𝐸 / 2)))
pntibndlem3.c 𝐢 = ((2 Β· 𝐡) + (logβ€˜2))
pntibndlem3.4 (πœ‘ β†’ 𝐸 ∈ (0(,)1))
pntibndlem3.6 (πœ‘ β†’ 𝑍 ∈ ℝ+)
pntibndlem2.10 (πœ‘ β†’ 𝑁 ∈ β„•)
pntibndlem2.5 (πœ‘ β†’ 𝑇 ∈ ℝ+)
pntibndlem2.6 (πœ‘ β†’ βˆ€π‘₯ ∈ (1(,)+∞)βˆ€π‘¦ ∈ (π‘₯[,](2 Β· π‘₯))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))))
pntibndlem2.7 𝑋 = ((expβ€˜(𝑇 / (𝐸 / 4))) + 𝑍)
pntibndlem2.8 (πœ‘ β†’ 𝑀 ∈ ((expβ€˜(𝐢 / 𝐸))[,)+∞))
pntibndlem2.9 (πœ‘ β†’ π‘Œ ∈ (𝑋(,)+∞))
pntibndlem2.11 (πœ‘ β†’ ((π‘Œ < 𝑁 ∧ 𝑁 ≀ ((𝑀 / 2) Β· π‘Œ)) ∧ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ≀ (𝐸 / 2)))
Assertion
Ref Expression
pntibndlem2 (πœ‘ β†’ βˆƒπ‘§ ∈ ℝ+ ((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
Distinct variable groups:   𝑒,π‘Ž,π‘₯,𝑦,𝑧,𝐸   𝑒,𝐿,π‘₯,𝑧   𝑁,π‘Ž,𝑒,π‘₯,𝑦,𝑧   𝑒,𝐴,π‘₯   𝑒,𝐢,π‘₯,𝑦   𝑒,𝑅,π‘₯,𝑦,𝑧   𝑧,𝑀   π‘₯,𝑇,𝑦   𝑧,π‘Œ   𝑒,𝑍,π‘₯,𝑦   πœ‘,𝑒
Allowed substitution hints:   πœ‘(π‘₯,𝑦,𝑧,π‘Ž)   𝐴(𝑦,𝑧,π‘Ž)   𝐡(π‘₯,𝑦,𝑧,𝑒,π‘Ž)   𝐢(𝑧,π‘Ž)   𝑅(π‘Ž)   𝑇(𝑧,𝑒,π‘Ž)   𝐾(π‘₯,𝑦,𝑧,𝑒,π‘Ž)   𝐿(𝑦,π‘Ž)   𝑀(π‘₯,𝑦,𝑒,π‘Ž)   𝑋(π‘₯,𝑦,𝑧,𝑒,π‘Ž)   π‘Œ(π‘₯,𝑦,𝑒,π‘Ž)   𝑍(𝑧,π‘Ž)

Proof of Theorem pntibndlem2
StepHypRef Expression
1 pntibndlem2.10 . . 3 (πœ‘ β†’ 𝑁 ∈ β„•)
21nnrpd 12962 . 2 (πœ‘ β†’ 𝑁 ∈ ℝ+)
3 pntibndlem2.11 . . . . 5 (πœ‘ β†’ ((π‘Œ < 𝑁 ∧ 𝑁 ≀ ((𝑀 / 2) Β· π‘Œ)) ∧ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ≀ (𝐸 / 2)))
43simpld 496 . . . 4 (πœ‘ β†’ (π‘Œ < 𝑁 ∧ 𝑁 ≀ ((𝑀 / 2) Β· π‘Œ)))
54simpld 496 . . 3 (πœ‘ β†’ π‘Œ < 𝑁)
6 1red 11163 . . . . . 6 (πœ‘ β†’ 1 ∈ ℝ)
7 ioossre 13332 . . . . . . . 8 (0(,)1) βŠ† ℝ
8 pntibnd.r . . . . . . . . 9 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
9 pntibndlem1.1 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ ℝ+)
10 pntibndlem1.l . . . . . . . . 9 𝐿 = ((1 / 4) / (𝐴 + 3))
118, 9, 10pntibndlem1 26953 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ (0(,)1))
127, 11sselid 3947 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ ℝ)
13 pntibndlem3.4 . . . . . . . 8 (πœ‘ β†’ 𝐸 ∈ (0(,)1))
147, 13sselid 3947 . . . . . . 7 (πœ‘ β†’ 𝐸 ∈ ℝ)
1512, 14remulcld 11192 . . . . . 6 (πœ‘ β†’ (𝐿 Β· 𝐸) ∈ ℝ)
166, 15readdcld 11191 . . . . 5 (πœ‘ β†’ (1 + (𝐿 Β· 𝐸)) ∈ ℝ)
171nnred 12175 . . . . 5 (πœ‘ β†’ 𝑁 ∈ ℝ)
1816, 17remulcld 11192 . . . 4 (πœ‘ β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) ∈ ℝ)
19 2re 12234 . . . . 5 2 ∈ ℝ
20 remulcl 11143 . . . . 5 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ (2 Β· 𝑁) ∈ ℝ)
2119, 17, 20sylancr 588 . . . 4 (πœ‘ β†’ (2 Β· 𝑁) ∈ ℝ)
22 pntibndlem3.c . . . . . . . . . 10 𝐢 = ((2 Β· 𝐡) + (logβ€˜2))
23 pntibndlem3.3 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ ℝ+)
2423rpred 12964 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ ℝ)
25 remulcl 11143 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (2 Β· 𝐡) ∈ ℝ)
2619, 24, 25sylancr 588 . . . . . . . . . . 11 (πœ‘ β†’ (2 Β· 𝐡) ∈ ℝ)
27 2rp 12927 . . . . . . . . . . . . 13 2 ∈ ℝ+
2827a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 2 ∈ ℝ+)
2928relogcld 25994 . . . . . . . . . . 11 (πœ‘ β†’ (logβ€˜2) ∈ ℝ)
3026, 29readdcld 11191 . . . . . . . . . 10 (πœ‘ β†’ ((2 Β· 𝐡) + (logβ€˜2)) ∈ ℝ)
3122, 30eqeltrid 2842 . . . . . . . . 9 (πœ‘ β†’ 𝐢 ∈ ℝ)
32 eliooord 13330 . . . . . . . . . . . 12 (𝐸 ∈ (0(,)1) β†’ (0 < 𝐸 ∧ 𝐸 < 1))
3313, 32syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (0 < 𝐸 ∧ 𝐸 < 1))
3433simpld 496 . . . . . . . . . 10 (πœ‘ β†’ 0 < 𝐸)
3514, 34elrpd 12961 . . . . . . . . 9 (πœ‘ β†’ 𝐸 ∈ ℝ+)
3631, 35rerpdivcld 12995 . . . . . . . 8 (πœ‘ β†’ (𝐢 / 𝐸) ∈ ℝ)
3736reefcld 15977 . . . . . . 7 (πœ‘ β†’ (expβ€˜(𝐢 / 𝐸)) ∈ ℝ)
38 pnfxr 11216 . . . . . . 7 +∞ ∈ ℝ*
39 icossre 13352 . . . . . . 7 (((expβ€˜(𝐢 / 𝐸)) ∈ ℝ ∧ +∞ ∈ ℝ*) β†’ ((expβ€˜(𝐢 / 𝐸))[,)+∞) βŠ† ℝ)
4037, 38, 39sylancl 587 . . . . . 6 (πœ‘ β†’ ((expβ€˜(𝐢 / 𝐸))[,)+∞) βŠ† ℝ)
41 pntibndlem2.8 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ ((expβ€˜(𝐢 / 𝐸))[,)+∞))
4240, 41sseldd 3950 . . . . 5 (πœ‘ β†’ 𝑀 ∈ ℝ)
43 ioossre 13332 . . . . . 6 (𝑋(,)+∞) βŠ† ℝ
44 pntibndlem2.9 . . . . . 6 (πœ‘ β†’ π‘Œ ∈ (𝑋(,)+∞))
4543, 44sselid 3947 . . . . 5 (πœ‘ β†’ π‘Œ ∈ ℝ)
4642, 45remulcld 11192 . . . 4 (πœ‘ β†’ (𝑀 Β· π‘Œ) ∈ ℝ)
4719a1i 11 . . . . 5 (πœ‘ β†’ 2 ∈ ℝ)
48 eliooord 13330 . . . . . . . . . . . . 13 (𝐿 ∈ (0(,)1) β†’ (0 < 𝐿 ∧ 𝐿 < 1))
4911, 48syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (0 < 𝐿 ∧ 𝐿 < 1))
5049simpld 496 . . . . . . . . . . 11 (πœ‘ β†’ 0 < 𝐿)
5112, 50elrpd 12961 . . . . . . . . . 10 (πœ‘ β†’ 𝐿 ∈ ℝ+)
5251rpge0d 12968 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ 𝐿)
5349simprd 497 . . . . . . . . 9 (πœ‘ β†’ 𝐿 < 1)
5435rpge0d 12968 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ 𝐸)
5533simprd 497 . . . . . . . . 9 (πœ‘ β†’ 𝐸 < 1)
5612, 6, 14, 6, 52, 53, 54, 55ltmul12ad 12103 . . . . . . . 8 (πœ‘ β†’ (𝐿 Β· 𝐸) < (1 Β· 1))
57 1t1e1 12322 . . . . . . . 8 (1 Β· 1) = 1
5856, 57breqtrdi 5151 . . . . . . 7 (πœ‘ β†’ (𝐿 Β· 𝐸) < 1)
5915, 6, 6, 58ltadd2dd 11321 . . . . . 6 (πœ‘ β†’ (1 + (𝐿 Β· 𝐸)) < (1 + 1))
60 df-2 12223 . . . . . 6 2 = (1 + 1)
6159, 60breqtrrdi 5152 . . . . 5 (πœ‘ β†’ (1 + (𝐿 Β· 𝐸)) < 2)
6216, 47, 2, 61ltmul1dd 13019 . . . 4 (πœ‘ β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (2 Β· 𝑁))
634simprd 497 . . . . . 6 (πœ‘ β†’ 𝑁 ≀ ((𝑀 / 2) Β· π‘Œ))
6442recnd 11190 . . . . . . 7 (πœ‘ β†’ 𝑀 ∈ β„‚)
6545recnd 11190 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ β„‚)
66 rpcnne0 12940 . . . . . . . 8 (2 ∈ ℝ+ β†’ (2 ∈ β„‚ ∧ 2 β‰  0))
6727, 66mp1i 13 . . . . . . 7 (πœ‘ β†’ (2 ∈ β„‚ ∧ 2 β‰  0))
68 div23 11839 . . . . . . 7 ((𝑀 ∈ β„‚ ∧ π‘Œ ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0)) β†’ ((𝑀 Β· π‘Œ) / 2) = ((𝑀 / 2) Β· π‘Œ))
6964, 65, 67, 68syl3anc 1372 . . . . . 6 (πœ‘ β†’ ((𝑀 Β· π‘Œ) / 2) = ((𝑀 / 2) Β· π‘Œ))
7063, 69breqtrrd 5138 . . . . 5 (πœ‘ β†’ 𝑁 ≀ ((𝑀 Β· π‘Œ) / 2))
7117, 46, 28lemuldiv2d 13014 . . . . 5 (πœ‘ β†’ ((2 Β· 𝑁) ≀ (𝑀 Β· π‘Œ) ↔ 𝑁 ≀ ((𝑀 Β· π‘Œ) / 2)))
7270, 71mpbird 257 . . . 4 (πœ‘ β†’ (2 Β· 𝑁) ≀ (𝑀 Β· π‘Œ))
7318, 21, 46, 62, 72ltletrd 11322 . . 3 (πœ‘ β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ))
74 pntibndlem3.2 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ (absβ€˜((π‘…β€˜π‘₯) / π‘₯)) ≀ 𝐴)
75 pntibndlem3.k . . . . . . . . . . . 12 𝐾 = (expβ€˜(𝐡 / (𝐸 / 2)))
768, 9, 10, 74, 23, 75, 22, 13, 9, 1pntibndlem2a 26954 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 ∈ ℝ ∧ 𝑁 ≀ 𝑒 ∧ 𝑒 ≀ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁)))
7776simp1d 1143 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ∈ ℝ)
782adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ∈ ℝ+)
7976simp2d 1144 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ≀ 𝑒)
8077, 78, 79rpgecld 13003 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ∈ ℝ+)
818pntrf 26927 . . . . . . . . . 10 𝑅:ℝ+βŸΆβ„
8281ffvelcdmi 7039 . . . . . . . . 9 (𝑒 ∈ ℝ+ β†’ (π‘…β€˜π‘’) ∈ ℝ)
8380, 82syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘’) ∈ ℝ)
8483, 80rerpdivcld 12995 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) / 𝑒) ∈ ℝ)
8584recnd 11190 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) / 𝑒) ∈ β„‚)
8685abscld 15328 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ∈ ℝ)
8781ffvelcdmi 7039 . . . . . . . . . . . 12 (𝑁 ∈ ℝ+ β†’ (π‘…β€˜π‘) ∈ ℝ)
882, 87syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (π‘…β€˜π‘) ∈ ℝ)
8988, 1nndivred 12214 . . . . . . . . . 10 (πœ‘ β†’ ((π‘…β€˜π‘) / 𝑁) ∈ ℝ)
9089adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘) / 𝑁) ∈ ℝ)
9190recnd 11190 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘) / 𝑁) ∈ β„‚)
9285, 91subcld 11519 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁)) ∈ β„‚)
9392abscld 15328 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ∈ ℝ)
9491abscld 15328 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ∈ ℝ)
9593, 94readdcld 11191 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁))) ∈ ℝ)
9614adantr 482 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐸 ∈ ℝ)
9785, 91abs2difd 15349 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) βˆ’ (absβ€˜((π‘…β€˜π‘) / 𝑁))) ≀ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))))
9886, 94, 93lesubaddd 11759 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) βˆ’ (absβ€˜((π‘…β€˜π‘) / 𝑁))) ≀ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ↔ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁)))))
9997, 98mpbid 231 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁))))
10096rehalfcld 12407 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 2) ∈ ℝ)
10117adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ∈ ℝ)
10277, 101resubcld 11590 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 βˆ’ 𝑁) ∈ ℝ)
103102, 78rerpdivcld 12995 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) ∈ ℝ)
104 3re 12240 . . . . . . . . . . . 12 3 ∈ ℝ
105104a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 3 ∈ ℝ)
10686, 105readdcld 11191 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ∈ ℝ)
107103, 106remulcld 11192 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ∈ ℝ)
108 pntibndlem2.5 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 ∈ ℝ+)
109108rpred 12964 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ ℝ)
110109adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑇 ∈ ℝ)
111 1red 11163 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 1 ∈ ℝ)
112 4nn 12243 . . . . . . . . . . . . . . . . . 18 4 ∈ β„•
113 nnrp 12933 . . . . . . . . . . . . . . . . . 18 (4 ∈ β„• β†’ 4 ∈ ℝ+)
114112, 113mp1i 13 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 4 ∈ ℝ+)
11535, 114rpdivcld 12981 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐸 / 4) ∈ ℝ+)
116108, 115rpdivcld 12981 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑇 / (𝐸 / 4)) ∈ ℝ+)
117116rpred 12964 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑇 / (𝐸 / 4)) ∈ ℝ)
118117reefcld 15977 . . . . . . . . . . . . 13 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) ∈ ℝ)
119118adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (expβ€˜(𝑇 / (𝐸 / 4))) ∈ ℝ)
120 efgt1 16005 . . . . . . . . . . . . . 14 ((𝑇 / (𝐸 / 4)) ∈ ℝ+ β†’ 1 < (expβ€˜(𝑇 / (𝐸 / 4))))
121116, 120syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 1 < (expβ€˜(𝑇 / (𝐸 / 4))))
122121adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 1 < (expβ€˜(𝑇 / (𝐸 / 4))))
123 pntibndlem2.7 . . . . . . . . . . . . . . . 16 𝑋 = ((expβ€˜(𝑇 / (𝐸 / 4))) + 𝑍)
124 pntibndlem3.6 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑍 ∈ ℝ+)
125124rpred 12964 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑍 ∈ ℝ)
126118, 125readdcld 11191 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((expβ€˜(𝑇 / (𝐸 / 4))) + 𝑍) ∈ ℝ)
127123, 126eqeltrid 2842 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 ∈ ℝ)
128118, 124ltaddrpd 12997 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < ((expβ€˜(𝑇 / (𝐸 / 4))) + 𝑍))
129128, 123breqtrrdi 5152 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < 𝑋)
130 eliooord 13330 . . . . . . . . . . . . . . . . 17 (π‘Œ ∈ (𝑋(,)+∞) β†’ (𝑋 < π‘Œ ∧ π‘Œ < +∞))
13144, 130syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑋 < π‘Œ ∧ π‘Œ < +∞))
132131simpld 496 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 < π‘Œ)
133118, 127, 45, 129, 132lttrd 11323 . . . . . . . . . . . . . 14 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < π‘Œ)
134118, 45, 17, 133, 5lttrd 11323 . . . . . . . . . . . . 13 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < 𝑁)
135134adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < 𝑁)
136111, 119, 101, 122, 135lttrd 11323 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 1 < 𝑁)
137101, 136rplogcld 26000 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (logβ€˜π‘) ∈ ℝ+)
138110, 137rerpdivcld 12995 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ∈ ℝ)
139107, 138readdcld 11191 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))) ∈ ℝ)
140 peano2re 11335 . . . . . . . . . . . 12 ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) ∈ ℝ β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) ∈ ℝ)
14186, 140syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) ∈ ℝ)
142103, 141remulcld 11192 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) ∈ ℝ)
143 chpcl 26489 . . . . . . . . . . . . 13 (𝑒 ∈ ℝ β†’ (Οˆβ€˜π‘’) ∈ ℝ)
14477, 143syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘’) ∈ ℝ)
145 chpcl 26489 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ β†’ (Οˆβ€˜π‘) ∈ ℝ)
146101, 145syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘) ∈ ℝ)
147144, 146resubcld 11590 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) ∈ ℝ)
148147, 78rerpdivcld 12995 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁) ∈ ℝ)
149142, 148readdcld 11191 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) ∈ ℝ)
150103, 86remulcld 11192 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) ∈ ℝ)
15188adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘) ∈ ℝ)
15283, 151resubcld 11590 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) ∈ ℝ)
153152recnd 11190 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) ∈ β„‚)
154153abscld 15328 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) ∈ ℝ)
155154, 78rerpdivcld 12995 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁) ∈ ℝ)
156150, 155readdcld 11191 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)) ∈ ℝ)
157103, 84remulcld 11192 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) ∈ ℝ)
158157renegcld 11589 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) ∈ ℝ)
159158recnd 11190 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) ∈ β„‚)
160152, 78rerpdivcld 12995 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁) ∈ ℝ)
161160recnd 11190 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁) ∈ β„‚)
162159, 161abstrid 15348 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) + (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁))) ≀ ((absβ€˜-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) + (absβ€˜(((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁))))
16377recnd 11190 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ∈ β„‚)
164101recnd 11190 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ∈ β„‚)
16578rpne0d 12969 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 β‰  0)
166163, 164, 164, 165divsubdird 11977 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) = ((𝑒 / 𝑁) βˆ’ (𝑁 / 𝑁)))
167164, 165dividd 11936 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 / 𝑁) = 1)
168167oveq2d 7378 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 / 𝑁) βˆ’ (𝑁 / 𝑁)) = ((𝑒 / 𝑁) βˆ’ 1))
169166, 168eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) = ((𝑒 / 𝑁) βˆ’ 1))
170169oveq1d 7377 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = (((𝑒 / 𝑁) βˆ’ 1) Β· ((π‘…β€˜π‘’) / 𝑒)))
17177, 78rerpdivcld 12995 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 / 𝑁) ∈ ℝ)
172171recnd 11190 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 / 𝑁) ∈ β„‚)
173 1cnd 11157 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 1 ∈ β„‚)
174172, 173, 85subdird 11619 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 / 𝑁) βˆ’ 1) Β· ((π‘…β€˜π‘’) / 𝑒)) = (((𝑒 / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) βˆ’ (1 Β· ((π‘…β€˜π‘’) / 𝑒))))
17580rpcnne0d 12973 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 ∈ β„‚ ∧ 𝑒 β‰  0))
17678rpcnne0d 12973 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 ∈ β„‚ ∧ 𝑁 β‰  0))
17783recnd 11190 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘’) ∈ β„‚)
178 dmdcan 11872 . . . . . . . . . . . . . . . . . . 19 (((𝑒 ∈ β„‚ ∧ 𝑒 β‰  0) ∧ (𝑁 ∈ β„‚ ∧ 𝑁 β‰  0) ∧ (π‘…β€˜π‘’) ∈ β„‚) β†’ ((𝑒 / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = ((π‘…β€˜π‘’) / 𝑁))
179175, 176, 177, 178syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = ((π‘…β€˜π‘’) / 𝑁))
18085mulid2d 11180 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 Β· ((π‘…β€˜π‘’) / 𝑒)) = ((π‘…β€˜π‘’) / 𝑒))
181179, 180oveq12d 7380 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) βˆ’ (1 Β· ((π‘…β€˜π‘’) / 𝑒))) = (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘’) / 𝑒)))
182170, 174, 1813eqtrd 2781 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘’) / 𝑒)))
183182negeqd 11402 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = -(((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘’) / 𝑒)))
18483, 78rerpdivcld 12995 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) / 𝑁) ∈ ℝ)
185184recnd 11190 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) / 𝑁) ∈ β„‚)
186185, 85negsubdi2d 11535 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘’) / 𝑒)) = (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘’) / 𝑁)))
187183, 186eqtrd 2777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘’) / 𝑁)))
188151recnd 11190 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘) ∈ β„‚)
189177, 188, 164, 165divsubdird 11977 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁) = (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘) / 𝑁)))
190187, 189oveq12d 7380 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) + (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁)) = ((((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘’) / 𝑁)) + (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘) / 𝑁))))
19185, 185, 91npncand 11543 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘’) / 𝑁)) + (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘) / 𝑁))) = (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁)))
192190, 191eqtrd 2777 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) + (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁)) = (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁)))
193192fveq2d 6851 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) + (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁))) = (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))))
194157recnd 11190 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) ∈ β„‚)
195194absnegd 15341 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) = (absβ€˜(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))))
196103recnd 11190 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) ∈ β„‚)
197196, 85absmuld 15346 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) = ((absβ€˜((𝑒 βˆ’ 𝑁) / 𝑁)) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))))
19877, 101subge0d 11752 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (0 ≀ (𝑒 βˆ’ 𝑁) ↔ 𝑁 ≀ 𝑒))
19979, 198mpbird 257 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 0 ≀ (𝑒 βˆ’ 𝑁))
200102, 78, 199divge0d 13004 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 0 ≀ ((𝑒 βˆ’ 𝑁) / 𝑁))
201103, 200absidd 15314 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((𝑒 βˆ’ 𝑁) / 𝑁)) = ((𝑒 βˆ’ 𝑁) / 𝑁))
202201oveq1d 7377 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((𝑒 βˆ’ 𝑁) / 𝑁)) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))))
203195, 197, 2023eqtrd 2781 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))))
204153, 164, 165absdivd 15347 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁)) = ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / (absβ€˜π‘)))
20578rprege0d 12971 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 ∈ ℝ ∧ 0 ≀ 𝑁))
206 absid 15188 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 0 ≀ 𝑁) β†’ (absβ€˜π‘) = 𝑁)
207205, 206syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜π‘) = 𝑁)
208207oveq2d 7378 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / (absβ€˜π‘)) = ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁))
209204, 208eqtrd 2777 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁)) = ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁))
210203, 209oveq12d 7380 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) + (absβ€˜(((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)))
211162, 193, 2103brtr3d 5141 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)))
212102, 147readdcld 11191 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) ∈ ℝ)
213212, 78rerpdivcld 12995 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁) ∈ ℝ)
214147recnd 11190 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) ∈ β„‚)
215164, 163subcld 11519 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 βˆ’ 𝑒) ∈ β„‚)
216214, 215abstrid 15348 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒))) ≀ ((absβ€˜((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) + (absβ€˜(𝑁 βˆ’ 𝑒))))
2178pntrval 26926 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ ℝ+ β†’ (π‘…β€˜π‘’) = ((Οˆβ€˜π‘’) βˆ’ 𝑒))
21880, 217syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘’) = ((Οˆβ€˜π‘’) βˆ’ 𝑒))
2198pntrval 26926 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℝ+ β†’ (π‘…β€˜π‘) = ((Οˆβ€˜π‘) βˆ’ 𝑁))
22078, 219syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘) = ((Οˆβ€˜π‘) βˆ’ 𝑁))
221218, 220oveq12d 7380 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) = (((Οˆβ€˜π‘’) βˆ’ 𝑒) βˆ’ ((Οˆβ€˜π‘) βˆ’ 𝑁)))
222144recnd 11190 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘’) ∈ β„‚)
223146recnd 11190 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘) ∈ β„‚)
224 subadd4 11452 . . . . . . . . . . . . . . . . . 18 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ (Οˆβ€˜π‘) ∈ β„‚) ∧ (𝑒 ∈ β„‚ ∧ 𝑁 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) βˆ’ (𝑒 βˆ’ 𝑁)) = (((Οˆβ€˜π‘’) + 𝑁) βˆ’ ((Οˆβ€˜π‘) + 𝑒)))
225 sub4 11453 . . . . . . . . . . . . . . . . . 18 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ (Οˆβ€˜π‘) ∈ β„‚) ∧ (𝑒 ∈ β„‚ ∧ 𝑁 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) βˆ’ (𝑒 βˆ’ 𝑁)) = (((Οˆβ€˜π‘’) βˆ’ 𝑒) βˆ’ ((Οˆβ€˜π‘) βˆ’ 𝑁)))
226 addsub4 11451 . . . . . . . . . . . . . . . . . . 19 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ 𝑁 ∈ β„‚) ∧ ((Οˆβ€˜π‘) ∈ β„‚ ∧ 𝑒 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) + 𝑁) βˆ’ ((Οˆβ€˜π‘) + 𝑒)) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)))
227226an42s 660 . . . . . . . . . . . . . . . . . 18 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ (Οˆβ€˜π‘) ∈ β„‚) ∧ (𝑒 ∈ β„‚ ∧ 𝑁 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) + 𝑁) βˆ’ ((Οˆβ€˜π‘) + 𝑒)) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)))
228224, 225, 2273eqtr3d 2785 . . . . . . . . . . . . . . . . 17 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ (Οˆβ€˜π‘) ∈ β„‚) ∧ (𝑒 ∈ β„‚ ∧ 𝑁 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) βˆ’ 𝑒) βˆ’ ((Οˆβ€˜π‘) βˆ’ 𝑁)) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)))
229222, 223, 163, 164, 228syl22anc 838 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ 𝑒) βˆ’ ((Οˆβ€˜π‘) βˆ’ 𝑁)) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)))
230221, 229eqtr2d 2778 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)) = ((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)))
231230fveq2d 6851 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒))) = (absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))))
232102recnd 11190 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 βˆ’ 𝑁) ∈ β„‚)
233 chpwordi 26522 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ 𝑒 ∈ ℝ ∧ 𝑁 ≀ 𝑒) β†’ (Οˆβ€˜π‘) ≀ (Οˆβ€˜π‘’))
234101, 77, 79, 233syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘) ≀ (Οˆβ€˜π‘’))
235146, 144, 234abssubge0d 15323 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) = ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)))
236101, 77, 79abssuble0d 15324 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(𝑁 βˆ’ 𝑒)) = (𝑒 βˆ’ 𝑁))
237235, 236oveq12d 7380 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) + (absβ€˜(𝑁 βˆ’ 𝑒))) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑒 βˆ’ 𝑁)))
238214, 232, 237comraddd 11376 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) + (absβ€˜(𝑁 βˆ’ 𝑒))) = ((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))))
239216, 231, 2383brtr3d 5141 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) ≀ ((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))))
240154, 212, 78, 239lediv1dd 13022 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁) ≀ (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁))
241155, 213, 150, 240leadd2dd 11777 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁)))
242150recnd 11190 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) ∈ β„‚)
243148recnd 11190 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁) ∈ β„‚)
244242, 196, 243addassd 11184 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((𝑒 βˆ’ 𝑁) / 𝑁)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) / 𝑁) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁))))
24586recnd 11190 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ∈ β„‚)
246196, 245, 173adddid 11186 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 1)))
247196mulid1d 11179 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 1) = ((𝑒 βˆ’ 𝑁) / 𝑁))
248247oveq2d 7378 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 1)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((𝑒 βˆ’ 𝑁) / 𝑁)))
249246, 248eqtrd 2777 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((𝑒 βˆ’ 𝑁) / 𝑁)))
250249oveq1d 7377 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) = (((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((𝑒 βˆ’ 𝑁) / 𝑁)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)))
251232, 214, 164, 165divdird 11976 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁) = (((𝑒 βˆ’ 𝑁) / 𝑁) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)))
252251oveq2d 7378 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) / 𝑁) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁))))
253244, 250, 2523eqtr4d 2787 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁)))
254241, 253breqtrrd 5138 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)))
25593, 156, 149, 211, 254letrd 11319 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)))
256 remulcl 11143 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ ((𝑒 βˆ’ 𝑁) / 𝑁) ∈ ℝ) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) ∈ ℝ)
25719, 103, 256sylancr 588 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) ∈ ℝ)
258257, 138readdcld 11191 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘))) ∈ ℝ)
259 remulcl 11143 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ (𝑒 βˆ’ 𝑁) ∈ ℝ) β†’ (2 Β· (𝑒 βˆ’ 𝑁)) ∈ ℝ)
26019, 102, 259sylancr 588 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· (𝑒 βˆ’ 𝑁)) ∈ ℝ)
261101, 137rerpdivcld 12995 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 / (logβ€˜π‘)) ∈ ℝ)
262110, 261remulcld 11192 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) ∈ ℝ)
263260, 262readdcld 11191 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) ∈ ℝ)
264 fveq2 6847 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑒 β†’ (Οˆβ€˜π‘¦) = (Οˆβ€˜π‘’))
265264oveq1d 7377 . . . . . . . . . . . . . . 15 (𝑦 = 𝑒 β†’ ((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) = ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)))
266 oveq1 7369 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑒 β†’ (𝑦 βˆ’ 𝑁) = (𝑒 βˆ’ 𝑁))
267266oveq2d 7378 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑒 β†’ (2 Β· (𝑦 βˆ’ 𝑁)) = (2 Β· (𝑒 βˆ’ 𝑁)))
268267oveq1d 7377 . . . . . . . . . . . . . . 15 (𝑦 = 𝑒 β†’ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) = ((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))))
269265, 268breq12d 5123 . . . . . . . . . . . . . 14 (𝑦 = 𝑒 β†’ (((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) ↔ ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘))))))
270 id 22 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑁 β†’ π‘₯ = 𝑁)
271 oveq2 7370 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑁 β†’ (2 Β· π‘₯) = (2 Β· 𝑁))
272270, 271oveq12d 7380 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑁 β†’ (π‘₯[,](2 Β· π‘₯)) = (𝑁[,](2 Β· 𝑁)))
273 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑁 β†’ (Οˆβ€˜π‘₯) = (Οˆβ€˜π‘))
274273oveq2d 7378 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑁 β†’ ((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) = ((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)))
275 oveq2 7370 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑁 β†’ (𝑦 βˆ’ π‘₯) = (𝑦 βˆ’ 𝑁))
276275oveq2d 7378 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑁 β†’ (2 Β· (𝑦 βˆ’ π‘₯)) = (2 Β· (𝑦 βˆ’ 𝑁)))
277 fveq2 6847 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑁 β†’ (logβ€˜π‘₯) = (logβ€˜π‘))
278270, 277oveq12d 7380 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑁 β†’ (π‘₯ / (logβ€˜π‘₯)) = (𝑁 / (logβ€˜π‘)))
279278oveq2d 7378 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑁 β†’ (𝑇 Β· (π‘₯ / (logβ€˜π‘₯))) = (𝑇 Β· (𝑁 / (logβ€˜π‘))))
280276, 279oveq12d 7380 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑁 β†’ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))) = ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))))
281274, 280breq12d 5123 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑁 β†’ (((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))) ↔ ((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘))))))
282272, 281raleqbidv 3322 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑁 β†’ (βˆ€π‘¦ ∈ (π‘₯[,](2 Β· π‘₯))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))) ↔ βˆ€π‘¦ ∈ (𝑁[,](2 Β· 𝑁))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘))))))
283 pntibndlem2.6 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆ€π‘₯ ∈ (1(,)+∞)βˆ€π‘¦ ∈ (π‘₯[,](2 Β· π‘₯))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))))
284283adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ βˆ€π‘₯ ∈ (1(,)+∞)βˆ€π‘¦ ∈ (π‘₯[,](2 Β· π‘₯))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))))
285 1xr 11221 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ*
286 elioopnf 13367 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ* β†’ (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁)))
287285, 286ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁))
288101, 136, 287sylanbrc 584 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ∈ (1(,)+∞))
289282, 284, 288rspcdva 3585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ βˆ€π‘¦ ∈ (𝑁[,](2 Β· 𝑁))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))))
29018adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) ∈ ℝ)
29121adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· 𝑁) ∈ ℝ)
29276simp3d 1145 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ≀ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁))
293 ltle 11250 . . . . . . . . . . . . . . . . . . . 20 (((1 + (𝐿 Β· 𝐸)) ∈ ℝ ∧ 2 ∈ ℝ) β†’ ((1 + (𝐿 Β· 𝐸)) < 2 β†’ (1 + (𝐿 Β· 𝐸)) ≀ 2))
29416, 19, 293sylancl 587 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((1 + (𝐿 Β· 𝐸)) < 2 β†’ (1 + (𝐿 Β· 𝐸)) ≀ 2))
29561, 294mpd 15 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (1 + (𝐿 Β· 𝐸)) ≀ 2)
296295adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 + (𝐿 Β· 𝐸)) ≀ 2)
29716adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 + (𝐿 Β· 𝐸)) ∈ ℝ)
29819a1i 11 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 2 ∈ ℝ)
299297, 298, 78lemul1d 13007 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((1 + (𝐿 Β· 𝐸)) ≀ 2 ↔ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) ≀ (2 Β· 𝑁)))
300296, 299mpbid 231 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) ≀ (2 Β· 𝑁))
30177, 290, 291, 292, 300letrd 11319 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ≀ (2 Β· 𝑁))
302 elicc2 13336 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℝ ∧ (2 Β· 𝑁) ∈ ℝ) β†’ (𝑒 ∈ (𝑁[,](2 Β· 𝑁)) ↔ (𝑒 ∈ ℝ ∧ 𝑁 ≀ 𝑒 ∧ 𝑒 ≀ (2 Β· 𝑁))))
303101, 291, 302syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 ∈ (𝑁[,](2 Β· 𝑁)) ↔ (𝑒 ∈ ℝ ∧ 𝑁 ≀ 𝑒 ∧ 𝑒 ≀ (2 Β· 𝑁))))
30477, 79, 301, 303mpbir3and 1343 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ∈ (𝑁[,](2 Β· 𝑁)))
305269, 289, 304rspcdva 3585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))))
306147, 263, 78, 305lediv1dd 13022 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁) ≀ (((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) / 𝑁))
307260recnd 11190 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· (𝑒 βˆ’ 𝑁)) ∈ β„‚)
308108adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑇 ∈ ℝ+)
309308rpred 12964 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑇 ∈ ℝ)
310309, 261remulcld 11192 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) ∈ ℝ)
311310recnd 11190 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) ∈ β„‚)
312 divdir 11845 . . . . . . . . . . . . . 14 (((2 Β· (𝑒 βˆ’ 𝑁)) ∈ β„‚ ∧ (𝑇 Β· (𝑁 / (logβ€˜π‘))) ∈ β„‚ ∧ (𝑁 ∈ β„‚ ∧ 𝑁 β‰  0)) β†’ (((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) / 𝑁) = (((2 Β· (𝑒 βˆ’ 𝑁)) / 𝑁) + ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁)))
313307, 311, 176, 312syl3anc 1372 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) / 𝑁) = (((2 Β· (𝑒 βˆ’ 𝑁)) / 𝑁) + ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁)))
314 2cnd 12238 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 2 ∈ β„‚)
315314, 232, 164, 165divassd 11973 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((2 Β· (𝑒 βˆ’ 𝑁)) / 𝑁) = (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)))
316110recnd 11190 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑇 ∈ β„‚)
317137rpcnne0d 12973 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((logβ€˜π‘) ∈ β„‚ ∧ (logβ€˜π‘) β‰  0))
318 div12 11842 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ β„‚ ∧ 𝑁 ∈ β„‚ ∧ ((logβ€˜π‘) ∈ β„‚ ∧ (logβ€˜π‘) β‰  0)) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) = (𝑁 Β· (𝑇 / (logβ€˜π‘))))
319316, 164, 317, 318syl3anc 1372 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) = (𝑁 Β· (𝑇 / (logβ€˜π‘))))
320319oveq1d 7377 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁) = ((𝑁 Β· (𝑇 / (logβ€˜π‘))) / 𝑁))
321308, 137rpdivcld 12981 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ∈ ℝ+)
322321rpcnd 12966 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ∈ β„‚)
323322, 164, 165divcan3d 11943 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑁 Β· (𝑇 / (logβ€˜π‘))) / 𝑁) = (𝑇 / (logβ€˜π‘)))
324320, 323eqtrd 2777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁) = (𝑇 / (logβ€˜π‘)))
325315, 324oveq12d 7380 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((2 Β· (𝑒 βˆ’ 𝑁)) / 𝑁) + ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁)) = ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘))))
326313, 325eqtrd 2777 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) / 𝑁) = ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘))))
327306, 326breqtrd 5136 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁) ≀ ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘))))
328148, 258, 142, 327leadd2dd 11777 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘)))))
329142recnd 11190 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) ∈ β„‚)
330257recnd 11190 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) ∈ β„‚)
331138recnd 11190 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ∈ β„‚)
332329, 330, 331addassd 11184 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁))) + (𝑇 / (logβ€˜π‘))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘)))))
333 2cn 12235 . . . . . . . . . . . . . . 15 2 ∈ β„‚
334 mulcom 11144 . . . . . . . . . . . . . . 15 ((2 ∈ β„‚ ∧ ((𝑒 βˆ’ 𝑁) / 𝑁) ∈ β„‚) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 2))
335333, 196, 334sylancr 588 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 2))
336335oveq2d 7378 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 2)))
337141recnd 11190 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) ∈ β„‚)
338196, 337, 314adddid 11186 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) + 2)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 2)))
339245, 173, 314addassd 11184 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) + 2) = ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + (1 + 2)))
340 1p2e3 12303 . . . . . . . . . . . . . . . 16 (1 + 2) = 3
341340oveq2i 7373 . . . . . . . . . . . . . . 15 ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + (1 + 2)) = ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)
342339, 341eqtrdi 2793 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) + 2) = ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3))
343342oveq2d 7378 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) + 2)) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)))
344336, 338, 3433eqtr2d 2783 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁))) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)))
345344oveq1d 7377 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁))) + (𝑇 / (logβ€˜π‘))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))))
346332, 345eqtr3d 2779 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘)))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))))
347328, 346breqtrd 5136 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))))
34893, 149, 139, 255, 347letrd 11319 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))))
349100rehalfcld 12407 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 2) / 2) ∈ ℝ)
35077, 297, 78ledivmul2d 13018 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 / 𝑁) ≀ (1 + (𝐿 Β· 𝐸)) ↔ 𝑒 ≀ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁)))
351292, 350mpbird 257 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 / 𝑁) ≀ (1 + (𝐿 Β· 𝐸)))
352 ax-1cn 11116 . . . . . . . . . . . . . . . 16 1 ∈ β„‚
35315adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐿 Β· 𝐸) ∈ ℝ)
354353recnd 11190 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐿 Β· 𝐸) ∈ β„‚)
355 addcom 11348 . . . . . . . . . . . . . . . 16 ((1 ∈ β„‚ ∧ (𝐿 Β· 𝐸) ∈ β„‚) β†’ (1 + (𝐿 Β· 𝐸)) = ((𝐿 Β· 𝐸) + 1))
356352, 354, 355sylancr 588 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 + (𝐿 Β· 𝐸)) = ((𝐿 Β· 𝐸) + 1))
357351, 356breqtrd 5136 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 / 𝑁) ≀ ((𝐿 Β· 𝐸) + 1))
358171, 111, 353lesubaddd 11759 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 / 𝑁) βˆ’ 1) ≀ (𝐿 Β· 𝐸) ↔ (𝑒 / 𝑁) ≀ ((𝐿 Β· 𝐸) + 1)))
359357, 358mpbird 257 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 / 𝑁) βˆ’ 1) ≀ (𝐿 Β· 𝐸))
360169, 359eqbrtrd 5132 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) ≀ (𝐿 Β· 𝐸))
3619adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐴 ∈ ℝ+)
362361rpred 12964 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐴 ∈ ℝ)
363 fveq2 6847 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑒 β†’ (π‘…β€˜π‘₯) = (π‘…β€˜π‘’))
364 id 22 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑒 β†’ π‘₯ = 𝑒)
365363, 364oveq12d 7380 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑒 β†’ ((π‘…β€˜π‘₯) / π‘₯) = ((π‘…β€˜π‘’) / 𝑒))
366365fveq2d 6851 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑒 β†’ (absβ€˜((π‘…β€˜π‘₯) / π‘₯)) = (absβ€˜((π‘…β€˜π‘’) / 𝑒)))
367366breq1d 5120 . . . . . . . . . . . . . 14 (π‘₯ = 𝑒 β†’ ((absβ€˜((π‘…β€˜π‘₯) / π‘₯)) ≀ 𝐴 ↔ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐴))
36874adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ βˆ€π‘₯ ∈ ℝ+ (absβ€˜((π‘…β€˜π‘₯) / π‘₯)) ≀ 𝐴)
369367, 368, 80rspcdva 3585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐴)
37086, 362, 105, 369leadd1dd 11776 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ≀ (𝐴 + 3))
371103, 200jca 513 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) ∈ ℝ ∧ 0 ≀ ((𝑒 βˆ’ 𝑁) / 𝑁)))
372 3rp 12928 . . . . . . . . . . . . . . 15 3 ∈ ℝ+
373 rpaddcl 12944 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ+ ∧ 3 ∈ ℝ+) β†’ (𝐴 + 3) ∈ ℝ+)
374361, 372, 373sylancl 587 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐴 + 3) ∈ ℝ+)
375374rprege0d 12971 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐴 + 3) ∈ ℝ ∧ 0 ≀ (𝐴 + 3)))
376 lemul12b 12019 . . . . . . . . . . . . 13 ((((((𝑒 βˆ’ 𝑁) / 𝑁) ∈ ℝ ∧ 0 ≀ ((𝑒 βˆ’ 𝑁) / 𝑁)) ∧ (𝐿 Β· 𝐸) ∈ ℝ) ∧ (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ∈ ℝ ∧ ((𝐴 + 3) ∈ ℝ ∧ 0 ≀ (𝐴 + 3)))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) ≀ (𝐿 Β· 𝐸) ∧ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ≀ (𝐴 + 3)) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ≀ ((𝐿 Β· 𝐸) Β· (𝐴 + 3))))
377371, 353, 106, 375, 376syl22anc 838 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) ≀ (𝐿 Β· 𝐸) ∧ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ≀ (𝐴 + 3)) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ≀ ((𝐿 Β· 𝐸) Β· (𝐴 + 3))))
378360, 370, 377mp2and 698 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ≀ ((𝐿 Β· 𝐸) Β· (𝐴 + 3)))
37935adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐸 ∈ ℝ+)
380112, 113mp1i 13 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 4 ∈ ℝ+)
381379, 380rpdivcld 12981 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 4) ∈ ℝ+)
382381rpcnd 12966 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 4) ∈ β„‚)
383374rpcnd 12966 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐴 + 3) ∈ β„‚)
384374rpne0d 12969 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐴 + 3) β‰  0)
385382, 383, 384divcan1d 11939 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝐸 / 4) / (𝐴 + 3)) Β· (𝐴 + 3)) = (𝐸 / 4))
38614recnd 11190 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐸 ∈ β„‚)
387386adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐸 ∈ β„‚)
388380rpcnd 12966 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 4 ∈ β„‚)
389380rpne0d 12969 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 4 β‰  0)
390387, 388, 389divrec2d 11942 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 4) = ((1 / 4) Β· 𝐸))
391390oveq1d 7377 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 4) / (𝐴 + 3)) = (((1 / 4) Β· 𝐸) / (𝐴 + 3)))
392 4cn 12245 . . . . . . . . . . . . . . . . . 18 4 ∈ β„‚
393 4ne0 12268 . . . . . . . . . . . . . . . . . 18 4 β‰  0
394392, 393reccli 11892 . . . . . . . . . . . . . . . . 17 (1 / 4) ∈ β„‚
395394a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 / 4) ∈ β„‚)
396395, 387, 383, 384div23d 11975 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((1 / 4) Β· 𝐸) / (𝐴 + 3)) = (((1 / 4) / (𝐴 + 3)) Β· 𝐸))
39710oveq1i 7372 . . . . . . . . . . . . . . 15 (𝐿 Β· 𝐸) = (((1 / 4) / (𝐴 + 3)) Β· 𝐸)
398396, 397eqtr4di 2795 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((1 / 4) Β· 𝐸) / (𝐴 + 3)) = (𝐿 Β· 𝐸))
399391, 398eqtr2d 2778 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐿 Β· 𝐸) = ((𝐸 / 4) / (𝐴 + 3)))
400399oveq1d 7377 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐿 Β· 𝐸) Β· (𝐴 + 3)) = (((𝐸 / 4) / (𝐴 + 3)) Β· (𝐴 + 3)))
401 2ne0 12264 . . . . . . . . . . . . . . 15 2 β‰  0
402401a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 2 β‰  0)
403387, 314, 314, 402, 402divdiv1d 11969 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 2) / 2) = (𝐸 / (2 Β· 2)))
404 2t2e4 12324 . . . . . . . . . . . . . 14 (2 Β· 2) = 4
405404oveq2i 7373 . . . . . . . . . . . . 13 (𝐸 / (2 Β· 2)) = (𝐸 / 4)
406403, 405eqtrdi 2793 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 2) / 2) = (𝐸 / 4))
407385, 400, 4063eqtr4d 2787 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐿 Β· 𝐸) Β· (𝐴 + 3)) = ((𝐸 / 2) / 2))
408378, 407breqtrd 5136 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ≀ ((𝐸 / 2) / 2))
409117adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (𝐸 / 4)) ∈ ℝ)
410137rpred 12964 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (logβ€˜π‘) ∈ ℝ)
41178reeflogd 25995 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (expβ€˜(logβ€˜π‘)) = 𝑁)
412135, 411breqtrrd 5138 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < (expβ€˜(logβ€˜π‘)))
413 eflt 16006 . . . . . . . . . . . . . . 15 (((𝑇 / (𝐸 / 4)) ∈ ℝ ∧ (logβ€˜π‘) ∈ ℝ) β†’ ((𝑇 / (𝐸 / 4)) < (logβ€˜π‘) ↔ (expβ€˜(𝑇 / (𝐸 / 4))) < (expβ€˜(logβ€˜π‘))))
414409, 410, 413syl2anc 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑇 / (𝐸 / 4)) < (logβ€˜π‘) ↔ (expβ€˜(𝑇 / (𝐸 / 4))) < (expβ€˜(logβ€˜π‘))))
415412, 414mpbird 257 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (𝐸 / 4)) < (logβ€˜π‘))
416409, 410, 415ltled 11310 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (𝐸 / 4)) ≀ (logβ€˜π‘))
417110, 381, 137, 416lediv23d 13032 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ≀ (𝐸 / 4))
418417, 406breqtrrd 5138 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ≀ ((𝐸 / 2) / 2))
419107, 138, 349, 349, 408, 418le2addd 11781 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))) ≀ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)))
420100recnd 11190 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 2) ∈ β„‚)
4214202halvesd 12406 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)) = (𝐸 / 2))
422419, 421breqtrd 5136 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))) ≀ (𝐸 / 2))
42393, 139, 100, 348, 422letrd 11319 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ≀ (𝐸 / 2))
4243simprd 497 . . . . . . . 8 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ≀ (𝐸 / 2))
425424adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ≀ (𝐸 / 2))
42693, 94, 100, 100, 423, 425le2addd 11781 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁))) ≀ ((𝐸 / 2) + (𝐸 / 2)))
4273872halvesd 12406 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
428426, 427breqtrd 5136 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁))) ≀ 𝐸)
42986, 95, 96, 99, 428letrd 11319 . . . 4 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸)
430429ralrimiva 3144 . . 3 (πœ‘ β†’ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸)
4315, 73, 430jca31 516 . 2 (πœ‘ β†’ ((π‘Œ < 𝑁 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
432 breq2 5114 . . . . 5 (𝑧 = 𝑁 β†’ (π‘Œ < 𝑧 ↔ π‘Œ < 𝑁))
433 oveq2 7370 . . . . . 6 (𝑧 = 𝑁 β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) = ((1 + (𝐿 Β· 𝐸)) Β· 𝑁))
434433breq1d 5120 . . . . 5 (𝑧 = 𝑁 β†’ (((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ) ↔ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ)))
435432, 434anbi12d 632 . . . 4 (𝑧 = 𝑁 β†’ ((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ↔ (π‘Œ < 𝑁 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ))))
436 id 22 . . . . . 6 (𝑧 = 𝑁 β†’ 𝑧 = 𝑁)
437436, 433oveq12d 7380 . . . . 5 (𝑧 = 𝑁 β†’ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧)) = (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁)))
438437raleqdv 3316 . . . 4 (𝑧 = 𝑁 β†’ (βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸 ↔ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
439435, 438anbi12d 632 . . 3 (𝑧 = 𝑁 β†’ (((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸) ↔ ((π‘Œ < 𝑁 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸)))
440439rspcev 3584 . 2 ((𝑁 ∈ ℝ+ ∧ ((π‘Œ < 𝑁 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸)) β†’ βˆƒπ‘§ ∈ ℝ+ ((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
4412, 431, 440syl2anc 585 1 (πœ‘ β†’ βˆƒπ‘§ ∈ ℝ+ ((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074   βŠ† wss 3915   class class class wbr 5110   ↦ cmpt 5193  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  -cneg 11393   / cdiv 11819  β„•cn 12160  2c2 12215  3c3 12216  4c4 12217  β„+crp 12922  (,)cioo 13271  [,)cico 13273  [,]cicc 13274  abscabs 15126  expce 15951  logclog 25926  Οˆcchp 26458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-pi 15962  df-dvds 16144  df-gcd 16382  df-prm 16555  df-pc 16716  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-vma 26463  df-chp 26464
This theorem is referenced by:  pntibndlem3  26956
  Copyright terms: Public domain W3C validator