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

Theorem pntibndlem2 27440
Description: Lemma for pntibnd 27442. 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 13011 . 2 (πœ‘ β†’ 𝑁 ∈ ℝ+)
3 pntibndlem2.11 . . . . 5 (πœ‘ β†’ ((π‘Œ < 𝑁 ∧ 𝑁 ≀ ((𝑀 / 2) Β· π‘Œ)) ∧ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ≀ (𝐸 / 2)))
43simpld 494 . . . 4 (πœ‘ β†’ (π‘Œ < 𝑁 ∧ 𝑁 ≀ ((𝑀 / 2) Β· π‘Œ)))
54simpld 494 . . 3 (πœ‘ β†’ π‘Œ < 𝑁)
6 1red 11212 . . . . . 6 (πœ‘ β†’ 1 ∈ ℝ)
7 ioossre 13382 . . . . . . . 8 (0(,)1) βŠ† ℝ
8 pntibnd.r . . . . . . . . 9 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
9 pntibndlem1.1 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ ℝ+)
10 pntibndlem1.l . . . . . . . . 9 𝐿 = ((1 / 4) / (𝐴 + 3))
118, 9, 10pntibndlem1 27438 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ (0(,)1))
127, 11sselid 3972 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ ℝ)
13 pntibndlem3.4 . . . . . . . 8 (πœ‘ β†’ 𝐸 ∈ (0(,)1))
147, 13sselid 3972 . . . . . . 7 (πœ‘ β†’ 𝐸 ∈ ℝ)
1512, 14remulcld 11241 . . . . . 6 (πœ‘ β†’ (𝐿 Β· 𝐸) ∈ ℝ)
166, 15readdcld 11240 . . . . 5 (πœ‘ β†’ (1 + (𝐿 Β· 𝐸)) ∈ ℝ)
171nnred 12224 . . . . 5 (πœ‘ β†’ 𝑁 ∈ ℝ)
1816, 17remulcld 11241 . . . 4 (πœ‘ β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) ∈ ℝ)
19 2re 12283 . . . . 5 2 ∈ ℝ
20 remulcl 11191 . . . . 5 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ (2 Β· 𝑁) ∈ ℝ)
2119, 17, 20sylancr 586 . . . 4 (πœ‘ β†’ (2 Β· 𝑁) ∈ ℝ)
22 pntibndlem3.c . . . . . . . . . 10 𝐢 = ((2 Β· 𝐡) + (logβ€˜2))
23 pntibndlem3.3 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ ℝ+)
2423rpred 13013 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ ℝ)
25 remulcl 11191 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (2 Β· 𝐡) ∈ ℝ)
2619, 24, 25sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ (2 Β· 𝐡) ∈ ℝ)
27 2rp 12976 . . . . . . . . . . . . 13 2 ∈ ℝ+
2827a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 2 ∈ ℝ+)
2928relogcld 26473 . . . . . . . . . . 11 (πœ‘ β†’ (logβ€˜2) ∈ ℝ)
3026, 29readdcld 11240 . . . . . . . . . 10 (πœ‘ β†’ ((2 Β· 𝐡) + (logβ€˜2)) ∈ ℝ)
3122, 30eqeltrid 2829 . . . . . . . . 9 (πœ‘ β†’ 𝐢 ∈ ℝ)
32 eliooord 13380 . . . . . . . . . . . 12 (𝐸 ∈ (0(,)1) β†’ (0 < 𝐸 ∧ 𝐸 < 1))
3313, 32syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (0 < 𝐸 ∧ 𝐸 < 1))
3433simpld 494 . . . . . . . . . 10 (πœ‘ β†’ 0 < 𝐸)
3514, 34elrpd 13010 . . . . . . . . 9 (πœ‘ β†’ 𝐸 ∈ ℝ+)
3631, 35rerpdivcld 13044 . . . . . . . 8 (πœ‘ β†’ (𝐢 / 𝐸) ∈ ℝ)
3736reefcld 16028 . . . . . . 7 (πœ‘ β†’ (expβ€˜(𝐢 / 𝐸)) ∈ ℝ)
38 pnfxr 11265 . . . . . . 7 +∞ ∈ ℝ*
39 icossre 13402 . . . . . . 7 (((expβ€˜(𝐢 / 𝐸)) ∈ ℝ ∧ +∞ ∈ ℝ*) β†’ ((expβ€˜(𝐢 / 𝐸))[,)+∞) βŠ† ℝ)
4037, 38, 39sylancl 585 . . . . . 6 (πœ‘ β†’ ((expβ€˜(𝐢 / 𝐸))[,)+∞) βŠ† ℝ)
41 pntibndlem2.8 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ ((expβ€˜(𝐢 / 𝐸))[,)+∞))
4240, 41sseldd 3975 . . . . 5 (πœ‘ β†’ 𝑀 ∈ ℝ)
43 ioossre 13382 . . . . . 6 (𝑋(,)+∞) βŠ† ℝ
44 pntibndlem2.9 . . . . . 6 (πœ‘ β†’ π‘Œ ∈ (𝑋(,)+∞))
4543, 44sselid 3972 . . . . 5 (πœ‘ β†’ π‘Œ ∈ ℝ)
4642, 45remulcld 11241 . . . 4 (πœ‘ β†’ (𝑀 Β· π‘Œ) ∈ ℝ)
4719a1i 11 . . . . 5 (πœ‘ β†’ 2 ∈ ℝ)
48 eliooord 13380 . . . . . . . . . . . . 13 (𝐿 ∈ (0(,)1) β†’ (0 < 𝐿 ∧ 𝐿 < 1))
4911, 48syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (0 < 𝐿 ∧ 𝐿 < 1))
5049simpld 494 . . . . . . . . . . 11 (πœ‘ β†’ 0 < 𝐿)
5112, 50elrpd 13010 . . . . . . . . . 10 (πœ‘ β†’ 𝐿 ∈ ℝ+)
5251rpge0d 13017 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ 𝐿)
5349simprd 495 . . . . . . . . 9 (πœ‘ β†’ 𝐿 < 1)
5435rpge0d 13017 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ 𝐸)
5533simprd 495 . . . . . . . . 9 (πœ‘ β†’ 𝐸 < 1)
5612, 6, 14, 6, 52, 53, 54, 55ltmul12ad 12152 . . . . . . . 8 (πœ‘ β†’ (𝐿 Β· 𝐸) < (1 Β· 1))
57 1t1e1 12371 . . . . . . . 8 (1 Β· 1) = 1
5856, 57breqtrdi 5179 . . . . . . 7 (πœ‘ β†’ (𝐿 Β· 𝐸) < 1)
5915, 6, 6, 58ltadd2dd 11370 . . . . . 6 (πœ‘ β†’ (1 + (𝐿 Β· 𝐸)) < (1 + 1))
60 df-2 12272 . . . . . 6 2 = (1 + 1)
6159, 60breqtrrdi 5180 . . . . 5 (πœ‘ β†’ (1 + (𝐿 Β· 𝐸)) < 2)
6216, 47, 2, 61ltmul1dd 13068 . . . 4 (πœ‘ β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (2 Β· 𝑁))
634simprd 495 . . . . . 6 (πœ‘ β†’ 𝑁 ≀ ((𝑀 / 2) Β· π‘Œ))
6442recnd 11239 . . . . . . 7 (πœ‘ β†’ 𝑀 ∈ β„‚)
6545recnd 11239 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ β„‚)
66 rpcnne0 12989 . . . . . . . 8 (2 ∈ ℝ+ β†’ (2 ∈ β„‚ ∧ 2 β‰  0))
6727, 66mp1i 13 . . . . . . 7 (πœ‘ β†’ (2 ∈ β„‚ ∧ 2 β‰  0))
68 div23 11888 . . . . . . 7 ((𝑀 ∈ β„‚ ∧ π‘Œ ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0)) β†’ ((𝑀 Β· π‘Œ) / 2) = ((𝑀 / 2) Β· π‘Œ))
6964, 65, 67, 68syl3anc 1368 . . . . . 6 (πœ‘ β†’ ((𝑀 Β· π‘Œ) / 2) = ((𝑀 / 2) Β· π‘Œ))
7063, 69breqtrrd 5166 . . . . 5 (πœ‘ β†’ 𝑁 ≀ ((𝑀 Β· π‘Œ) / 2))
7117, 46, 28lemuldiv2d 13063 . . . . 5 (πœ‘ β†’ ((2 Β· 𝑁) ≀ (𝑀 Β· π‘Œ) ↔ 𝑁 ≀ ((𝑀 Β· π‘Œ) / 2)))
7270, 71mpbird 257 . . . 4 (πœ‘ β†’ (2 Β· 𝑁) ≀ (𝑀 Β· π‘Œ))
7318, 21, 46, 62, 72ltletrd 11371 . . 3 (πœ‘ β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ))
74 pntibndlem3.2 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ (absβ€˜((π‘…β€˜π‘₯) / π‘₯)) ≀ 𝐴)
75 pntibndlem3.k . . . . . . . . . . . 12 𝐾 = (expβ€˜(𝐡 / (𝐸 / 2)))
768, 9, 10, 74, 23, 75, 22, 13, 9, 1pntibndlem2a 27439 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 ∈ ℝ ∧ 𝑁 ≀ 𝑒 ∧ 𝑒 ≀ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁)))
7776simp1d 1139 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ∈ ℝ)
782adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ∈ ℝ+)
7976simp2d 1140 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ≀ 𝑒)
8077, 78, 79rpgecld 13052 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ∈ ℝ+)
818pntrf 27412 . . . . . . . . . 10 𝑅:ℝ+βŸΆβ„
8281ffvelcdmi 7075 . . . . . . . . 9 (𝑒 ∈ ℝ+ β†’ (π‘…β€˜π‘’) ∈ ℝ)
8380, 82syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘’) ∈ ℝ)
8483, 80rerpdivcld 13044 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) / 𝑒) ∈ ℝ)
8584recnd 11239 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) / 𝑒) ∈ β„‚)
8685abscld 15380 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ∈ ℝ)
8781ffvelcdmi 7075 . . . . . . . . . . . 12 (𝑁 ∈ ℝ+ β†’ (π‘…β€˜π‘) ∈ ℝ)
882, 87syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (π‘…β€˜π‘) ∈ ℝ)
8988, 1nndivred 12263 . . . . . . . . . 10 (πœ‘ β†’ ((π‘…β€˜π‘) / 𝑁) ∈ ℝ)
9089adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘) / 𝑁) ∈ ℝ)
9190recnd 11239 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘) / 𝑁) ∈ β„‚)
9285, 91subcld 11568 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁)) ∈ β„‚)
9392abscld 15380 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ∈ ℝ)
9491abscld 15380 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ∈ ℝ)
9593, 94readdcld 11240 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁))) ∈ ℝ)
9614adantr 480 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐸 ∈ ℝ)
9785, 91abs2difd 15401 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) βˆ’ (absβ€˜((π‘…β€˜π‘) / 𝑁))) ≀ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))))
9886, 94, 93lesubaddd 11808 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) βˆ’ (absβ€˜((π‘…β€˜π‘) / 𝑁))) ≀ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ↔ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁)))))
9997, 98mpbid 231 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁))))
10096rehalfcld 12456 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 2) ∈ ℝ)
10117adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ∈ ℝ)
10277, 101resubcld 11639 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 βˆ’ 𝑁) ∈ ℝ)
103102, 78rerpdivcld 13044 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) ∈ ℝ)
104 3re 12289 . . . . . . . . . . . 12 3 ∈ ℝ
105104a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 3 ∈ ℝ)
10686, 105readdcld 11240 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ∈ ℝ)
107103, 106remulcld 11241 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ∈ ℝ)
108 pntibndlem2.5 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 ∈ ℝ+)
109108rpred 13013 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ ℝ)
110109adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑇 ∈ ℝ)
111 1red 11212 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 1 ∈ ℝ)
112 4nn 12292 . . . . . . . . . . . . . . . . . 18 4 ∈ β„•
113 nnrp 12982 . . . . . . . . . . . . . . . . . 18 (4 ∈ β„• β†’ 4 ∈ ℝ+)
114112, 113mp1i 13 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 4 ∈ ℝ+)
11535, 114rpdivcld 13030 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐸 / 4) ∈ ℝ+)
116108, 115rpdivcld 13030 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑇 / (𝐸 / 4)) ∈ ℝ+)
117116rpred 13013 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑇 / (𝐸 / 4)) ∈ ℝ)
118117reefcld 16028 . . . . . . . . . . . . 13 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) ∈ ℝ)
119118adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (expβ€˜(𝑇 / (𝐸 / 4))) ∈ ℝ)
120 efgt1 16056 . . . . . . . . . . . . . 14 ((𝑇 / (𝐸 / 4)) ∈ ℝ+ β†’ 1 < (expβ€˜(𝑇 / (𝐸 / 4))))
121116, 120syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 1 < (expβ€˜(𝑇 / (𝐸 / 4))))
122121adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 1 < (expβ€˜(𝑇 / (𝐸 / 4))))
123 pntibndlem2.7 . . . . . . . . . . . . . . . 16 𝑋 = ((expβ€˜(𝑇 / (𝐸 / 4))) + 𝑍)
124 pntibndlem3.6 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑍 ∈ ℝ+)
125124rpred 13013 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑍 ∈ ℝ)
126118, 125readdcld 11240 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((expβ€˜(𝑇 / (𝐸 / 4))) + 𝑍) ∈ ℝ)
127123, 126eqeltrid 2829 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 ∈ ℝ)
128118, 124ltaddrpd 13046 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < ((expβ€˜(𝑇 / (𝐸 / 4))) + 𝑍))
129128, 123breqtrrdi 5180 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < 𝑋)
130 eliooord 13380 . . . . . . . . . . . . . . . . 17 (π‘Œ ∈ (𝑋(,)+∞) β†’ (𝑋 < π‘Œ ∧ π‘Œ < +∞))
13144, 130syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑋 < π‘Œ ∧ π‘Œ < +∞))
132131simpld 494 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 < π‘Œ)
133118, 127, 45, 129, 132lttrd 11372 . . . . . . . . . . . . . 14 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < π‘Œ)
134118, 45, 17, 133, 5lttrd 11372 . . . . . . . . . . . . 13 (πœ‘ β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < 𝑁)
135134adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < 𝑁)
136111, 119, 101, 122, 135lttrd 11372 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 1 < 𝑁)
137101, 136rplogcld 26479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (logβ€˜π‘) ∈ ℝ+)
138110, 137rerpdivcld 13044 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ∈ ℝ)
139107, 138readdcld 11240 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))) ∈ ℝ)
140 peano2re 11384 . . . . . . . . . . . 12 ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) ∈ ℝ β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) ∈ ℝ)
14186, 140syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) ∈ ℝ)
142103, 141remulcld 11241 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) ∈ ℝ)
143 chpcl 26972 . . . . . . . . . . . . 13 (𝑒 ∈ ℝ β†’ (Οˆβ€˜π‘’) ∈ ℝ)
14477, 143syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘’) ∈ ℝ)
145 chpcl 26972 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ β†’ (Οˆβ€˜π‘) ∈ ℝ)
146101, 145syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘) ∈ ℝ)
147144, 146resubcld 11639 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) ∈ ℝ)
148147, 78rerpdivcld 13044 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁) ∈ ℝ)
149142, 148readdcld 11240 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) ∈ ℝ)
150103, 86remulcld 11241 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) ∈ ℝ)
15188adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘) ∈ ℝ)
15283, 151resubcld 11639 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) ∈ ℝ)
153152recnd 11239 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) ∈ β„‚)
154153abscld 15380 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) ∈ ℝ)
155154, 78rerpdivcld 13044 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁) ∈ ℝ)
156150, 155readdcld 11240 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)) ∈ ℝ)
157103, 84remulcld 11241 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) ∈ ℝ)
158157renegcld 11638 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) ∈ ℝ)
159158recnd 11239 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) ∈ β„‚)
160152, 78rerpdivcld 13044 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁) ∈ ℝ)
161160recnd 11239 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁) ∈ β„‚)
162159, 161abstrid 15400 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) + (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁))) ≀ ((absβ€˜-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) + (absβ€˜(((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁))))
16377recnd 11239 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ∈ β„‚)
164101recnd 11239 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ∈ β„‚)
16578rpne0d 13018 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 β‰  0)
166163, 164, 164, 165divsubdird 12026 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) = ((𝑒 / 𝑁) βˆ’ (𝑁 / 𝑁)))
167164, 165dividd 11985 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 / 𝑁) = 1)
168167oveq2d 7417 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 / 𝑁) βˆ’ (𝑁 / 𝑁)) = ((𝑒 / 𝑁) βˆ’ 1))
169166, 168eqtrd 2764 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) = ((𝑒 / 𝑁) βˆ’ 1))
170169oveq1d 7416 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = (((𝑒 / 𝑁) βˆ’ 1) Β· ((π‘…β€˜π‘’) / 𝑒)))
17177, 78rerpdivcld 13044 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 / 𝑁) ∈ ℝ)
172171recnd 11239 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 / 𝑁) ∈ β„‚)
173 1cnd 11206 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 1 ∈ β„‚)
174172, 173, 85subdird 11668 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 / 𝑁) βˆ’ 1) Β· ((π‘…β€˜π‘’) / 𝑒)) = (((𝑒 / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) βˆ’ (1 Β· ((π‘…β€˜π‘’) / 𝑒))))
17580rpcnne0d 13022 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 ∈ β„‚ ∧ 𝑒 β‰  0))
17678rpcnne0d 13022 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 ∈ β„‚ ∧ 𝑁 β‰  0))
17783recnd 11239 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘’) ∈ β„‚)
178 dmdcan 11921 . . . . . . . . . . . . . . . . . . 19 (((𝑒 ∈ β„‚ ∧ 𝑒 β‰  0) ∧ (𝑁 ∈ β„‚ ∧ 𝑁 β‰  0) ∧ (π‘…β€˜π‘’) ∈ β„‚) β†’ ((𝑒 / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = ((π‘…β€˜π‘’) / 𝑁))
179175, 176, 177, 178syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = ((π‘…β€˜π‘’) / 𝑁))
18085mullidd 11229 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 Β· ((π‘…β€˜π‘’) / 𝑒)) = ((π‘…β€˜π‘’) / 𝑒))
181179, 180oveq12d 7419 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) βˆ’ (1 Β· ((π‘…β€˜π‘’) / 𝑒))) = (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘’) / 𝑒)))
182170, 174, 1813eqtrd 2768 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘’) / 𝑒)))
183182negeqd 11451 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = -(((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘’) / 𝑒)))
18483, 78rerpdivcld 13044 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) / 𝑁) ∈ ℝ)
185184recnd 11239 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) / 𝑁) ∈ β„‚)
186185, 85negsubdi2d 11584 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘’) / 𝑒)) = (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘’) / 𝑁)))
187183, 186eqtrd 2764 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ -(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) = (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘’) / 𝑁)))
188151recnd 11239 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘) ∈ β„‚)
189177, 188, 164, 165divsubdird 12026 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁) = (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘) / 𝑁)))
190187, 189oveq12d 7419 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) + (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁)) = ((((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘’) / 𝑁)) + (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘) / 𝑁))))
19185, 185, 91npncand 11592 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘’) / 𝑁)) + (((π‘…β€˜π‘’) / 𝑁) βˆ’ ((π‘…β€˜π‘) / 𝑁))) = (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁)))
192190, 191eqtrd 2764 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) + (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁)) = (((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁)))
193192fveq2d 6885 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) + (((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁))) = (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))))
194157recnd 11239 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒)) ∈ β„‚)
195194absnegd 15393 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) = (absβ€˜(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))))
196103recnd 11239 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) ∈ β„‚)
197196, 85absmuld 15398 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) = ((absβ€˜((𝑒 βˆ’ 𝑁) / 𝑁)) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))))
19877, 101subge0d 11801 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (0 ≀ (𝑒 βˆ’ 𝑁) ↔ 𝑁 ≀ 𝑒))
19979, 198mpbird 257 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 0 ≀ (𝑒 βˆ’ 𝑁))
200102, 78, 199divge0d 13053 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 0 ≀ ((𝑒 βˆ’ 𝑁) / 𝑁))
201103, 200absidd 15366 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((𝑒 βˆ’ 𝑁) / 𝑁)) = ((𝑒 βˆ’ 𝑁) / 𝑁))
202201oveq1d 7416 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((𝑒 βˆ’ 𝑁) / 𝑁)) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))))
203195, 197, 2023eqtrd 2768 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))))
204153, 164, 165absdivd 15399 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁)) = ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / (absβ€˜π‘)))
20578rprege0d 13020 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 ∈ ℝ ∧ 0 ≀ 𝑁))
206 absid 15240 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 0 ≀ 𝑁) β†’ (absβ€˜π‘) = 𝑁)
207205, 206syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜π‘) = 𝑁)
208207oveq2d 7417 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / (absβ€˜π‘)) = ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁))
209204, 208eqtrd 2764 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁)) = ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁))
210203, 209oveq12d 7419 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜-(((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((π‘…β€˜π‘’) / 𝑒))) + (absβ€˜(((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) / 𝑁))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)))
211162, 193, 2103brtr3d 5169 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)))
212102, 147readdcld 11240 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) ∈ ℝ)
213212, 78rerpdivcld 13044 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁) ∈ ℝ)
214147recnd 11239 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) ∈ β„‚)
215164, 163subcld 11568 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 βˆ’ 𝑒) ∈ β„‚)
216214, 215abstrid 15400 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒))) ≀ ((absβ€˜((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) + (absβ€˜(𝑁 βˆ’ 𝑒))))
2178pntrval 27411 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ ℝ+ β†’ (π‘…β€˜π‘’) = ((Οˆβ€˜π‘’) βˆ’ 𝑒))
21880, 217syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘’) = ((Οˆβ€˜π‘’) βˆ’ 𝑒))
2198pntrval 27411 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℝ+ β†’ (π‘…β€˜π‘) = ((Οˆβ€˜π‘) βˆ’ 𝑁))
22078, 219syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (π‘…β€˜π‘) = ((Οˆβ€˜π‘) βˆ’ 𝑁))
221218, 220oveq12d 7419 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)) = (((Οˆβ€˜π‘’) βˆ’ 𝑒) βˆ’ ((Οˆβ€˜π‘) βˆ’ 𝑁)))
222144recnd 11239 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘’) ∈ β„‚)
223146recnd 11239 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘) ∈ β„‚)
224 subadd4 11501 . . . . . . . . . . . . . . . . . 18 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ (Οˆβ€˜π‘) ∈ β„‚) ∧ (𝑒 ∈ β„‚ ∧ 𝑁 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) βˆ’ (𝑒 βˆ’ 𝑁)) = (((Οˆβ€˜π‘’) + 𝑁) βˆ’ ((Οˆβ€˜π‘) + 𝑒)))
225 sub4 11502 . . . . . . . . . . . . . . . . . 18 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ (Οˆβ€˜π‘) ∈ β„‚) ∧ (𝑒 ∈ β„‚ ∧ 𝑁 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) βˆ’ (𝑒 βˆ’ 𝑁)) = (((Οˆβ€˜π‘’) βˆ’ 𝑒) βˆ’ ((Οˆβ€˜π‘) βˆ’ 𝑁)))
226 addsub4 11500 . . . . . . . . . . . . . . . . . . 19 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ 𝑁 ∈ β„‚) ∧ ((Οˆβ€˜π‘) ∈ β„‚ ∧ 𝑒 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) + 𝑁) βˆ’ ((Οˆβ€˜π‘) + 𝑒)) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)))
227226an42s 658 . . . . . . . . . . . . . . . . . 18 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ (Οˆβ€˜π‘) ∈ β„‚) ∧ (𝑒 ∈ β„‚ ∧ 𝑁 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) + 𝑁) βˆ’ ((Οˆβ€˜π‘) + 𝑒)) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)))
228224, 225, 2273eqtr3d 2772 . . . . . . . . . . . . . . . . 17 ((((Οˆβ€˜π‘’) ∈ β„‚ ∧ (Οˆβ€˜π‘) ∈ β„‚) ∧ (𝑒 ∈ β„‚ ∧ 𝑁 ∈ β„‚)) β†’ (((Οˆβ€˜π‘’) βˆ’ 𝑒) βˆ’ ((Οˆβ€˜π‘) βˆ’ 𝑁)) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)))
229222, 223, 163, 164, 228syl22anc 836 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ 𝑒) βˆ’ ((Οˆβ€˜π‘) βˆ’ 𝑁)) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)))
230221, 229eqtr2d 2765 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒)) = ((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘)))
231230fveq2d 6885 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑁 βˆ’ 𝑒))) = (absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))))
232102recnd 11239 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 βˆ’ 𝑁) ∈ β„‚)
233 chpwordi 27005 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ 𝑒 ∈ ℝ ∧ 𝑁 ≀ 𝑒) β†’ (Οˆβ€˜π‘) ≀ (Οˆβ€˜π‘’))
234101, 77, 79, 233syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (Οˆβ€˜π‘) ≀ (Οˆβ€˜π‘’))
235146, 144, 234abssubge0d 15375 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) = ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)))
236101, 77, 79abssuble0d 15376 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(𝑁 βˆ’ 𝑒)) = (𝑒 βˆ’ 𝑁))
237235, 236oveq12d 7419 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) + (absβ€˜(𝑁 βˆ’ 𝑒))) = (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) + (𝑒 βˆ’ 𝑁)))
238214, 232, 237comraddd 11425 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) + (absβ€˜(𝑁 βˆ’ 𝑒))) = ((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))))
239216, 231, 2383brtr3d 5169 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) ≀ ((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))))
240154, 212, 78, 239lediv1dd 13071 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁) ≀ (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁))
241155, 213, 150, 240leadd2dd 11826 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁)))
242150recnd 11239 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) ∈ β„‚)
243148recnd 11239 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁) ∈ β„‚)
244242, 196, 243addassd 11233 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((𝑒 βˆ’ 𝑁) / 𝑁)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) / 𝑁) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁))))
24586recnd 11239 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ∈ β„‚)
246196, 245, 173adddid 11235 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 1)))
247196mulridd 11228 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 1) = ((𝑒 βˆ’ 𝑁) / 𝑁))
248247oveq2d 7417 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 1)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((𝑒 βˆ’ 𝑁) / 𝑁)))
249246, 248eqtrd 2764 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((𝑒 βˆ’ 𝑁) / 𝑁)))
250249oveq1d 7416 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) = (((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((𝑒 βˆ’ 𝑁) / 𝑁)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)))
251232, 214, 164, 165divdird 12025 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁) = (((𝑒 βˆ’ 𝑁) / 𝑁) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)))
252251oveq2d 7417 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) / 𝑁) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁))))
253244, 250, 2523eqtr4d 2774 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + (((𝑒 βˆ’ 𝑁) + ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘))) / 𝑁)))
254241, 253breqtrrd 5166 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· (absβ€˜((π‘…β€˜π‘’) / 𝑒))) + ((absβ€˜((π‘…β€˜π‘’) βˆ’ (π‘…β€˜π‘))) / 𝑁)) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)))
25593, 156, 149, 211, 254letrd 11368 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)))
256 remulcl 11191 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ ((𝑒 βˆ’ 𝑁) / 𝑁) ∈ ℝ) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) ∈ ℝ)
25719, 103, 256sylancr 586 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) ∈ ℝ)
258257, 138readdcld 11240 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘))) ∈ ℝ)
259 remulcl 11191 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ (𝑒 βˆ’ 𝑁) ∈ ℝ) β†’ (2 Β· (𝑒 βˆ’ 𝑁)) ∈ ℝ)
26019, 102, 259sylancr 586 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· (𝑒 βˆ’ 𝑁)) ∈ ℝ)
261101, 137rerpdivcld 13044 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑁 / (logβ€˜π‘)) ∈ ℝ)
262110, 261remulcld 11241 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) ∈ ℝ)
263260, 262readdcld 11240 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) ∈ ℝ)
264 fveq2 6881 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑒 β†’ (Οˆβ€˜π‘¦) = (Οˆβ€˜π‘’))
265264oveq1d 7416 . . . . . . . . . . . . . . 15 (𝑦 = 𝑒 β†’ ((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) = ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)))
266 oveq1 7408 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑒 β†’ (𝑦 βˆ’ 𝑁) = (𝑒 βˆ’ 𝑁))
267266oveq2d 7417 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑒 β†’ (2 Β· (𝑦 βˆ’ 𝑁)) = (2 Β· (𝑒 βˆ’ 𝑁)))
268267oveq1d 7416 . . . . . . . . . . . . . . 15 (𝑦 = 𝑒 β†’ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) = ((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))))
269265, 268breq12d 5151 . . . . . . . . . . . . . 14 (𝑦 = 𝑒 β†’ (((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) ↔ ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘))))))
270 id 22 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑁 β†’ π‘₯ = 𝑁)
271 oveq2 7409 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑁 β†’ (2 Β· π‘₯) = (2 Β· 𝑁))
272270, 271oveq12d 7419 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑁 β†’ (π‘₯[,](2 Β· π‘₯)) = (𝑁[,](2 Β· 𝑁)))
273 fveq2 6881 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑁 β†’ (Οˆβ€˜π‘₯) = (Οˆβ€˜π‘))
274273oveq2d 7417 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑁 β†’ ((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) = ((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)))
275 oveq2 7409 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑁 β†’ (𝑦 βˆ’ π‘₯) = (𝑦 βˆ’ 𝑁))
276275oveq2d 7417 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑁 β†’ (2 Β· (𝑦 βˆ’ π‘₯)) = (2 Β· (𝑦 βˆ’ 𝑁)))
277 fveq2 6881 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑁 β†’ (logβ€˜π‘₯) = (logβ€˜π‘))
278270, 277oveq12d 7419 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑁 β†’ (π‘₯ / (logβ€˜π‘₯)) = (𝑁 / (logβ€˜π‘)))
279278oveq2d 7417 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑁 β†’ (𝑇 Β· (π‘₯ / (logβ€˜π‘₯))) = (𝑇 Β· (𝑁 / (logβ€˜π‘))))
280276, 279oveq12d 7419 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑁 β†’ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))) = ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))))
281274, 280breq12d 5151 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑁 β†’ (((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))) ↔ ((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘))))))
282272, 281raleqbidv 3334 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑁 β†’ (βˆ€π‘¦ ∈ (π‘₯[,](2 Β· π‘₯))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))) ↔ βˆ€π‘¦ ∈ (𝑁[,](2 Β· 𝑁))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘))))))
283 pntibndlem2.6 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆ€π‘₯ ∈ (1(,)+∞)βˆ€π‘¦ ∈ (π‘₯[,](2 Β· π‘₯))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))))
284283adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ βˆ€π‘₯ ∈ (1(,)+∞)βˆ€π‘¦ ∈ (π‘₯[,](2 Β· π‘₯))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘₯)) ≀ ((2 Β· (𝑦 βˆ’ π‘₯)) + (𝑇 Β· (π‘₯ / (logβ€˜π‘₯)))))
285 1xr 11270 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ*
286 elioopnf 13417 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ* β†’ (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁)))
287285, 286ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁))
288101, 136, 287sylanbrc 582 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑁 ∈ (1(,)+∞))
289282, 284, 288rspcdva 3605 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ βˆ€π‘¦ ∈ (𝑁[,](2 Β· 𝑁))((Οˆβ€˜π‘¦) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑦 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))))
29018adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) ∈ ℝ)
29121adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· 𝑁) ∈ ℝ)
29276simp3d 1141 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ≀ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁))
293 ltle 11299 . . . . . . . . . . . . . . . . . . . 20 (((1 + (𝐿 Β· 𝐸)) ∈ ℝ ∧ 2 ∈ ℝ) β†’ ((1 + (𝐿 Β· 𝐸)) < 2 β†’ (1 + (𝐿 Β· 𝐸)) ≀ 2))
29416, 19, 293sylancl 585 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((1 + (𝐿 Β· 𝐸)) < 2 β†’ (1 + (𝐿 Β· 𝐸)) ≀ 2))
29561, 294mpd 15 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (1 + (𝐿 Β· 𝐸)) ≀ 2)
296295adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 + (𝐿 Β· 𝐸)) ≀ 2)
29716adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 + (𝐿 Β· 𝐸)) ∈ ℝ)
29819a1i 11 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 2 ∈ ℝ)
299297, 298, 78lemul1d 13056 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((1 + (𝐿 Β· 𝐸)) ≀ 2 ↔ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) ≀ (2 Β· 𝑁)))
300296, 299mpbid 231 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) ≀ (2 Β· 𝑁))
30177, 290, 291, 292, 300letrd 11368 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ≀ (2 Β· 𝑁))
302 elicc2 13386 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℝ ∧ (2 Β· 𝑁) ∈ ℝ) β†’ (𝑒 ∈ (𝑁[,](2 Β· 𝑁)) ↔ (𝑒 ∈ ℝ ∧ 𝑁 ≀ 𝑒 ∧ 𝑒 ≀ (2 Β· 𝑁))))
303101, 291, 302syl2anc 583 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 ∈ (𝑁[,](2 Β· 𝑁)) ↔ (𝑒 ∈ ℝ ∧ 𝑁 ≀ 𝑒 ∧ 𝑒 ≀ (2 Β· 𝑁))))
30477, 79, 301, 303mpbir3and 1339 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑒 ∈ (𝑁[,](2 Β· 𝑁)))
305269, 289, 304rspcdva 3605 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) ≀ ((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))))
306147, 263, 78, 305lediv1dd 13071 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁) ≀ (((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) / 𝑁))
307260recnd 11239 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· (𝑒 βˆ’ 𝑁)) ∈ β„‚)
308108adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑇 ∈ ℝ+)
309308rpred 13013 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑇 ∈ ℝ)
310309, 261remulcld 11241 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) ∈ ℝ)
311310recnd 11239 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) ∈ β„‚)
312 divdir 11894 . . . . . . . . . . . . . 14 (((2 Β· (𝑒 βˆ’ 𝑁)) ∈ β„‚ ∧ (𝑇 Β· (𝑁 / (logβ€˜π‘))) ∈ β„‚ ∧ (𝑁 ∈ β„‚ ∧ 𝑁 β‰  0)) β†’ (((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) / 𝑁) = (((2 Β· (𝑒 βˆ’ 𝑁)) / 𝑁) + ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁)))
313307, 311, 176, 312syl3anc 1368 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) / 𝑁) = (((2 Β· (𝑒 βˆ’ 𝑁)) / 𝑁) + ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁)))
314 2cnd 12287 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 2 ∈ β„‚)
315314, 232, 164, 165divassd 12022 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((2 Β· (𝑒 βˆ’ 𝑁)) / 𝑁) = (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)))
316110recnd 11239 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝑇 ∈ β„‚)
317137rpcnne0d 13022 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((logβ€˜π‘) ∈ β„‚ ∧ (logβ€˜π‘) β‰  0))
318 div12 11891 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ β„‚ ∧ 𝑁 ∈ β„‚ ∧ ((logβ€˜π‘) ∈ β„‚ ∧ (logβ€˜π‘) β‰  0)) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) = (𝑁 Β· (𝑇 / (logβ€˜π‘))))
319316, 164, 317, 318syl3anc 1368 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 Β· (𝑁 / (logβ€˜π‘))) = (𝑁 Β· (𝑇 / (logβ€˜π‘))))
320319oveq1d 7416 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁) = ((𝑁 Β· (𝑇 / (logβ€˜π‘))) / 𝑁))
321308, 137rpdivcld 13030 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ∈ ℝ+)
322321rpcnd 13015 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ∈ β„‚)
323322, 164, 165divcan3d 11992 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑁 Β· (𝑇 / (logβ€˜π‘))) / 𝑁) = (𝑇 / (logβ€˜π‘)))
324320, 323eqtrd 2764 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁) = (𝑇 / (logβ€˜π‘)))
325315, 324oveq12d 7419 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((2 Β· (𝑒 βˆ’ 𝑁)) / 𝑁) + ((𝑇 Β· (𝑁 / (logβ€˜π‘))) / 𝑁)) = ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘))))
326313, 325eqtrd 2764 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((2 Β· (𝑒 βˆ’ 𝑁)) + (𝑇 Β· (𝑁 / (logβ€˜π‘)))) / 𝑁) = ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘))))
327306, 326breqtrd 5164 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁) ≀ ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘))))
328148, 258, 142, 327leadd2dd 11826 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘)))))
329142recnd 11239 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) ∈ β„‚)
330257recnd 11239 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) ∈ β„‚)
331138recnd 11239 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ∈ β„‚)
332329, 330, 331addassd 11233 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁))) + (𝑇 / (logβ€˜π‘))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘)))))
333 2cn 12284 . . . . . . . . . . . . . . 15 2 ∈ β„‚
334 mulcom 11192 . . . . . . . . . . . . . . 15 ((2 ∈ β„‚ ∧ ((𝑒 βˆ’ 𝑁) / 𝑁) ∈ β„‚) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 2))
335333, 196, 334sylancr 586 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 2))
336335oveq2d 7417 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 2)))
337141recnd 11239 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) ∈ β„‚)
338196, 337, 314adddid 11235 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) + 2)) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((𝑒 βˆ’ 𝑁) / 𝑁) Β· 2)))
339245, 173, 314addassd 11233 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) + 2) = ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + (1 + 2)))
340 1p2e3 12352 . . . . . . . . . . . . . . . 16 (1 + 2) = 3
341340oveq2i 7412 . . . . . . . . . . . . . . 15 ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + (1 + 2)) = ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)
342339, 341eqtrdi 2780 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) + 2) = ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3))
343342oveq2d 7417 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1) + 2)) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)))
344336, 338, 3433eqtr2d 2770 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁))) = (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)))
345344oveq1d 7416 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁))) + (𝑇 / (logβ€˜π‘))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))))
346332, 345eqtr3d 2766 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + ((2 Β· ((𝑒 βˆ’ 𝑁) / 𝑁)) + (𝑇 / (logβ€˜π‘)))) = ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))))
347328, 346breqtrd 5164 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 1)) + (((Οˆβ€˜π‘’) βˆ’ (Οˆβ€˜π‘)) / 𝑁)) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))))
34893, 149, 139, 255, 347letrd 11368 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ≀ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))))
349100rehalfcld 12456 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 2) / 2) ∈ ℝ)
35077, 297, 78ledivmul2d 13067 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 / 𝑁) ≀ (1 + (𝐿 Β· 𝐸)) ↔ 𝑒 ≀ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁)))
351292, 350mpbird 257 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 / 𝑁) ≀ (1 + (𝐿 Β· 𝐸)))
352 ax-1cn 11164 . . . . . . . . . . . . . . . 16 1 ∈ β„‚
35315adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐿 Β· 𝐸) ∈ ℝ)
354353recnd 11239 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐿 Β· 𝐸) ∈ β„‚)
355 addcom 11397 . . . . . . . . . . . . . . . 16 ((1 ∈ β„‚ ∧ (𝐿 Β· 𝐸) ∈ β„‚) β†’ (1 + (𝐿 Β· 𝐸)) = ((𝐿 Β· 𝐸) + 1))
356352, 354, 355sylancr 586 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 + (𝐿 Β· 𝐸)) = ((𝐿 Β· 𝐸) + 1))
357351, 356breqtrd 5164 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑒 / 𝑁) ≀ ((𝐿 Β· 𝐸) + 1))
358171, 111, 353lesubaddd 11808 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 / 𝑁) βˆ’ 1) ≀ (𝐿 Β· 𝐸) ↔ (𝑒 / 𝑁) ≀ ((𝐿 Β· 𝐸) + 1)))
359357, 358mpbird 257 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 / 𝑁) βˆ’ 1) ≀ (𝐿 Β· 𝐸))
360169, 359eqbrtrd 5160 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑒 βˆ’ 𝑁) / 𝑁) ≀ (𝐿 Β· 𝐸))
3619adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐴 ∈ ℝ+)
362361rpred 13013 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐴 ∈ ℝ)
363 fveq2 6881 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑒 β†’ (π‘…β€˜π‘₯) = (π‘…β€˜π‘’))
364 id 22 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑒 β†’ π‘₯ = 𝑒)
365363, 364oveq12d 7419 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑒 β†’ ((π‘…β€˜π‘₯) / π‘₯) = ((π‘…β€˜π‘’) / 𝑒))
366365fveq2d 6885 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑒 β†’ (absβ€˜((π‘…β€˜π‘₯) / π‘₯)) = (absβ€˜((π‘…β€˜π‘’) / 𝑒)))
367366breq1d 5148 . . . . . . . . . . . . . 14 (π‘₯ = 𝑒 β†’ ((absβ€˜((π‘…β€˜π‘₯) / π‘₯)) ≀ 𝐴 ↔ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐴))
36874adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ βˆ€π‘₯ ∈ ℝ+ (absβ€˜((π‘…β€˜π‘₯) / π‘₯)) ≀ 𝐴)
369367, 368, 80rspcdva 3605 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐴)
37086, 362, 105, 369leadd1dd 11825 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ≀ (𝐴 + 3))
371103, 200jca 511 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) ∈ ℝ ∧ 0 ≀ ((𝑒 βˆ’ 𝑁) / 𝑁)))
372 3rp 12977 . . . . . . . . . . . . . . 15 3 ∈ ℝ+
373 rpaddcl 12993 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ+ ∧ 3 ∈ ℝ+) β†’ (𝐴 + 3) ∈ ℝ+)
374361, 372, 373sylancl 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐴 + 3) ∈ ℝ+)
375374rprege0d 13020 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐴 + 3) ∈ ℝ ∧ 0 ≀ (𝐴 + 3)))
376 lemul12b 12068 . . . . . . . . . . . . 13 ((((((𝑒 βˆ’ 𝑁) / 𝑁) ∈ ℝ ∧ 0 ≀ ((𝑒 βˆ’ 𝑁) / 𝑁)) ∧ (𝐿 Β· 𝐸) ∈ ℝ) ∧ (((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ∈ ℝ ∧ ((𝐴 + 3) ∈ ℝ ∧ 0 ≀ (𝐴 + 3)))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) ≀ (𝐿 Β· 𝐸) ∧ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ≀ (𝐴 + 3)) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ≀ ((𝐿 Β· 𝐸) Β· (𝐴 + 3))))
377371, 353, 106, 375, 376syl22anc 836 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) ≀ (𝐿 Β· 𝐸) ∧ ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3) ≀ (𝐴 + 3)) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ≀ ((𝐿 Β· 𝐸) Β· (𝐴 + 3))))
378360, 370, 377mp2and 696 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ≀ ((𝐿 Β· 𝐸) Β· (𝐴 + 3)))
37935adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐸 ∈ ℝ+)
380112, 113mp1i 13 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 4 ∈ ℝ+)
381379, 380rpdivcld 13030 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 4) ∈ ℝ+)
382381rpcnd 13015 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 4) ∈ β„‚)
383374rpcnd 13015 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐴 + 3) ∈ β„‚)
384374rpne0d 13018 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐴 + 3) β‰  0)
385382, 383, 384divcan1d 11988 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝐸 / 4) / (𝐴 + 3)) Β· (𝐴 + 3)) = (𝐸 / 4))
38614recnd 11239 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐸 ∈ β„‚)
387386adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 𝐸 ∈ β„‚)
388380rpcnd 13015 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 4 ∈ β„‚)
389380rpne0d 13018 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 4 β‰  0)
390387, 388, 389divrec2d 11991 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 4) = ((1 / 4) Β· 𝐸))
391390oveq1d 7416 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 4) / (𝐴 + 3)) = (((1 / 4) Β· 𝐸) / (𝐴 + 3)))
392 4cn 12294 . . . . . . . . . . . . . . . . . 18 4 ∈ β„‚
393 4ne0 12317 . . . . . . . . . . . . . . . . . 18 4 β‰  0
394392, 393reccli 11941 . . . . . . . . . . . . . . . . 17 (1 / 4) ∈ β„‚
395394a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (1 / 4) ∈ β„‚)
396395, 387, 383, 384div23d 12024 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((1 / 4) Β· 𝐸) / (𝐴 + 3)) = (((1 / 4) / (𝐴 + 3)) Β· 𝐸))
39710oveq1i 7411 . . . . . . . . . . . . . . 15 (𝐿 Β· 𝐸) = (((1 / 4) / (𝐴 + 3)) Β· 𝐸)
398396, 397eqtr4di 2782 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((1 / 4) Β· 𝐸) / (𝐴 + 3)) = (𝐿 Β· 𝐸))
399391, 398eqtr2d 2765 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐿 Β· 𝐸) = ((𝐸 / 4) / (𝐴 + 3)))
400399oveq1d 7416 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐿 Β· 𝐸) Β· (𝐴 + 3)) = (((𝐸 / 4) / (𝐴 + 3)) Β· (𝐴 + 3)))
401 2ne0 12313 . . . . . . . . . . . . . . 15 2 β‰  0
402401a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ 2 β‰  0)
403387, 314, 314, 402, 402divdiv1d 12018 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 2) / 2) = (𝐸 / (2 Β· 2)))
404 2t2e4 12373 . . . . . . . . . . . . . 14 (2 Β· 2) = 4
405404oveq2i 7412 . . . . . . . . . . . . 13 (𝐸 / (2 Β· 2)) = (𝐸 / 4)
406403, 405eqtrdi 2780 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 2) / 2) = (𝐸 / 4))
407385, 400, 4063eqtr4d 2774 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐿 Β· 𝐸) Β· (𝐴 + 3)) = ((𝐸 / 2) / 2))
408378, 407breqtrd 5164 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) ≀ ((𝐸 / 2) / 2))
409117adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (𝐸 / 4)) ∈ ℝ)
410137rpred 13013 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (logβ€˜π‘) ∈ ℝ)
41178reeflogd 26474 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (expβ€˜(logβ€˜π‘)) = 𝑁)
412135, 411breqtrrd 5166 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (expβ€˜(𝑇 / (𝐸 / 4))) < (expβ€˜(logβ€˜π‘)))
413 eflt 16057 . . . . . . . . . . . . . . 15 (((𝑇 / (𝐸 / 4)) ∈ ℝ ∧ (logβ€˜π‘) ∈ ℝ) β†’ ((𝑇 / (𝐸 / 4)) < (logβ€˜π‘) ↔ (expβ€˜(𝑇 / (𝐸 / 4))) < (expβ€˜(logβ€˜π‘))))
414409, 410, 413syl2anc 583 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝑇 / (𝐸 / 4)) < (logβ€˜π‘) ↔ (expβ€˜(𝑇 / (𝐸 / 4))) < (expβ€˜(logβ€˜π‘))))
415412, 414mpbird 257 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (𝐸 / 4)) < (logβ€˜π‘))
416409, 410, 415ltled 11359 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (𝐸 / 4)) ≀ (logβ€˜π‘))
417110, 381, 137, 416lediv23d 13081 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ≀ (𝐸 / 4))
418417, 406breqtrrd 5166 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝑇 / (logβ€˜π‘)) ≀ ((𝐸 / 2) / 2))
419107, 138, 349, 349, 408, 418le2addd 11830 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))) ≀ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)))
420100recnd 11239 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (𝐸 / 2) ∈ β„‚)
4214202halvesd 12455 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)) = (𝐸 / 2))
422419, 421breqtrd 5164 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((((𝑒 βˆ’ 𝑁) / 𝑁) Β· ((absβ€˜((π‘…β€˜π‘’) / 𝑒)) + 3)) + (𝑇 / (logβ€˜π‘))) ≀ (𝐸 / 2))
42393, 139, 100, 348, 422letrd 11368 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) ≀ (𝐸 / 2))
4243simprd 495 . . . . . . . 8 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ≀ (𝐸 / 2))
425424adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘) / 𝑁)) ≀ (𝐸 / 2))
42693, 94, 100, 100, 423, 425le2addd 11830 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁))) ≀ ((𝐸 / 2) + (𝐸 / 2)))
4273872halvesd 12455 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
428426, 427breqtrd 5164 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ ((absβ€˜(((π‘…β€˜π‘’) / 𝑒) βˆ’ ((π‘…β€˜π‘) / 𝑁))) + (absβ€˜((π‘…β€˜π‘) / 𝑁))) ≀ 𝐸)
42986, 95, 96, 99, 428letrd 11368 . . . 4 ((πœ‘ ∧ 𝑒 ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))) β†’ (absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸)
430429ralrimiva 3138 . . 3 (πœ‘ β†’ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸)
4315, 73, 430jca31 514 . 2 (πœ‘ β†’ ((π‘Œ < 𝑁 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
432 breq2 5142 . . . . 5 (𝑧 = 𝑁 β†’ (π‘Œ < 𝑧 ↔ π‘Œ < 𝑁))
433 oveq2 7409 . . . . . 6 (𝑧 = 𝑁 β†’ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) = ((1 + (𝐿 Β· 𝐸)) Β· 𝑁))
434433breq1d 5148 . . . . 5 (𝑧 = 𝑁 β†’ (((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ) ↔ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ)))
435432, 434anbi12d 630 . . . 4 (𝑧 = 𝑁 β†’ ((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ↔ (π‘Œ < 𝑁 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ))))
436 id 22 . . . . . 6 (𝑧 = 𝑁 β†’ 𝑧 = 𝑁)
437436, 433oveq12d 7419 . . . . 5 (𝑧 = 𝑁 β†’ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧)) = (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁)))
438437raleqdv 3317 . . . 4 (𝑧 = 𝑁 β†’ (βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸 ↔ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
439435, 438anbi12d 630 . . 3 (𝑧 = 𝑁 β†’ (((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸) ↔ ((π‘Œ < 𝑁 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸)))
440439rspcev 3604 . 2 ((𝑁 ∈ ℝ+ ∧ ((π‘Œ < 𝑁 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑁) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑁[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑁))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸)) β†’ βˆƒπ‘§ ∈ ℝ+ ((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
4412, 431, 440syl2anc 583 1 (πœ‘ β†’ βˆƒπ‘§ ∈ ℝ+ ((π‘Œ < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝑀 Β· π‘Œ)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062   βŠ† wss 3940   class class class wbr 5138   ↦ cmpt 5221  β€˜cfv 6533  (class class class)co 7401  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111  +∞cpnf 11242  β„*cxr 11244   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441  -cneg 11442   / cdiv 11868  β„•cn 12209  2c2 12264  3c3 12265  4c4 12266  β„+crp 12971  (,)cioo 13321  [,)cico 13323  [,]cicc 13324  abscabs 15178  expce 16002  logclog 26405  Οˆcchp 26941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-pi 16013  df-dvds 16195  df-gcd 16433  df-prm 16606  df-pc 16769  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-fbas 21225  df-fg 21226  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-nei 22924  df-lp 22962  df-perf 22963  df-cn 23053  df-cnp 23054  df-haus 23141  df-tx 23388  df-hmeo 23581  df-fil 23672  df-fm 23764  df-flim 23765  df-flf 23766  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718  df-log 26407  df-vma 26946  df-chp 26947
This theorem is referenced by:  pntibndlem3  27441
  Copyright terms: Public domain W3C validator