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

Theorem pntlemj 26967
Description: Lemma for pnt 26978. The induction step. Using pntibnd 26957, 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 26959 . . . . . 6 (๐œ‘ โ†’ (๐ธ โˆˆ โ„+ โˆง ๐พ โˆˆ โ„+ โˆง (๐ธ โˆˆ (0(,)1) โˆง 1 < ๐พ โˆง (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+)))
1211simp3d 1145 . . . . 5 (๐œ‘ โ†’ (๐ธ โˆˆ (0(,)1) โˆง 1 < ๐พ โˆง (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+))
1312simp3d 1145 . . . 4 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+)
141, 2, 3, 4, 5, 6pntlemd 26958 . . . . . . . 8 (๐œ‘ โ†’ (๐ฟ โˆˆ โ„+ โˆง ๐ท โˆˆ โ„+ โˆง ๐น โˆˆ โ„+))
1514simp1d 1143 . . . . . . 7 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„+)
1611simp1d 1143 . . . . . . 7 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
1715, 16rpmulcld 12978 . . . . . 6 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) โˆˆ โ„+)
18 8nn 12253 . . . . . . 7 8 โˆˆ โ„•
19 nnrp 12931 . . . . . . 7 (8 โˆˆ โ„• โ†’ 8 โˆˆ โ„+)
2018, 19ax-mp 5 . . . . . 6 8 โˆˆ โ„+
21 rpdivcl 12945 . . . . . 6 (((๐ฟ ยท ๐ธ) โˆˆ โ„+ โˆง 8 โˆˆ โ„+) โ†’ ((๐ฟ ยท ๐ธ) / 8) โˆˆ โ„+)
2217, 20, 21sylancl 587 . . . . 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 26961 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ โˆˆ โ„+ โˆง (1 < ๐‘ โˆง e โ‰ค (โˆšโ€˜๐‘) โˆง (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘Œ)) โˆง ((4 / (๐ฟ ยท ๐ธ)) โ‰ค (โˆšโ€˜๐‘) โˆง (((logโ€˜๐‘‹) / (logโ€˜๐พ)) + 2) โ‰ค (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โˆง ((๐‘ˆ ยท 3) + ๐ถ) โ‰ค (((๐‘ˆ โˆ’ ๐ธ) ยท ((๐ฟ ยท (๐ธโ†‘2)) / (32 ยท ๐ต))) ยท (logโ€˜๐‘)))))
2928simp1d 1143 . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ โ„+)
3029rpred 12962 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
3128simp2d 1144 . . . . . . 7 (๐œ‘ โ†’ (1 < ๐‘ โˆง e โ‰ค (โˆšโ€˜๐‘) โˆง (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘Œ)))
3231simp1d 1143 . . . . . 6 (๐œ‘ โ†’ 1 < ๐‘)
3330, 32rplogcld 26000 . . . . 5 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„+)
3422, 33rpmulcld 12978 . . . 4 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)) โˆˆ โ„+)
3513, 34rpmulcld 12978 . . 3 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โˆˆ โ„+)
3635rpred 12962 . 2 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โˆˆ โ„)
37 pntlem1.i . . . . . 6 ๐ผ = (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰)))
38 fzfid 13884 . . . . . 6 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โˆˆ Fin)
3937, 38eqeltrid 2838 . . . . 5 (๐œ‘ โ†’ ๐ผ โˆˆ Fin)
40 hashcl 14262 . . . . 5 (๐ผ โˆˆ Fin โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„•0)
4139, 40syl 17 . . . 4 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„•0)
4241nn0red 12479 . . 3 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„)
4313rpred 12962 . . . 4 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
44 pntlem1.v . . . . . . 7 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„+)
4529, 44rpdivcld 12979 . . . . . 6 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„+)
4645relogcld 25994 . . . . 5 (๐œ‘ โ†’ (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„)
4746, 45rerpdivcld 12993 . . . 4 (๐œ‘ โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„)
4843, 47remulcld 11190 . . 3 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
4942, 48remulcld 11190 . 2 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) โˆˆ โ„)
50 pntlem1.o . . . 4 ๐‘‚ = (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
51 fzfid 13884 . . . 4 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โˆˆ Fin)
5250, 51eqeltrid 2838 . . 3 (๐œ‘ โ†’ ๐‘‚ โˆˆ Fin)
537rpred 12962 . . . . . . 7 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„)
5453adantr 482 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘ˆ โˆˆ โ„)
5511simp2d 1144 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐พ โˆˆ โ„+)
56 pntlem1.j . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐‘€..^๐‘))
57 elfzoelz 13578 . . . . . . . . . . . . 13 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ โ„ค)
5856, 57syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค)
5958peano2zd 12615 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฝ + 1) โˆˆ โ„ค)
6055, 59rpexpcld 14156 . . . . . . . . . 10 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โˆˆ โ„+)
6129, 60rpdivcld 12979 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„+)
6261rprege0d 12969 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / (๐พโ†‘(๐ฝ + 1)))))
63 flge0nn0 13731 . . . . . . . 8 (((๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / (๐พโ†‘(๐ฝ + 1)))) โ†’ (โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) โˆˆ โ„•0)
64 nn0p1nn 12457 . . . . . . . 8 ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) โˆˆ โ„•0 โ†’ ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„•)
6562, 63, 643syl 18 . . . . . . 7 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„•)
66 elfzuz 13443 . . . . . . . 8 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)))
6766, 50eleq2s 2852 . . . . . . 7 (๐‘› โˆˆ ๐‘‚ โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)))
68 eluznn 12848 . . . . . . 7 ((((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„• โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1))) โ†’ ๐‘› โˆˆ โ„•)
6965, 67, 68syl2an 597 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„•)
7054, 69nndivred 12212 . . . . 5 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ˆ / ๐‘›) โˆˆ โ„)
7129adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘ โˆˆ โ„+)
7269nnrpd 12960 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„+)
7371, 72rpdivcld 12979 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / ๐‘›) โˆˆ โ„+)
741pntrf 26927 . . . . . . . . . 10 ๐‘…:โ„+โŸถโ„
7574ffvelcdmi 7035 . . . . . . . . 9 ((๐‘ / ๐‘›) โˆˆ โ„+ โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
7673, 75syl 17 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
7776, 71rerpdivcld 12993 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„)
7877recnd 11188 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„‚)
7978abscld 15327 . . . . 5 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โˆˆ โ„)
8070, 79resubcld 11588 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) โˆˆ โ„)
8172relogcld 25994 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
8280, 81remulcld 11190 . . 3 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โˆˆ โ„)
8352, 82fsumrecl 15624 . 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 26966 . 2 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
9048recnd 11188 . . . . 5 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚)
91 fsumconst 15680 . . . . 5 ((๐ผ โˆˆ Fin โˆง ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚) โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
9239, 90, 91syl2anc 585 . . . 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 26965 . . . . 5 (๐œ‘ โ†’ ๐ผ โŠ† ๐‘‚)
9490ralrimivw 3144 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚)
9552olcd 873 . . . . 5 (๐œ‘ โ†’ (๐‘‚ โŠ† (โ„คโ‰ฅโ€˜1) โˆจ ๐‘‚ โˆˆ Fin))
96 sumss2 15616 . . . . 5 (((๐ผ โŠ† ๐‘‚ โˆง โˆ€๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚) โˆง (๐‘‚ โŠ† (โ„คโ‰ฅโ€˜1) โˆจ ๐‘‚ โˆˆ Fin)) โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9793, 94, 95, 96syl21anc 837 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9892, 97eqtr3d 2775 . . 3 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9948adantr 482 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
10099adantlr 714 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
101 0red 11163 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ยฌ ๐‘› โˆˆ ๐ผ) โ†’ 0 โˆˆ โ„)
102100, 101ifclda 4522 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โˆˆ โ„)
103 breq1 5109 . . . . 5 (((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โ†” if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›))))
104 breq1 5109 . . . . 5 (0 = if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ†’ (0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โ†” if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›))))
10513rpregt0d 12968 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ)))
106105adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ)))
107106simpld 496 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
108 1rp 12924 . . . . . . . . . . . . . . . . 17 1 โˆˆ โ„+
109 rpaddcl 12942 . . . . . . . . . . . . . . . . 17 ((1 โˆˆ โ„+ โˆง (๐ฟ ยท ๐ธ) โˆˆ โ„+) โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
110108, 17, 109sylancr 588 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
111110, 44rpmulcld 12978 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„+)
11229, 111rpdivcld 12979 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„+)
113112rprege0d 12969 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
114 flge0nn0 13731 . . . . . . . . . . . . 13 (((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„•0)
115 nn0p1nn 12457 . . . . . . . . . . . . 13 ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„•0 โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„•)
116113, 114, 1153syl 18 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„•)
117 elfzuz 13443 . . . . . . . . . . . . 13 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
118117, 37eleq2s 2852 . . . . . . . . . . . 12 (๐‘› โˆˆ ๐ผ โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
119 eluznn 12848 . . . . . . . . . . . 12 ((((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„• โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))) โ†’ ๐‘› โˆˆ โ„•)
120116, 118, 119syl2an 597 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„•)
121120nnrpd 12960 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„+)
122121relogcld 25994 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
123122, 120nndivred 12212 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜๐‘›) / ๐‘›) โˆˆ โ„)
124107, 123remulcld 11190 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)) โˆˆ โ„)
12593sselda 3945 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ ๐‘‚)
126125, 82syldan 592 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โˆˆ โ„)
127 simpr 486 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ ๐ผ)
128127, 37eleqtrdi 2844 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))))
129 elfzle2 13451 . . . . . . . . . . 11 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰)))
130128, 129syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰)))
13145rpred 12962 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„)
132131adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘‰) โˆˆ โ„)
133128elfzelzd 13448 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„ค)
134 flge 13716 . . . . . . . . . . 11 (((๐‘ / ๐‘‰) โˆˆ โ„ โˆง ๐‘› โˆˆ โ„ค) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰))))
135132, 133, 134syl2anc 585 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰))))
136130, 135mpbird 257 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โ‰ค (๐‘ / ๐‘‰))
137120nnred 12173 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„)
138 ere 15976 . . . . . . . . . . . 12 e โˆˆ โ„
139138a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โˆˆ โ„)
140112rpred 12962 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„)
141140adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„)
142138a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ e โˆˆ โ„)
14329rpsqrtcld 15302 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„+)
144143rpred 12962 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„)
14531simp2d 1144 . . . . . . . . . . . . 13 (๐œ‘ โ†’ e โ‰ค (โˆšโ€˜๐‘))
146111rpred 12962 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„)
14760rpred 12962 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โˆˆ โ„)
14888simpld 496 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((๐พโ†‘๐ฝ) < ๐‘‰ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ))))
149148simprd 497 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ)))
15055rpcnd 12964 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐พ โˆˆ โ„‚)
15155, 58rpexpcld 14156 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„+)
152151rpcnd 12964 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„‚)
153150, 152mulcomd 11181 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐พ ยท (๐พโ†‘๐ฝ)) = ((๐พโ†‘๐ฝ) ยท ๐พ))
1541, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemg 26962 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โ‰ค (๐‘ โˆ’ ๐‘€)))
155154simp1d 1143 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
156 elfzouz 13582 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
15756, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
158 eluznn 12848 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘€ โˆˆ โ„• โˆง ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐ฝ โˆˆ โ„•)
159155, 157, 158syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•)
160159nnnn0d 12478 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•0)
161150, 160expp1d 14058 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) = ((๐พโ†‘๐ฝ) ยท ๐พ))
162153, 161eqtr4d 2776 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐พ ยท (๐พโ†‘๐ฝ)) = (๐พโ†‘(๐ฝ + 1)))
163149, 162breqtrd 5132 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พโ†‘(๐ฝ + 1)))
164146, 147, 163ltled 11308 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (๐พโ†‘(๐ฝ + 1)))
165 fzofzp1 13675 . . . . . . . . . . . . . . . . . . . 20 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ (๐ฝ + 1) โˆˆ (๐‘€...๐‘))
16656, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ฝ + 1) โˆˆ (๐‘€...๐‘))
1671, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 26963 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐ฝ + 1) โˆˆ (๐‘€...๐‘)) โ†’ (๐‘‹ < (๐พโ†‘(๐ฝ + 1)) โˆง (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘)))
168166, 167mpdan 686 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘‹ < (๐พโ†‘(๐ฝ + 1)) โˆง (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘)))
169168simprd 497 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘))
170146, 147, 144, 164, 169letrd 11317 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (โˆšโ€˜๐‘))
171146, 144, 143lemul2d 13006 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (โˆšโ€˜๐‘) โ†” ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘))))
172170, 171mpbid 231 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)))
17329rprege0d 12969 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘))
174 remsqsqrt 15147 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘) โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
175173, 174syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
176172, 175breqtrd 5132 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘)
177144, 30, 111lemuldivd 13011 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘ โ†” (โˆšโ€˜๐‘) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
178176, 177mpbid 231 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
179142, 144, 140, 145, 178letrd 11317 . . . . . . . . . . . 12 (๐œ‘ โ†’ e โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
180179adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
181 reflcl 13707 . . . . . . . . . . . . . 14 ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„)
182 peano2re 11333 . . . . . . . . . . . . . 14 ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
183140, 181, 1823syl 18 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
184183adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
185 fllep1 13712 . . . . . . . . . . . . 13 ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))
186141, 185syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))
187 elfzle1 13450 . . . . . . . . . . . . 13 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โ‰ค ๐‘›)
188128, 187syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โ‰ค ๐‘›)
189141, 184, 137, 186, 188letrd 11317 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘›)
190139, 141, 137, 180, 189letrd 11317 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค ๐‘›)
191139, 137, 132, 190, 136letrd 11317 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค (๐‘ / ๐‘‰))
192 logdivle 25993 . . . . . . . . . 10 (((๐‘› โˆˆ โ„ โˆง e โ‰ค ๐‘›) โˆง ((๐‘ / ๐‘‰) โˆˆ โ„ โˆง e โ‰ค (๐‘ / ๐‘‰))) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›)))
193137, 190, 132, 191, 192syl22anc 838 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›)))
194136, 193mpbid 231 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›))
19547adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„)
196 lemul2 12013 . . . . . . . . 9 ((((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„ โˆง ((logโ€˜๐‘›) / ๐‘›) โˆˆ โ„ โˆง ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ))) โ†’ (((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›) โ†” ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›))))
197195, 123, 106, 196syl3anc 1372 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›) โ†” ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›))))
198194, 197mpbid 231 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
19913rpcnd 12964 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚)
200199adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚)
201122recnd 11188 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜๐‘›) โˆˆ โ„‚)
202121rpcnne0d 12971 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0))
203 div23 11837 . . . . . . . . . 10 (((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚ โˆง (logโ€˜๐‘›) โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)))
204200, 201, 202, 203syl3anc 1372 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)))
205 divass 11836 . . . . . . . . . 10 (((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚ โˆง (logโ€˜๐‘›) โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
206200, 201, 202, 205syl3anc 1372 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
207204, 206eqtr3d 2775 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
20843adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
209208, 120nndivred 12212 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) โˆˆ โ„)
210125, 80syldan 592 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) โˆˆ โ„)
211 log1 25957 . . . . . . . . . 10 (logโ€˜1) = 0
212120nnge1d 12206 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ 1 โ‰ค ๐‘›)
213 logleb 25974 . . . . . . . . . . . 12 ((1 โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โ†’ (1 โ‰ค ๐‘› โ†” (logโ€˜1) โ‰ค (logโ€˜๐‘›)))
214108, 121, 213sylancr 588 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (1 โ‰ค ๐‘› โ†” (logโ€˜1) โ‰ค (logโ€˜๐‘›)))
215212, 214mpbid 231 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜1) โ‰ค (logโ€˜๐‘›))
216211, 215eqbrtrrid 5142 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ 0 โ‰ค (logโ€˜๐‘›))
2177rpcnd 12964 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„‚)
218217adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ˆ โˆˆ โ„‚)
21916rpred 12962 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
220219adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐ธ โˆˆ โ„)
221220recnd 11188 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐ธ โˆˆ โ„‚)
222 divsubdir 11854 . . . . . . . . . . 11 ((๐‘ˆ โˆˆ โ„‚ โˆง ๐ธ โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) = ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)))
223218, 221, 202, 222syl3anc 1372 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) = ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)))
224125, 79syldan 592 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โˆˆ โ„)
225220, 120nndivred 12212 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐ธ / ๐‘›) โˆˆ โ„)
226125, 70syldan 592 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ / ๐‘›) โˆˆ โ„)
227125, 76syldan 592 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
228227recnd 11188 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚)
22929adantr 482 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ โˆˆ โ„+)
230229rpcnne0d 12971 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0))
231 divdiv2 11872 . . . . . . . . . . . . . . . . 17 (((๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚ โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0) โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘))
232228, 230, 202, 231syl3anc 1372 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘))
233121rpcnd 12964 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„‚)
234 div23 11837 . . . . . . . . . . . . . . . . 17 (((๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚ โˆง ๐‘› โˆˆ โ„‚ โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0)) โ†’ (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
235228, 233, 230, 234syl3anc 1372 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
236232, 235eqtrd 2773 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
237236fveq2d 6847 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) = (absโ€˜(((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›)))
238125, 78syldan 592 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„‚)
239238, 233absmuld 15345 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜(((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›)) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท (absโ€˜๐‘›)))
240121rprege0d 12969 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„ โˆง 0 โ‰ค ๐‘›))
241 absid 15187 . . . . . . . . . . . . . . . 16 ((๐‘› โˆˆ โ„ โˆง 0 โ‰ค ๐‘›) โ†’ (absโ€˜๐‘›) = ๐‘›)
242240, 241syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜๐‘›) = ๐‘›)
243242oveq2d 7374 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท (absโ€˜๐‘›)) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›))
244237, 239, 2433eqtrd 2777 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›))
245 fveq2 6843 . . . . . . . . . . . . . . . . 17 (๐‘ข = (๐‘ / ๐‘›) โ†’ (๐‘…โ€˜๐‘ข) = (๐‘…โ€˜(๐‘ / ๐‘›)))
246 id 22 . . . . . . . . . . . . . . . . 17 (๐‘ข = (๐‘ / ๐‘›) โ†’ ๐‘ข = (๐‘ / ๐‘›))
247245, 246oveq12d 7376 . . . . . . . . . . . . . . . 16 (๐‘ข = (๐‘ / ๐‘›) โ†’ ((๐‘…โ€˜๐‘ข) / ๐‘ข) = ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)))
248247fveq2d 6847 . . . . . . . . . . . . . . 15 (๐‘ข = (๐‘ / ๐‘›) โ†’ (absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) = (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))))
249248breq1d 5116 . . . . . . . . . . . . . 14 (๐‘ข = (๐‘ / ๐‘›) โ†’ ((absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ โ†” (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) โ‰ค ๐ธ))
25088simprd 497 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ)
251250adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ)
25230adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ โˆˆ โ„)
253252, 120nndivred 12212 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โˆˆ โ„)
25444rpregt0d 12968 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰))
255254adantr 482 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰))
256 lemuldiv2 12041 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰)) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘› โ‰ค (๐‘ / ๐‘‰)))
257137, 252, 255, 256syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘› โ‰ค (๐‘ / ๐‘‰)))
258136, 257mpbird 257 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‰ ยท ๐‘›) โ‰ค ๐‘)
259255simpld 496 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โˆˆ โ„)
260259, 252, 121lemuldivd 13011 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘‰ โ‰ค (๐‘ / ๐‘›)))
261258, 260mpbid 231 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โ‰ค (๐‘ / ๐‘›))
262111rpregt0d 12968 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
263262adantr 482 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
264121rpregt0d 12968 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„ โˆง 0 < ๐‘›))
265 lediv23 12052 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„ โˆง (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆง (๐‘› โˆˆ โ„ โˆง 0 < ๐‘›)) โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘› โ†” (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
266252, 263, 264, 265syl3anc 1372 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘› โ†” (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
267189, 266mpbid 231 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))
26844rpred 12962 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„)
269268adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โˆˆ โ„)
270146adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„)
271 elicc2 13335 . . . . . . . . . . . . . . . 16 ((๐‘‰ โˆˆ โ„ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„) โ†’ ((๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ†” ((๐‘ / ๐‘›) โˆˆ โ„ โˆง ๐‘‰ โ‰ค (๐‘ / ๐‘›) โˆง (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
272269, 270, 271syl2anc 585 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ†” ((๐‘ / ๐‘›) โˆˆ โ„ โˆง ๐‘‰ โ‰ค (๐‘ / ๐‘›) โˆง (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
273253, 261, 267, 272mpbir3and 1343 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
274249, 251, 273rspcdva 3581 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) โ‰ค ๐ธ)
275244, 274eqbrtrrd 5130 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›) โ‰ค ๐ธ)
276224, 220, 121lemuldivd 13011 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›) โ‰ค ๐ธ โ†” (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โ‰ค (๐ธ / ๐‘›)))
277275, 276mpbid 231 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โ‰ค (๐ธ / ๐‘›))
278224, 225, 226, 277lesub2dd 11777 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)) โ‰ค ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))))
279223, 278eqbrtrd 5128 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) โ‰ค ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))))
280209, 210, 122, 216, 279lemul1ad 12099 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
281207, 280eqbrtrrd 5130 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
28299, 124, 126, 198, 281letrd 11317 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
283282adantlr 714 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
28469nnred 12173 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„)
28529, 151rpdivcld 12979 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„+)
286285rpred 12962 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„)
287286adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„)
28823simpld 496 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„+)
28929, 288rpdivcld 12979 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„+)
290289rpred 12962 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„)
291290adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„)
292 simpr 486 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ ๐‘‚)
293292, 50eleqtrdi 2844 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
294 elfzle2 13451 . . . . . . . . . . 11 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
295293, 294syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
29669nnzd 12531 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„ค)
297 flge 13716 . . . . . . . . . . 11 (((๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„ โˆง ๐‘› โˆˆ โ„ค) โ†’ (๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
298287, 296, 297syl2anc 585 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
299295, 298mpbird 257 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)))
300288rpred 12962 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
30124simpld 496 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„+)
302301rpred 12962 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
303151rpred 12962 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„)
30424simprd 497 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘Œ < ๐‘‹)
305300, 302, 304ltled 11308 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โ‰ค ๐‘‹)
306 elfzofz 13594 . . . . . . . . . . . . . . . 16 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ (๐‘€...๐‘))
30756, 306syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐‘€...๐‘))
3081, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 26963 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐ฝ โˆˆ (๐‘€...๐‘)) โ†’ (๐‘‹ < (๐พโ†‘๐ฝ) โˆง (๐พโ†‘๐ฝ) โ‰ค (โˆšโ€˜๐‘)))
309307, 308mpdan 686 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‹ < (๐พโ†‘๐ฝ) โˆง (๐พโ†‘๐ฝ) โ‰ค (โˆšโ€˜๐‘)))
310309simpld 496 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‹ < (๐พโ†‘๐ฝ))
311302, 303, 310ltled 11308 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โ‰ค (๐พโ†‘๐ฝ))
312300, 302, 303, 305, 311letrd 11317 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โ‰ค (๐พโ†‘๐ฝ))
313288, 151, 29lediv2d 12986 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘Œ โ‰ค (๐พโ†‘๐ฝ) โ†” (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ)))
314312, 313mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ))
315314adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ))
316284, 287, 291, 299, 315letrd 11317 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (๐‘ / ๐‘Œ))
31769, 316jca 513 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘› โˆˆ โ„• โˆง ๐‘› โ‰ค (๐‘ / ๐‘Œ)))
3181, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86pntlemn 26964 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โ‰ค (๐‘ / ๐‘Œ))) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
319317, 318syldan 592 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
320319adantr 482 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ยฌ ๐‘› โˆˆ ๐ผ) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
321103, 104, 283, 320ifbothda 4525 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32252, 102, 82, 321fsumle 15689 . . 3 (๐œ‘ โ†’ ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32398, 322eqbrtrd 5128 . 2 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32436, 49, 83, 89, 323letrd 11317 1 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070   โŠ† wss 3911  ifcif 4487   class class class wbr 5106   โ†ฆ cmpt 5189  โ€˜cfv 6497  (class class class)co 7358  Fincfn 8886  โ„‚cc 11054  โ„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   ยท cmul 11061  +โˆžcpnf 11191   < clt 11194   โ‰ค cle 11195   โˆ’ cmin 11390   / cdiv 11817  โ„•cn 12158  2c2 12213  3c3 12214  4c4 12215  8c8 12219  โ„•0cn0 12418  โ„คcz 12504  cdc 12623  โ„คโ‰ฅcuz 12768  โ„+crp 12920  (,)cioo 13270  [,)cico 13272  [,]cicc 13273  ...cfz 13430  ..^cfzo 13573  โŒŠcfl 13701  โ†‘cexp 13973  โ™ฏchash 14236  โˆšcsqrt 15124  abscabs 15125  ฮฃcsu 15576  expce 15949  eceu 15950  logclog 25926  ฯˆcchp 26458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-dju 9842  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577  df-ef 15955  df-e 15956  df-sin 15957  df-cos 15958  df-pi 15960  df-dvds 16142  df-gcd 16380  df-prm 16553  df-pc 16714  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-vma 26463  df-chp 26464
This theorem is referenced by:  pntlemi  26968
  Copyright terms: Public domain W3C validator