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

Theorem pntlemj 27103
Description: Lemma for pnt 27114. The induction step. Using pntibnd 27093, we find an interval in ๐พโ†‘๐ฝ...๐พโ†‘(๐ฝ + 1) which is sufficiently large and has a much smaller value, ๐‘…(๐‘ง) / ๐‘ง โ‰ค ๐ธ (instead of our original bound ๐‘…(๐‘ง) / ๐‘ง โ‰ค ๐‘ˆ). (Contributed by Mario Carneiro, 13-Apr-2016.)
Hypotheses
Ref Expression
pntlem1.r ๐‘… = (๐‘Ž โˆˆ โ„+ โ†ฆ ((ฯˆโ€˜๐‘Ž) โˆ’ ๐‘Ž))
pntlem1.a (๐œ‘ โ†’ ๐ด โˆˆ โ„+)
pntlem1.b (๐œ‘ โ†’ ๐ต โˆˆ โ„+)
pntlem1.l (๐œ‘ โ†’ ๐ฟ โˆˆ (0(,)1))
pntlem1.d ๐ท = (๐ด + 1)
pntlem1.f ๐น = ((1 โˆ’ (1 / ๐ท)) ยท ((๐ฟ / (32 ยท ๐ต)) / (๐ทโ†‘2)))
pntlem1.u (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„+)
pntlem1.u2 (๐œ‘ โ†’ ๐‘ˆ โ‰ค ๐ด)
pntlem1.e ๐ธ = (๐‘ˆ / ๐ท)
pntlem1.k ๐พ = (expโ€˜(๐ต / ๐ธ))
pntlem1.y (๐œ‘ โ†’ (๐‘Œ โˆˆ โ„+ โˆง 1 โ‰ค ๐‘Œ))
pntlem1.x (๐œ‘ โ†’ (๐‘‹ โˆˆ โ„+ โˆง ๐‘Œ < ๐‘‹))
pntlem1.c (๐œ‘ โ†’ ๐ถ โˆˆ โ„+)
pntlem1.w ๐‘Š = (((๐‘Œ + (4 / (๐ฟ ยท ๐ธ)))โ†‘2) + (((๐‘‹ ยท (๐พโ†‘2))โ†‘4) + (expโ€˜(((32 ยท ๐ต) / ((๐‘ˆ โˆ’ ๐ธ) ยท (๐ฟ ยท (๐ธโ†‘2)))) ยท ((๐‘ˆ ยท 3) + ๐ถ)))))
pntlem1.z (๐œ‘ โ†’ ๐‘ โˆˆ (๐‘Š[,)+โˆž))
pntlem1.m ๐‘€ = ((โŒŠโ€˜((logโ€˜๐‘‹) / (logโ€˜๐พ))) + 1)
pntlem1.n ๐‘ = (โŒŠโ€˜(((logโ€˜๐‘) / (logโ€˜๐พ)) / 2))
pntlem1.U (๐œ‘ โ†’ โˆ€๐‘ง โˆˆ (๐‘Œ[,)+โˆž)(absโ€˜((๐‘…โ€˜๐‘ง) / ๐‘ง)) โ‰ค ๐‘ˆ)
pntlem1.K (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ (๐‘‹(,)+โˆž)โˆƒ๐‘ง โˆˆ โ„+ ((๐‘ฆ < ๐‘ง โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘ง) < (๐พ ยท ๐‘ฆ)) โˆง โˆ€๐‘ข โˆˆ (๐‘ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘ง))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ))
pntlem1.o ๐‘‚ = (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
pntlem1.v (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„+)
pntlem1.V (๐œ‘ โ†’ (((๐พโ†‘๐ฝ) < ๐‘‰ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ))) โˆง โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ))
pntlem1.j (๐œ‘ โ†’ ๐ฝ โˆˆ (๐‘€..^๐‘))
pntlem1.i ๐ผ = (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰)))
Assertion
Ref Expression
pntlemj (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
Distinct variable groups:   ๐‘ง,๐ถ   ๐‘›,๐ผ   ๐‘ฆ,๐‘›,๐‘ง,๐ฝ   ๐‘ข,๐‘›,๐ฟ,๐‘ฆ,๐‘ง   ๐‘›,๐พ,๐‘ฆ,๐‘ง   ๐‘›,๐‘€,๐‘ง   ๐‘›,๐‘‚,๐‘ง   ๐œ‘,๐‘›   ๐‘›,๐‘,๐‘ง   ๐‘…,๐‘›,๐‘ข,๐‘ฆ,๐‘ง   ๐‘›,๐‘‰,๐‘ข   ๐‘ˆ,๐‘›,๐‘ง   ๐‘›,๐‘Š,๐‘ง   ๐‘›,๐‘‹,๐‘ฆ,๐‘ง   ๐‘›,๐‘Œ,๐‘ง   ๐‘›,๐‘Ž,๐‘ข,๐‘ฆ,๐‘ง,๐ธ   ๐‘›,๐‘,๐‘ข,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘ฆ,๐‘ง,๐‘ข,๐‘Ž)   ๐ด(๐‘ฆ,๐‘ง,๐‘ข,๐‘›,๐‘Ž)   ๐ต(๐‘ฆ,๐‘ง,๐‘ข,๐‘›,๐‘Ž)   ๐ถ(๐‘ฆ,๐‘ข,๐‘›,๐‘Ž)   ๐ท(๐‘ฆ,๐‘ง,๐‘ข,๐‘›,๐‘Ž)   ๐‘…(๐‘Ž)   ๐‘ˆ(๐‘ฆ,๐‘ข,๐‘Ž)   ๐น(๐‘ฆ,๐‘ง,๐‘ข,๐‘›,๐‘Ž)   ๐ผ(๐‘ฆ,๐‘ง,๐‘ข,๐‘Ž)   ๐ฝ(๐‘ข,๐‘Ž)   ๐พ(๐‘ข,๐‘Ž)   ๐ฟ(๐‘Ž)   ๐‘€(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘‚(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘‰(๐‘ฆ,๐‘ง,๐‘Ž)   ๐‘Š(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘‹(๐‘ข,๐‘Ž)   ๐‘Œ(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘(๐‘ฆ,๐‘Ž)

Proof of Theorem pntlemj
StepHypRef Expression
1 pntlem1.r . . . . . . 7 ๐‘… = (๐‘Ž โˆˆ โ„+ โ†ฆ ((ฯˆโ€˜๐‘Ž) โˆ’ ๐‘Ž))
2 pntlem1.a . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ โ„+)
3 pntlem1.b . . . . . . 7 (๐œ‘ โ†’ ๐ต โˆˆ โ„+)
4 pntlem1.l . . . . . . 7 (๐œ‘ โ†’ ๐ฟ โˆˆ (0(,)1))
5 pntlem1.d . . . . . . 7 ๐ท = (๐ด + 1)
6 pntlem1.f . . . . . . 7 ๐น = ((1 โˆ’ (1 / ๐ท)) ยท ((๐ฟ / (32 ยท ๐ต)) / (๐ทโ†‘2)))
7 pntlem1.u . . . . . . 7 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„+)
8 pntlem1.u2 . . . . . . 7 (๐œ‘ โ†’ ๐‘ˆ โ‰ค ๐ด)
9 pntlem1.e . . . . . . 7 ๐ธ = (๐‘ˆ / ๐ท)
10 pntlem1.k . . . . . . 7 ๐พ = (expโ€˜(๐ต / ๐ธ))
111, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 27095 . . . . . 6 (๐œ‘ โ†’ (๐ธ โˆˆ โ„+ โˆง ๐พ โˆˆ โ„+ โˆง (๐ธ โˆˆ (0(,)1) โˆง 1 < ๐พ โˆง (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+)))
1211simp3d 1144 . . . . 5 (๐œ‘ โ†’ (๐ธ โˆˆ (0(,)1) โˆง 1 < ๐พ โˆง (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+))
1312simp3d 1144 . . . 4 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+)
141, 2, 3, 4, 5, 6pntlemd 27094 . . . . . . . 8 (๐œ‘ โ†’ (๐ฟ โˆˆ โ„+ โˆง ๐ท โˆˆ โ„+ โˆง ๐น โˆˆ โ„+))
1514simp1d 1142 . . . . . . 7 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„+)
1611simp1d 1142 . . . . . . 7 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
1715, 16rpmulcld 13031 . . . . . 6 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) โˆˆ โ„+)
18 8nn 12306 . . . . . . 7 8 โˆˆ โ„•
19 nnrp 12984 . . . . . . 7 (8 โˆˆ โ„• โ†’ 8 โˆˆ โ„+)
2018, 19ax-mp 5 . . . . . 6 8 โˆˆ โ„+
21 rpdivcl 12998 . . . . . 6 (((๐ฟ ยท ๐ธ) โˆˆ โ„+ โˆง 8 โˆˆ โ„+) โ†’ ((๐ฟ ยท ๐ธ) / 8) โˆˆ โ„+)
2217, 20, 21sylancl 586 . . . . 5 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 8) โˆˆ โ„+)
23 pntlem1.y . . . . . . . . 9 (๐œ‘ โ†’ (๐‘Œ โˆˆ โ„+ โˆง 1 โ‰ค ๐‘Œ))
24 pntlem1.x . . . . . . . . 9 (๐œ‘ โ†’ (๐‘‹ โˆˆ โ„+ โˆง ๐‘Œ < ๐‘‹))
25 pntlem1.c . . . . . . . . 9 (๐œ‘ โ†’ ๐ถ โˆˆ โ„+)
26 pntlem1.w . . . . . . . . 9 ๐‘Š = (((๐‘Œ + (4 / (๐ฟ ยท ๐ธ)))โ†‘2) + (((๐‘‹ ยท (๐พโ†‘2))โ†‘4) + (expโ€˜(((32 ยท ๐ต) / ((๐‘ˆ โˆ’ ๐ธ) ยท (๐ฟ ยท (๐ธโ†‘2)))) ยท ((๐‘ˆ ยท 3) + ๐ถ)))))
27 pntlem1.z . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ (๐‘Š[,)+โˆž))
281, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27pntlemb 27097 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ โˆˆ โ„+ โˆง (1 < ๐‘ โˆง e โ‰ค (โˆšโ€˜๐‘) โˆง (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘Œ)) โˆง ((4 / (๐ฟ ยท ๐ธ)) โ‰ค (โˆšโ€˜๐‘) โˆง (((logโ€˜๐‘‹) / (logโ€˜๐พ)) + 2) โ‰ค (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โˆง ((๐‘ˆ ยท 3) + ๐ถ) โ‰ค (((๐‘ˆ โˆ’ ๐ธ) ยท ((๐ฟ ยท (๐ธโ†‘2)) / (32 ยท ๐ต))) ยท (logโ€˜๐‘)))))
2928simp1d 1142 . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ โ„+)
3029rpred 13015 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
3128simp2d 1143 . . . . . . 7 (๐œ‘ โ†’ (1 < ๐‘ โˆง e โ‰ค (โˆšโ€˜๐‘) โˆง (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘Œ)))
3231simp1d 1142 . . . . . 6 (๐œ‘ โ†’ 1 < ๐‘)
3330, 32rplogcld 26136 . . . . 5 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„+)
3422, 33rpmulcld 13031 . . . 4 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)) โˆˆ โ„+)
3513, 34rpmulcld 13031 . . 3 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โˆˆ โ„+)
3635rpred 13015 . 2 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โˆˆ โ„)
37 pntlem1.i . . . . . 6 ๐ผ = (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰)))
38 fzfid 13937 . . . . . 6 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โˆˆ Fin)
3937, 38eqeltrid 2837 . . . . 5 (๐œ‘ โ†’ ๐ผ โˆˆ Fin)
40 hashcl 14315 . . . . 5 (๐ผ โˆˆ Fin โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„•0)
4139, 40syl 17 . . . 4 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„•0)
4241nn0red 12532 . . 3 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„)
4313rpred 13015 . . . 4 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
44 pntlem1.v . . . . . . 7 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„+)
4529, 44rpdivcld 13032 . . . . . 6 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„+)
4645relogcld 26130 . . . . 5 (๐œ‘ โ†’ (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„)
4746, 45rerpdivcld 13046 . . . 4 (๐œ‘ โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„)
4843, 47remulcld 11243 . . 3 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
4942, 48remulcld 11243 . 2 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) โˆˆ โ„)
50 pntlem1.o . . . 4 ๐‘‚ = (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
51 fzfid 13937 . . . 4 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โˆˆ Fin)
5250, 51eqeltrid 2837 . . 3 (๐œ‘ โ†’ ๐‘‚ โˆˆ Fin)
537rpred 13015 . . . . . . 7 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„)
5453adantr 481 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘ˆ โˆˆ โ„)
5511simp2d 1143 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐พ โˆˆ โ„+)
56 pntlem1.j . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐‘€..^๐‘))
57 elfzoelz 13631 . . . . . . . . . . . . 13 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ โ„ค)
5856, 57syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค)
5958peano2zd 12668 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฝ + 1) โˆˆ โ„ค)
6055, 59rpexpcld 14209 . . . . . . . . . 10 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โˆˆ โ„+)
6129, 60rpdivcld 13032 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„+)
6261rprege0d 13022 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / (๐พโ†‘(๐ฝ + 1)))))
63 flge0nn0 13784 . . . . . . . 8 (((๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / (๐พโ†‘(๐ฝ + 1)))) โ†’ (โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) โˆˆ โ„•0)
64 nn0p1nn 12510 . . . . . . . 8 ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) โˆˆ โ„•0 โ†’ ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„•)
6562, 63, 643syl 18 . . . . . . 7 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„•)
66 elfzuz 13496 . . . . . . . 8 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)))
6766, 50eleq2s 2851 . . . . . . 7 (๐‘› โˆˆ ๐‘‚ โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)))
68 eluznn 12901 . . . . . . 7 ((((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„• โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1))) โ†’ ๐‘› โˆˆ โ„•)
6965, 67, 68syl2an 596 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„•)
7054, 69nndivred 12265 . . . . 5 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ˆ / ๐‘›) โˆˆ โ„)
7129adantr 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘ โˆˆ โ„+)
7269nnrpd 13013 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„+)
7371, 72rpdivcld 13032 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / ๐‘›) โˆˆ โ„+)
741pntrf 27063 . . . . . . . . . 10 ๐‘…:โ„+โŸถโ„
7574ffvelcdmi 7085 . . . . . . . . 9 ((๐‘ / ๐‘›) โˆˆ โ„+ โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
7673, 75syl 17 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
7776, 71rerpdivcld 13046 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„)
7877recnd 11241 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„‚)
7978abscld 15382 . . . . 5 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โˆˆ โ„)
8070, 79resubcld 11641 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) โˆˆ โ„)
8172relogcld 26130 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
8280, 81remulcld 11243 . . 3 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โˆˆ โ„)
8352, 82fsumrecl 15679 . 2 (๐œ‘ โ†’ ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โˆˆ โ„)
84 pntlem1.m . . 3 ๐‘€ = ((โŒŠโ€˜((logโ€˜๐‘‹) / (logโ€˜๐พ))) + 1)
85 pntlem1.n . . 3 ๐‘ = (โŒŠโ€˜(((logโ€˜๐‘) / (logโ€˜๐พ)) / 2))
86 pntlem1.U . . 3 (๐œ‘ โ†’ โˆ€๐‘ง โˆˆ (๐‘Œ[,)+โˆž)(absโ€˜((๐‘…โ€˜๐‘ง) / ๐‘ง)) โ‰ค ๐‘ˆ)
87 pntlem1.K . . 3 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ (๐‘‹(,)+โˆž)โˆƒ๐‘ง โˆˆ โ„+ ((๐‘ฆ < ๐‘ง โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘ง) < (๐พ ยท ๐‘ฆ)) โˆง โˆ€๐‘ข โˆˆ (๐‘ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘ง))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ))
88 pntlem1.V . . 3 (๐œ‘ โ†’ (((๐พโ†‘๐ฝ) < ๐‘‰ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ))) โˆง โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ))
891, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37pntlemr 27102 . 2 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
9048recnd 11241 . . . . 5 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚)
91 fsumconst 15735 . . . . 5 ((๐ผ โˆˆ Fin โˆง ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚) โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
9239, 90, 91syl2anc 584 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
931, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37pntlemq 27101 . . . . 5 (๐œ‘ โ†’ ๐ผ โŠ† ๐‘‚)
9490ralrimivw 3150 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚)
9552olcd 872 . . . . 5 (๐œ‘ โ†’ (๐‘‚ โŠ† (โ„คโ‰ฅโ€˜1) โˆจ ๐‘‚ โˆˆ Fin))
96 sumss2 15671 . . . . 5 (((๐ผ โŠ† ๐‘‚ โˆง โˆ€๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚) โˆง (๐‘‚ โŠ† (โ„คโ‰ฅโ€˜1) โˆจ ๐‘‚ โˆˆ Fin)) โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9793, 94, 95, 96syl21anc 836 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9892, 97eqtr3d 2774 . . 3 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9948adantr 481 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
10099adantlr 713 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
101 0red 11216 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ยฌ ๐‘› โˆˆ ๐ผ) โ†’ 0 โˆˆ โ„)
102100, 101ifclda 4563 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โˆˆ โ„)
103 breq1 5151 . . . . 5 (((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โ†” if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›))))
104 breq1 5151 . . . . 5 (0 = if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ†’ (0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โ†” if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›))))
10513rpregt0d 13021 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ)))
106105adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ)))
107106simpld 495 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
108 1rp 12977 . . . . . . . . . . . . . . . . 17 1 โˆˆ โ„+
109 rpaddcl 12995 . . . . . . . . . . . . . . . . 17 ((1 โˆˆ โ„+ โˆง (๐ฟ ยท ๐ธ) โˆˆ โ„+) โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
110108, 17, 109sylancr 587 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
111110, 44rpmulcld 13031 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„+)
11229, 111rpdivcld 13032 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„+)
113112rprege0d 13022 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
114 flge0nn0 13784 . . . . . . . . . . . . 13 (((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„•0)
115 nn0p1nn 12510 . . . . . . . . . . . . 13 ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„•0 โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„•)
116113, 114, 1153syl 18 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„•)
117 elfzuz 13496 . . . . . . . . . . . . 13 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
118117, 37eleq2s 2851 . . . . . . . . . . . 12 (๐‘› โˆˆ ๐ผ โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
119 eluznn 12901 . . . . . . . . . . . 12 ((((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„• โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))) โ†’ ๐‘› โˆˆ โ„•)
120116, 118, 119syl2an 596 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„•)
121120nnrpd 13013 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„+)
122121relogcld 26130 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
123122, 120nndivred 12265 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜๐‘›) / ๐‘›) โˆˆ โ„)
124107, 123remulcld 11243 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)) โˆˆ โ„)
12593sselda 3982 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ ๐‘‚)
126125, 82syldan 591 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โˆˆ โ„)
127 simpr 485 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ ๐ผ)
128127, 37eleqtrdi 2843 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))))
129 elfzle2 13504 . . . . . . . . . . 11 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰)))
130128, 129syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰)))
13145rpred 13015 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„)
132131adantr 481 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘‰) โˆˆ โ„)
133128elfzelzd 13501 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„ค)
134 flge 13769 . . . . . . . . . . 11 (((๐‘ / ๐‘‰) โˆˆ โ„ โˆง ๐‘› โˆˆ โ„ค) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰))))
135132, 133, 134syl2anc 584 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰))))
136130, 135mpbird 256 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โ‰ค (๐‘ / ๐‘‰))
137120nnred 12226 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„)
138 ere 16031 . . . . . . . . . . . 12 e โˆˆ โ„
139138a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โˆˆ โ„)
140112rpred 13015 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„)
141140adantr 481 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„)
142138a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ e โˆˆ โ„)
14329rpsqrtcld 15357 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„+)
144143rpred 13015 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„)
14531simp2d 1143 . . . . . . . . . . . . 13 (๐œ‘ โ†’ e โ‰ค (โˆšโ€˜๐‘))
146111rpred 13015 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„)
14760rpred 13015 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โˆˆ โ„)
14888simpld 495 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((๐พโ†‘๐ฝ) < ๐‘‰ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ))))
149148simprd 496 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ)))
15055rpcnd 13017 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐พ โˆˆ โ„‚)
15155, 58rpexpcld 14209 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„+)
152151rpcnd 13017 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„‚)
153150, 152mulcomd 11234 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐พ ยท (๐พโ†‘๐ฝ)) = ((๐พโ†‘๐ฝ) ยท ๐พ))
1541, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemg 27098 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โ‰ค (๐‘ โˆ’ ๐‘€)))
155154simp1d 1142 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
156 elfzouz 13635 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
15756, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
158 eluznn 12901 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘€ โˆˆ โ„• โˆง ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐ฝ โˆˆ โ„•)
159155, 157, 158syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•)
160159nnnn0d 12531 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•0)
161150, 160expp1d 14111 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) = ((๐พโ†‘๐ฝ) ยท ๐พ))
162153, 161eqtr4d 2775 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐พ ยท (๐พโ†‘๐ฝ)) = (๐พโ†‘(๐ฝ + 1)))
163149, 162breqtrd 5174 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พโ†‘(๐ฝ + 1)))
164146, 147, 163ltled 11361 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (๐พโ†‘(๐ฝ + 1)))
165 fzofzp1 13728 . . . . . . . . . . . . . . . . . . . 20 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ (๐ฝ + 1) โˆˆ (๐‘€...๐‘))
16656, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ฝ + 1) โˆˆ (๐‘€...๐‘))
1671, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 27099 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐ฝ + 1) โˆˆ (๐‘€...๐‘)) โ†’ (๐‘‹ < (๐พโ†‘(๐ฝ + 1)) โˆง (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘)))
168166, 167mpdan 685 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘‹ < (๐พโ†‘(๐ฝ + 1)) โˆง (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘)))
169168simprd 496 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘))
170146, 147, 144, 164, 169letrd 11370 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (โˆšโ€˜๐‘))
171146, 144, 143lemul2d 13059 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (โˆšโ€˜๐‘) โ†” ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘))))
172170, 171mpbid 231 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)))
17329rprege0d 13022 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘))
174 remsqsqrt 15202 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘) โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
175173, 174syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
176172, 175breqtrd 5174 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘)
177144, 30, 111lemuldivd 13064 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘ โ†” (โˆšโ€˜๐‘) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
178176, 177mpbid 231 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
179142, 144, 140, 145, 178letrd 11370 . . . . . . . . . . . 12 (๐œ‘ โ†’ e โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
180179adantr 481 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
181 reflcl 13760 . . . . . . . . . . . . . 14 ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„)
182 peano2re 11386 . . . . . . . . . . . . . 14 ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
183140, 181, 1823syl 18 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
184183adantr 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
185 fllep1 13765 . . . . . . . . . . . . 13 ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))
186141, 185syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))
187 elfzle1 13503 . . . . . . . . . . . . 13 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โ‰ค ๐‘›)
188128, 187syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โ‰ค ๐‘›)
189141, 184, 137, 186, 188letrd 11370 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘›)
190139, 141, 137, 180, 189letrd 11370 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค ๐‘›)
191139, 137, 132, 190, 136letrd 11370 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค (๐‘ / ๐‘‰))
192 logdivle 26129 . . . . . . . . . 10 (((๐‘› โˆˆ โ„ โˆง e โ‰ค ๐‘›) โˆง ((๐‘ / ๐‘‰) โˆˆ โ„ โˆง e โ‰ค (๐‘ / ๐‘‰))) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›)))
193137, 190, 132, 191, 192syl22anc 837 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›)))
194136, 193mpbid 231 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›))
19547adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„)
196 lemul2 12066 . . . . . . . . 9 ((((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„ โˆง ((logโ€˜๐‘›) / ๐‘›) โˆˆ โ„ โˆง ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ))) โ†’ (((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›) โ†” ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›))))
197195, 123, 106, 196syl3anc 1371 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›) โ†” ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›))))
198194, 197mpbid 231 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
19913rpcnd 13017 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚)
200199adantr 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚)
201122recnd 11241 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜๐‘›) โˆˆ โ„‚)
202121rpcnne0d 13024 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0))
203 div23 11890 . . . . . . . . . 10 (((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚ โˆง (logโ€˜๐‘›) โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)))
204200, 201, 202, 203syl3anc 1371 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)))
205 divass 11889 . . . . . . . . . 10 (((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚ โˆง (logโ€˜๐‘›) โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
206200, 201, 202, 205syl3anc 1371 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
207204, 206eqtr3d 2774 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
20843adantr 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
209208, 120nndivred 12265 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) โˆˆ โ„)
210125, 80syldan 591 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) โˆˆ โ„)
211 log1 26093 . . . . . . . . . 10 (logโ€˜1) = 0
212120nnge1d 12259 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ 1 โ‰ค ๐‘›)
213 logleb 26110 . . . . . . . . . . . 12 ((1 โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โ†’ (1 โ‰ค ๐‘› โ†” (logโ€˜1) โ‰ค (logโ€˜๐‘›)))
214108, 121, 213sylancr 587 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (1 โ‰ค ๐‘› โ†” (logโ€˜1) โ‰ค (logโ€˜๐‘›)))
215212, 214mpbid 231 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜1) โ‰ค (logโ€˜๐‘›))
216211, 215eqbrtrrid 5184 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ 0 โ‰ค (logโ€˜๐‘›))
2177rpcnd 13017 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„‚)
218217adantr 481 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ˆ โˆˆ โ„‚)
21916rpred 13015 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
220219adantr 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐ธ โˆˆ โ„)
221220recnd 11241 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐ธ โˆˆ โ„‚)
222 divsubdir 11907 . . . . . . . . . . 11 ((๐‘ˆ โˆˆ โ„‚ โˆง ๐ธ โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) = ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)))
223218, 221, 202, 222syl3anc 1371 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) = ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)))
224125, 79syldan 591 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โˆˆ โ„)
225220, 120nndivred 12265 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐ธ / ๐‘›) โˆˆ โ„)
226125, 70syldan 591 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ / ๐‘›) โˆˆ โ„)
227125, 76syldan 591 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
228227recnd 11241 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚)
22929adantr 481 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ โˆˆ โ„+)
230229rpcnne0d 13024 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0))
231 divdiv2 11925 . . . . . . . . . . . . . . . . 17 (((๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚ โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0) โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘))
232228, 230, 202, 231syl3anc 1371 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘))
233121rpcnd 13017 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„‚)
234 div23 11890 . . . . . . . . . . . . . . . . 17 (((๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚ โˆง ๐‘› โˆˆ โ„‚ โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0)) โ†’ (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
235228, 233, 230, 234syl3anc 1371 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
236232, 235eqtrd 2772 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
237236fveq2d 6895 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) = (absโ€˜(((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›)))
238125, 78syldan 591 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„‚)
239238, 233absmuld 15400 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜(((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›)) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท (absโ€˜๐‘›)))
240121rprege0d 13022 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„ โˆง 0 โ‰ค ๐‘›))
241 absid 15242 . . . . . . . . . . . . . . . 16 ((๐‘› โˆˆ โ„ โˆง 0 โ‰ค ๐‘›) โ†’ (absโ€˜๐‘›) = ๐‘›)
242240, 241syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜๐‘›) = ๐‘›)
243242oveq2d 7424 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท (absโ€˜๐‘›)) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›))
244237, 239, 2433eqtrd 2776 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›))
245 fveq2 6891 . . . . . . . . . . . . . . . . 17 (๐‘ข = (๐‘ / ๐‘›) โ†’ (๐‘…โ€˜๐‘ข) = (๐‘…โ€˜(๐‘ / ๐‘›)))
246 id 22 . . . . . . . . . . . . . . . . 17 (๐‘ข = (๐‘ / ๐‘›) โ†’ ๐‘ข = (๐‘ / ๐‘›))
247245, 246oveq12d 7426 . . . . . . . . . . . . . . . 16 (๐‘ข = (๐‘ / ๐‘›) โ†’ ((๐‘…โ€˜๐‘ข) / ๐‘ข) = ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)))
248247fveq2d 6895 . . . . . . . . . . . . . . 15 (๐‘ข = (๐‘ / ๐‘›) โ†’ (absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) = (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))))
249248breq1d 5158 . . . . . . . . . . . . . 14 (๐‘ข = (๐‘ / ๐‘›) โ†’ ((absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ โ†” (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) โ‰ค ๐ธ))
25088simprd 496 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ)
251250adantr 481 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ)
25230adantr 481 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ โˆˆ โ„)
253252, 120nndivred 12265 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โˆˆ โ„)
25444rpregt0d 13021 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰))
255254adantr 481 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰))
256 lemuldiv2 12094 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰)) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘› โ‰ค (๐‘ / ๐‘‰)))
257137, 252, 255, 256syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘› โ‰ค (๐‘ / ๐‘‰)))
258136, 257mpbird 256 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‰ ยท ๐‘›) โ‰ค ๐‘)
259255simpld 495 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โˆˆ โ„)
260259, 252, 121lemuldivd 13064 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘‰ โ‰ค (๐‘ / ๐‘›)))
261258, 260mpbid 231 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โ‰ค (๐‘ / ๐‘›))
262111rpregt0d 13021 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
263262adantr 481 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
264121rpregt0d 13021 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„ โˆง 0 < ๐‘›))
265 lediv23 12105 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„ โˆง (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆง (๐‘› โˆˆ โ„ โˆง 0 < ๐‘›)) โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘› โ†” (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
266252, 263, 264, 265syl3anc 1371 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘› โ†” (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
267189, 266mpbid 231 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))
26844rpred 13015 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„)
269268adantr 481 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โˆˆ โ„)
270146adantr 481 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„)
271 elicc2 13388 . . . . . . . . . . . . . . . 16 ((๐‘‰ โˆˆ โ„ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„) โ†’ ((๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ†” ((๐‘ / ๐‘›) โˆˆ โ„ โˆง ๐‘‰ โ‰ค (๐‘ / ๐‘›) โˆง (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
272269, 270, 271syl2anc 584 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ†” ((๐‘ / ๐‘›) โˆˆ โ„ โˆง ๐‘‰ โ‰ค (๐‘ / ๐‘›) โˆง (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
273253, 261, 267, 272mpbir3and 1342 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
274249, 251, 273rspcdva 3613 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) โ‰ค ๐ธ)
275244, 274eqbrtrrd 5172 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›) โ‰ค ๐ธ)
276224, 220, 121lemuldivd 13064 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›) โ‰ค ๐ธ โ†” (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โ‰ค (๐ธ / ๐‘›)))
277275, 276mpbid 231 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โ‰ค (๐ธ / ๐‘›))
278224, 225, 226, 277lesub2dd 11830 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)) โ‰ค ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))))
279223, 278eqbrtrd 5170 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) โ‰ค ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))))
280209, 210, 122, 216, 279lemul1ad 12152 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
281207, 280eqbrtrrd 5172 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
28299, 124, 126, 198, 281letrd 11370 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
283282adantlr 713 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
28469nnred 12226 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„)
28529, 151rpdivcld 13032 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„+)
286285rpred 13015 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„)
287286adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„)
28823simpld 495 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„+)
28929, 288rpdivcld 13032 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„+)
290289rpred 13015 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„)
291290adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„)
292 simpr 485 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ ๐‘‚)
293292, 50eleqtrdi 2843 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
294 elfzle2 13504 . . . . . . . . . . 11 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
295293, 294syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
29669nnzd 12584 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„ค)
297 flge 13769 . . . . . . . . . . 11 (((๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„ โˆง ๐‘› โˆˆ โ„ค) โ†’ (๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
298287, 296, 297syl2anc 584 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
299295, 298mpbird 256 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)))
300288rpred 13015 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
30124simpld 495 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„+)
302301rpred 13015 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
303151rpred 13015 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„)
30424simprd 496 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘Œ < ๐‘‹)
305300, 302, 304ltled 11361 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โ‰ค ๐‘‹)
306 elfzofz 13647 . . . . . . . . . . . . . . . 16 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ (๐‘€...๐‘))
30756, 306syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐‘€...๐‘))
3081, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 27099 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐ฝ โˆˆ (๐‘€...๐‘)) โ†’ (๐‘‹ < (๐พโ†‘๐ฝ) โˆง (๐พโ†‘๐ฝ) โ‰ค (โˆšโ€˜๐‘)))
309307, 308mpdan 685 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‹ < (๐พโ†‘๐ฝ) โˆง (๐พโ†‘๐ฝ) โ‰ค (โˆšโ€˜๐‘)))
310309simpld 495 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‹ < (๐พโ†‘๐ฝ))
311302, 303, 310ltled 11361 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โ‰ค (๐พโ†‘๐ฝ))
312300, 302, 303, 305, 311letrd 11370 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โ‰ค (๐พโ†‘๐ฝ))
313288, 151, 29lediv2d 13039 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘Œ โ‰ค (๐พโ†‘๐ฝ) โ†” (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ)))
314312, 313mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ))
315314adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ))
316284, 287, 291, 299, 315letrd 11370 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (๐‘ / ๐‘Œ))
31769, 316jca 512 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘› โˆˆ โ„• โˆง ๐‘› โ‰ค (๐‘ / ๐‘Œ)))
3181, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86pntlemn 27100 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โ‰ค (๐‘ / ๐‘Œ))) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
319317, 318syldan 591 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
320319adantr 481 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ยฌ ๐‘› โˆˆ ๐ผ) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
321103, 104, 283, 320ifbothda 4566 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32252, 102, 82, 321fsumle 15744 . . 3 (๐œ‘ โ†’ ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32398, 322eqbrtrd 5170 . 2 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32436, 49, 83, 89, 323letrd 11370 1 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070   โŠ† wss 3948  ifcif 4528   class class class wbr 5148   โ†ฆ cmpt 5231  โ€˜cfv 6543  (class class class)co 7408  Fincfn 8938  โ„‚cc 11107  โ„cr 11108  0cc0 11109  1c1 11110   + caddc 11112   ยท cmul 11114  +โˆžcpnf 11244   < clt 11247   โ‰ค cle 11248   โˆ’ cmin 11443   / cdiv 11870  โ„•cn 12211  2c2 12266  3c3 12267  4c4 12268  8c8 12272  โ„•0cn0 12471  โ„คcz 12557  cdc 12676  โ„คโ‰ฅcuz 12821  โ„+crp 12973  (,)cioo 13323  [,)cico 13325  [,]cicc 13326  ...cfz 13483  ..^cfzo 13626  โŒŠcfl 13754  โ†‘cexp 14026  โ™ฏchash 14289  โˆšcsqrt 15179  abscabs 15180  ฮฃcsu 15631  expce 16004  eceu 16005  logclog 26062  ฯˆcchp 26594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-inf2 9635  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187  ax-addf 11188  ax-mulf 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7669  df-om 7855  df-1st 7974  df-2nd 7975  df-supp 8146  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-2o 8466  df-oadd 8469  df-er 8702  df-map 8821  df-pm 8822  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-fi 9405  df-sup 9436  df-inf 9437  df-oi 9504  df-dju 9895  df-card 9933  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12472  df-z 12558  df-dec 12677  df-uz 12822  df-q 12932  df-rp 12974  df-xneg 13091  df-xadd 13092  df-xmul 13093  df-ioo 13327  df-ioc 13328  df-ico 13329  df-icc 13330  df-fz 13484  df-fzo 13627  df-fl 13756  df-mod 13834  df-seq 13966  df-exp 14027  df-fac 14233  df-bc 14262  df-hash 14290  df-shft 15013  df-cj 15045  df-re 15046  df-im 15047  df-sqrt 15181  df-abs 15182  df-limsup 15414  df-clim 15431  df-rlim 15432  df-sum 15632  df-ef 16010  df-e 16011  df-sin 16012  df-cos 16013  df-pi 16015  df-dvds 16197  df-gcd 16435  df-prm 16608  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 18560  df-sgrp 18609  df-mnd 18625  df-submnd 18671  df-mulg 18950  df-cntz 19180  df-cmn 19649  df-psmet 20935  df-xmet 20936  df-met 20937  df-bl 20938  df-mopn 20939  df-fbas 20940  df-fg 20941  df-cnfld 20944  df-top 22395  df-topon 22412  df-topsp 22434  df-bases 22448  df-cld 22522  df-ntr 22523  df-cls 22524  df-nei 22601  df-lp 22639  df-perf 22640  df-cn 22730  df-cnp 22731  df-haus 22818  df-tx 23065  df-hmeo 23258  df-fil 23349  df-fm 23441  df-flim 23442  df-flf 23443  df-xms 23825  df-ms 23826  df-tms 23827  df-cncf 24393  df-limc 25382  df-dv 25383  df-log 26064  df-vma 26599  df-chp 26600
This theorem is referenced by:  pntlemi  27104
  Copyright terms: Public domain W3C validator