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

Theorem pntlemj 27449
Description: Lemma for pnt 27460. The induction step. Using pntibnd 27439, 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 27441 . . . . . 6 (๐œ‘ โ†’ (๐ธ โˆˆ โ„+ โˆง ๐พ โˆˆ โ„+ โˆง (๐ธ โˆˆ (0(,)1) โˆง 1 < ๐พ โˆง (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+)))
1211simp3d 1143 . . . . 5 (๐œ‘ โ†’ (๐ธ โˆˆ (0(,)1) โˆง 1 < ๐พ โˆง (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+))
1312simp3d 1143 . . . 4 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+)
141, 2, 3, 4, 5, 6pntlemd 27440 . . . . . . . 8 (๐œ‘ โ†’ (๐ฟ โˆˆ โ„+ โˆง ๐ท โˆˆ โ„+ โˆง ๐น โˆˆ โ„+))
1514simp1d 1141 . . . . . . 7 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„+)
1611simp1d 1141 . . . . . . 7 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
1715, 16rpmulcld 13039 . . . . . 6 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) โˆˆ โ„+)
18 8nn 12314 . . . . . . 7 8 โˆˆ โ„•
19 nnrp 12992 . . . . . . 7 (8 โˆˆ โ„• โ†’ 8 โˆˆ โ„+)
2018, 19ax-mp 5 . . . . . 6 8 โˆˆ โ„+
21 rpdivcl 13006 . . . . . 6 (((๐ฟ ยท ๐ธ) โˆˆ โ„+ โˆง 8 โˆˆ โ„+) โ†’ ((๐ฟ ยท ๐ธ) / 8) โˆˆ โ„+)
2217, 20, 21sylancl 585 . . . . 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 27443 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ โˆˆ โ„+ โˆง (1 < ๐‘ โˆง e โ‰ค (โˆšโ€˜๐‘) โˆง (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘Œ)) โˆง ((4 / (๐ฟ ยท ๐ธ)) โ‰ค (โˆšโ€˜๐‘) โˆง (((logโ€˜๐‘‹) / (logโ€˜๐พ)) + 2) โ‰ค (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โˆง ((๐‘ˆ ยท 3) + ๐ถ) โ‰ค (((๐‘ˆ โˆ’ ๐ธ) ยท ((๐ฟ ยท (๐ธโ†‘2)) / (32 ยท ๐ต))) ยท (logโ€˜๐‘)))))
2928simp1d 1141 . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ โ„+)
3029rpred 13023 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
3128simp2d 1142 . . . . . . 7 (๐œ‘ โ†’ (1 < ๐‘ โˆง e โ‰ค (โˆšโ€˜๐‘) โˆง (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘Œ)))
3231simp1d 1141 . . . . . 6 (๐œ‘ โ†’ 1 < ๐‘)
3330, 32rplogcld 26477 . . . . 5 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„+)
3422, 33rpmulcld 13039 . . . 4 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)) โˆˆ โ„+)
3513, 34rpmulcld 13039 . . 3 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โˆˆ โ„+)
3635rpred 13023 . 2 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โˆˆ โ„)
37 pntlem1.i . . . . . 6 ๐ผ = (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰)))
38 fzfid 13945 . . . . . 6 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โˆˆ Fin)
3937, 38eqeltrid 2836 . . . . 5 (๐œ‘ โ†’ ๐ผ โˆˆ Fin)
40 hashcl 14323 . . . . 5 (๐ผ โˆˆ Fin โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„•0)
4139, 40syl 17 . . . 4 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„•0)
4241nn0red 12540 . . 3 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„)
4313rpred 13023 . . . 4 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
44 pntlem1.v . . . . . . 7 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„+)
4529, 44rpdivcld 13040 . . . . . 6 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„+)
4645relogcld 26471 . . . . 5 (๐œ‘ โ†’ (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„)
4746, 45rerpdivcld 13054 . . . 4 (๐œ‘ โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„)
4843, 47remulcld 11251 . . 3 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
4942, 48remulcld 11251 . 2 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) โˆˆ โ„)
50 pntlem1.o . . . 4 ๐‘‚ = (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
51 fzfid 13945 . . . 4 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โˆˆ Fin)
5250, 51eqeltrid 2836 . . 3 (๐œ‘ โ†’ ๐‘‚ โˆˆ Fin)
537rpred 13023 . . . . . . 7 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„)
5453adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘ˆ โˆˆ โ„)
5511simp2d 1142 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐พ โˆˆ โ„+)
56 pntlem1.j . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐‘€..^๐‘))
57 elfzoelz 13639 . . . . . . . . . . . . 13 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ โ„ค)
5856, 57syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค)
5958peano2zd 12676 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฝ + 1) โˆˆ โ„ค)
6055, 59rpexpcld 14217 . . . . . . . . . 10 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โˆˆ โ„+)
6129, 60rpdivcld 13040 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„+)
6261rprege0d 13030 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / (๐พโ†‘(๐ฝ + 1)))))
63 flge0nn0 13792 . . . . . . . 8 (((๐‘ / (๐พโ†‘(๐ฝ + 1))) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / (๐พโ†‘(๐ฝ + 1)))) โ†’ (โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) โˆˆ โ„•0)
64 nn0p1nn 12518 . . . . . . . 8 ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) โˆˆ โ„•0 โ†’ ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„•)
6562, 63, 643syl 18 . . . . . . 7 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„•)
66 elfzuz 13504 . . . . . . . 8 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)))
6766, 50eleq2s 2850 . . . . . . 7 (๐‘› โˆˆ ๐‘‚ โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)))
68 eluznn 12909 . . . . . . 7 ((((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1) โˆˆ โ„• โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1))) โ†’ ๐‘› โˆˆ โ„•)
6965, 67, 68syl2an 595 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„•)
7054, 69nndivred 12273 . . . . 5 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ˆ / ๐‘›) โˆˆ โ„)
7129adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘ โˆˆ โ„+)
7269nnrpd 13021 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„+)
7371, 72rpdivcld 13040 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / ๐‘›) โˆˆ โ„+)
741pntrf 27409 . . . . . . . . . 10 ๐‘…:โ„+โŸถโ„
7574ffvelcdmi 7085 . . . . . . . . 9 ((๐‘ / ๐‘›) โˆˆ โ„+ โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
7673, 75syl 17 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
7776, 71rerpdivcld 13054 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„)
7877recnd 11249 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„‚)
7978abscld 15390 . . . . 5 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โˆˆ โ„)
8070, 79resubcld 11649 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) โˆˆ โ„)
8172relogcld 26471 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
8280, 81remulcld 11251 . . 3 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โˆˆ โ„)
8352, 82fsumrecl 15687 . 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 27448 . 2 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
9048recnd 11249 . . . . 5 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚)
91 fsumconst 15743 . . . . 5 ((๐ผ โˆˆ Fin โˆง ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚) โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
9239, 90, 91syl2anc 583 . . . 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 27447 . . . . 5 (๐œ‘ โ†’ ๐ผ โІ ๐‘‚)
9490ralrimivw 3149 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚)
9552olcd 871 . . . . 5 (๐œ‘ โ†’ (๐‘‚ โІ (โ„คโ‰ฅโ€˜1) โˆจ ๐‘‚ โˆˆ Fin))
96 sumss2 15679 . . . . 5 (((๐ผ โІ ๐‘‚ โˆง โˆ€๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„‚) โˆง (๐‘‚ โІ (โ„คโ‰ฅโ€˜1) โˆจ ๐‘‚ โˆˆ Fin)) โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9793, 94, 95, 96syl21anc 835 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘› โˆˆ ๐ผ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9892, 97eqtr3d 2773 . . 3 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) = ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0))
9948adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
10099adantlr 712 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
101 0red 11224 . . . . 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 13029 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ)))
106105adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ)))
107106simpld 494 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
108 1rp 12985 . . . . . . . . . . . . . . . . 17 1 โˆˆ โ„+
109 rpaddcl 13003 . . . . . . . . . . . . . . . . 17 ((1 โˆˆ โ„+ โˆง (๐ฟ ยท ๐ธ) โˆˆ โ„+) โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
110108, 17, 109sylancr 586 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
111110, 44rpmulcld 13039 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„+)
11229, 111rpdivcld 13040 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„+)
113112rprege0d 13030 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
114 flge0nn0 13792 . . . . . . . . . . . . 13 (((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โˆง 0 โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„•0)
115 nn0p1nn 12518 . . . . . . . . . . . . 13 ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„•0 โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„•)
116113, 114, 1153syl 18 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„•)
117 elfzuz 13504 . . . . . . . . . . . . 13 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
118117, 37eleq2s 2850 . . . . . . . . . . . 12 (๐‘› โˆˆ ๐ผ โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
119 eluznn 12909 . . . . . . . . . . . 12 ((((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„• โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))) โ†’ ๐‘› โˆˆ โ„•)
120116, 118, 119syl2an 595 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„•)
121120nnrpd 13021 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„+)
122121relogcld 26471 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
123122, 120nndivred 12273 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜๐‘›) / ๐‘›) โˆˆ โ„)
124107, 123remulcld 11251 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)) โˆˆ โ„)
12593sselda 3982 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ ๐‘‚)
126125, 82syldan 590 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)) โˆˆ โ„)
127 simpr 484 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ ๐ผ)
128127, 37eleqtrdi 2842 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))))
129 elfzle2 13512 . . . . . . . . . . 11 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰)))
130128, 129syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰)))
13145rpred 13023 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„)
132131adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘‰) โˆˆ โ„)
133128elfzelzd 13509 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„ค)
134 flge 13777 . . . . . . . . . . 11 (((๐‘ / ๐‘‰) โˆˆ โ„ โˆง ๐‘› โˆˆ โ„ค) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰))))
135132, 133, 134syl2anc 583 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / ๐‘‰))))
136130, 135mpbird 257 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โ‰ค (๐‘ / ๐‘‰))
137120nnred 12234 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„)
138 ere 16039 . . . . . . . . . . . 12 e โˆˆ โ„
139138a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โˆˆ โ„)
140112rpred 13023 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„)
141140adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„)
142138a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ e โˆˆ โ„)
14329rpsqrtcld 15365 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„+)
144143rpred 13023 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„)
14531simp2d 1142 . . . . . . . . . . . . 13 (๐œ‘ โ†’ e โ‰ค (โˆšโ€˜๐‘))
146111rpred 13023 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„)
14760rpred 13023 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โˆˆ โ„)
14888simpld 494 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((๐พโ†‘๐ฝ) < ๐‘‰ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ))))
149148simprd 495 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ)))
15055rpcnd 13025 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐พ โˆˆ โ„‚)
15155, 58rpexpcld 14217 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„+)
152151rpcnd 13025 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„‚)
153150, 152mulcomd 11242 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐พ ยท (๐พโ†‘๐ฝ)) = ((๐พโ†‘๐ฝ) ยท ๐พ))
1541, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemg 27444 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โ‰ค (๐‘ โˆ’ ๐‘€)))
155154simp1d 1141 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
156 elfzouz 13643 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
15756, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
158 eluznn 12909 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘€ โˆˆ โ„• โˆง ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐ฝ โˆˆ โ„•)
159155, 157, 158syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•)
160159nnnn0d 12539 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•0)
161150, 160expp1d 14119 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) = ((๐พโ†‘๐ฝ) ยท ๐พ))
162153, 161eqtr4d 2774 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐พ ยท (๐พโ†‘๐ฝ)) = (๐พโ†‘(๐ฝ + 1)))
163149, 162breqtrd 5174 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พโ†‘(๐ฝ + 1)))
164146, 147, 163ltled 11369 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (๐พโ†‘(๐ฝ + 1)))
165 fzofzp1 13736 . . . . . . . . . . . . . . . . . . . 20 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ (๐ฝ + 1) โˆˆ (๐‘€...๐‘))
16656, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ฝ + 1) โˆˆ (๐‘€...๐‘))
1671, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 27445 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐ฝ + 1) โˆˆ (๐‘€...๐‘)) โ†’ (๐‘‹ < (๐พโ†‘(๐ฝ + 1)) โˆง (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘)))
168166, 167mpdan 684 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘‹ < (๐พโ†‘(๐ฝ + 1)) โˆง (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘)))
169168simprd 495 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘))
170146, 147, 144, 164, 169letrd 11378 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (โˆšโ€˜๐‘))
171146, 144, 143lemul2d 13067 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (โˆšโ€˜๐‘) โ†” ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘))))
172170, 171mpbid 231 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)))
17329rprege0d 13030 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘))
174 remsqsqrt 15210 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘) โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
175173, 174syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
176172, 175breqtrd 5174 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘)
177144, 30, 111lemuldivd 13072 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘ โ†” (โˆšโ€˜๐‘) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
178176, 177mpbid 231 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
179142, 144, 140, 145, 178letrd 11378 . . . . . . . . . . . 12 (๐œ‘ โ†’ e โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
180179adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
181 reflcl 13768 . . . . . . . . . . . . . 14 ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„)
182 peano2re 11394 . . . . . . . . . . . . . 14 ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
183140, 181, 1823syl 18 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
184183adantr 480 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โˆˆ โ„)
185 fllep1 13773 . . . . . . . . . . . . 13 ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))
186141, 185syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1))
187 elfzle1 13511 . . . . . . . . . . . . 13 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โ‰ค ๐‘›)
188128, 187syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1) โ‰ค ๐‘›)
189141, 184, 137, 186, 188letrd 11378 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘›)
190139, 141, 137, 180, 189letrd 11378 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค ๐‘›)
191139, 137, 132, 190, 136letrd 11378 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ e โ‰ค (๐‘ / ๐‘‰))
192 logdivle 26470 . . . . . . . . . 10 (((๐‘› โˆˆ โ„ โˆง e โ‰ค ๐‘›) โˆง ((๐‘ / ๐‘‰) โˆˆ โ„ โˆง e โ‰ค (๐‘ / ๐‘‰))) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›)))
193137, 190, 132, 191, 192syl22anc 836 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โ‰ค (๐‘ / ๐‘‰) โ†” ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›)))
194136, 193mpbid 231 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›))
19547adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„)
196 lemul2 12074 . . . . . . . . 9 ((((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„ โˆง ((logโ€˜๐‘›) / ๐‘›) โˆˆ โ„ โˆง ((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„ โˆง 0 < (๐‘ˆ โˆ’ ๐ธ))) โ†’ (((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›) โ†” ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›))))
197195, 123, 106, 196syl3anc 1370 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โ‰ค ((logโ€˜๐‘›) / ๐‘›) โ†” ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›))))
198194, 197mpbid 231 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
19913rpcnd 13025 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚)
200199adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚)
201122recnd 11249 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜๐‘›) โˆˆ โ„‚)
202121rpcnne0d 13032 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0))
203 div23 11898 . . . . . . . . . 10 (((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚ โˆง (logโ€˜๐‘›) โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)))
204200, 201, 202, 203syl3anc 1370 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)))
205 divass 11897 . . . . . . . . . 10 (((๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚ โˆง (logโ€˜๐‘›) โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
206200, 201, 202, 205syl3anc 1370 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) ยท (logโ€˜๐‘›)) / ๐‘›) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
207204, 206eqtr3d 2773 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)) = ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)))
20843adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„)
209208, 120nndivred 12273 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) โˆˆ โ„)
210125, 80syldan 590 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) โˆˆ โ„)
211 log1 26434 . . . . . . . . . 10 (logโ€˜1) = 0
212120nnge1d 12267 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ 1 โ‰ค ๐‘›)
213 logleb 26451 . . . . . . . . . . . 12 ((1 โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โ†’ (1 โ‰ค ๐‘› โ†” (logโ€˜1) โ‰ค (logโ€˜๐‘›)))
214108, 121, 213sylancr 586 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (1 โ‰ค ๐‘› โ†” (logโ€˜1) โ‰ค (logโ€˜๐‘›)))
215212, 214mpbid 231 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (logโ€˜1) โ‰ค (logโ€˜๐‘›))
216211, 215eqbrtrrid 5184 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ 0 โ‰ค (logโ€˜๐‘›))
2177rpcnd 13025 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„‚)
218217adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ˆ โˆˆ โ„‚)
21916rpred 13023 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
220219adantr 480 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐ธ โˆˆ โ„)
221220recnd 11249 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐ธ โˆˆ โ„‚)
222 divsubdir 11915 . . . . . . . . . . 11 ((๐‘ˆ โˆˆ โ„‚ โˆง ๐ธ โˆˆ โ„‚ โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) = ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)))
223218, 221, 202, 222syl3anc 1370 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) = ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)))
224125, 79syldan 590 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โˆˆ โ„)
225220, 120nndivred 12273 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐ธ / ๐‘›) โˆˆ โ„)
226125, 70syldan 590 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ˆ / ๐‘›) โˆˆ โ„)
227125, 76syldan 590 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„)
228227recnd 11249 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚)
22929adantr 480 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ โˆˆ โ„+)
230229rpcnne0d 13032 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0))
231 divdiv2 11933 . . . . . . . . . . . . . . . . 17 (((๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚ โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0) โˆง (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0)) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘))
232228, 230, 202, 231syl3anc 1370 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘))
233121rpcnd 13025 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘› โˆˆ โ„‚)
234 div23 11898 . . . . . . . . . . . . . . . . 17 (((๐‘…โ€˜(๐‘ / ๐‘›)) โˆˆ โ„‚ โˆง ๐‘› โˆˆ โ„‚ โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0)) โ†’ (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
235228, 233, 230, 234syl3anc 1370 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘…โ€˜(๐‘ / ๐‘›)) ยท ๐‘›) / ๐‘) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
236232, 235eqtrd 2771 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)) = (((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›))
237236fveq2d 6895 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) = (absโ€˜(((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›)))
238125, 78syldan 590 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) โˆˆ โ„‚)
239238, 233absmuld 15408 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜(((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘) ยท ๐‘›)) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท (absโ€˜๐‘›)))
240121rprege0d 13030 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„ โˆง 0 โ‰ค ๐‘›))
241 absid 15250 . . . . . . . . . . . . . . . 16 ((๐‘› โˆˆ โ„ โˆง 0 โ‰ค ๐‘›) โ†’ (absโ€˜๐‘›) = ๐‘›)
242240, 241syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜๐‘›) = ๐‘›)
243242oveq2d 7428 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท (absโ€˜๐‘›)) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›))
244237, 239, 2433eqtrd 2775 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) = ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›))
245 fveq2 6891 . . . . . . . . . . . . . . . . 17 (๐‘ข = (๐‘ / ๐‘›) โ†’ (๐‘…โ€˜๐‘ข) = (๐‘…โ€˜(๐‘ / ๐‘›)))
246 id 22 . . . . . . . . . . . . . . . . 17 (๐‘ข = (๐‘ / ๐‘›) โ†’ ๐‘ข = (๐‘ / ๐‘›))
247245, 246oveq12d 7430 . . . . . . . . . . . . . . . 16 (๐‘ข = (๐‘ / ๐‘›) โ†’ ((๐‘…โ€˜๐‘ข) / ๐‘ข) = ((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›)))
248247fveq2d 6895 . . . . . . . . . . . . . . 15 (๐‘ข = (๐‘ / ๐‘›) โ†’ (absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) = (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))))
249248breq1d 5158 . . . . . . . . . . . . . 14 (๐‘ข = (๐‘ / ๐‘›) โ†’ ((absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ โ†” (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) โ‰ค ๐ธ))
25088simprd 495 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ)
251250adantr 480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ)
25230adantr 480 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘ โˆˆ โ„)
253252, 120nndivred 12273 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โˆˆ โ„)
25444rpregt0d 13029 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰))
255254adantr 480 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰))
256 lemuldiv2 12102 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง (๐‘‰ โˆˆ โ„ โˆง 0 < ๐‘‰)) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘› โ‰ค (๐‘ / ๐‘‰)))
257137, 252, 255, 256syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘› โ‰ค (๐‘ / ๐‘‰)))
258136, 257mpbird 257 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘‰ ยท ๐‘›) โ‰ค ๐‘)
259255simpld 494 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โˆˆ โ„)
260259, 252, 121lemuldivd 13072 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘‰ ยท ๐‘›) โ‰ค ๐‘ โ†” ๐‘‰ โ‰ค (๐‘ / ๐‘›)))
261258, 260mpbid 231 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โ‰ค (๐‘ / ๐‘›))
262111rpregt0d 13029 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
263262adantr 480 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
264121rpregt0d 13029 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘› โˆˆ โ„ โˆง 0 < ๐‘›))
265 lediv23 12113 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„ โˆง (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„ โˆง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆง (๐‘› โˆˆ โ„ โˆง 0 < ๐‘›)) โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘› โ†” (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
266252, 263, 264, 265syl3anc 1370 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘› โ†” (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
267189, 266mpbid 231 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))
26844rpred 13023 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„)
269268adantr 480 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ๐‘‰ โˆˆ โ„)
270146adantr 480 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„)
271 elicc2 13396 . . . . . . . . . . . . . . . 16 ((๐‘‰ โˆˆ โ„ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„) โ†’ ((๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ†” ((๐‘ / ๐‘›) โˆˆ โ„ โˆง ๐‘‰ โ‰ค (๐‘ / ๐‘›) โˆง (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
272269, 270, 271syl2anc 583 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ†” ((๐‘ / ๐‘›) โˆˆ โ„ โˆง ๐‘‰ โ‰ค (๐‘ / ๐‘›) โˆง (๐‘ / ๐‘›) โ‰ค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
273253, 261, 267, 272mpbir3and 1341 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (๐‘ / ๐‘›) โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
274249, 251, 273rspcdva 3613 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / (๐‘ / ๐‘›))) โ‰ค ๐ธ)
275244, 274eqbrtrrd 5172 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›) โ‰ค ๐ธ)
276224, 220, 121lemuldivd 13072 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) ยท ๐‘›) โ‰ค ๐ธ โ†” (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โ‰ค (๐ธ / ๐‘›)))
277275, 276mpbid 231 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘)) โ‰ค (๐ธ / ๐‘›))
278224, 225, 226, 277lesub2dd 11838 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ / ๐‘›) โˆ’ (๐ธ / ๐‘›)) โ‰ค ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))))
279223, 278eqbrtrd 5170 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) โ‰ค ((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))))
280209, 210, 122, 216, 279lemul1ad 12160 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ (((๐‘ˆ โˆ’ ๐ธ) / ๐‘›) ยท (logโ€˜๐‘›)) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
281207, 280eqbrtrrd 5172 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜๐‘›) / ๐‘›)) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
28299, 124, 126, 198, 281letrd 11378 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
283282adantlr 712 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ๐‘› โˆˆ ๐ผ) โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
28469nnred 12234 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„)
28529, 151rpdivcld 13040 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„+)
286285rpred 13023 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„)
287286adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„)
28823simpld 494 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„+)
28929, 288rpdivcld 13040 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„+)
290289rpred 13023 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„)
291290adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / ๐‘Œ) โˆˆ โ„)
292 simpr 484 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ ๐‘‚)
293292, 50eleqtrdi 2842 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
294 elfzle2 13512 . . . . . . . . . . 11 (๐‘› โˆˆ (((โŒŠโ€˜(๐‘ / (๐พโ†‘(๐ฝ + 1)))) + 1)...(โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
295293, 294syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ))))
29669nnzd 12592 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โˆˆ โ„ค)
297 flge 13777 . . . . . . . . . . 11 (((๐‘ / (๐พโ†‘๐ฝ)) โˆˆ โ„ โˆง ๐‘› โˆˆ โ„ค) โ†’ (๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
298287, 296, 297syl2anc 583 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)) โ†” ๐‘› โ‰ค (โŒŠโ€˜(๐‘ / (๐พโ†‘๐ฝ)))))
299295, 298mpbird 257 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (๐‘ / (๐พโ†‘๐ฝ)))
300288rpred 13023 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
30124simpld 494 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„+)
302301rpred 13023 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
303151rpred 13023 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„)
30424simprd 495 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘Œ < ๐‘‹)
305300, 302, 304ltled 11369 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โ‰ค ๐‘‹)
306 elfzofz 13655 . . . . . . . . . . . . . . . 16 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ (๐‘€...๐‘))
30756, 306syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐‘€...๐‘))
3081, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 27445 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐ฝ โˆˆ (๐‘€...๐‘)) โ†’ (๐‘‹ < (๐พโ†‘๐ฝ) โˆง (๐พโ†‘๐ฝ) โ‰ค (โˆšโ€˜๐‘)))
309307, 308mpdan 684 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‹ < (๐พโ†‘๐ฝ) โˆง (๐พโ†‘๐ฝ) โ‰ค (โˆšโ€˜๐‘)))
310309simpld 494 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‹ < (๐พโ†‘๐ฝ))
311302, 303, 310ltled 11369 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โ‰ค (๐พโ†‘๐ฝ))
312300, 302, 303, 305, 311letrd 11378 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โ‰ค (๐พโ†‘๐ฝ))
313288, 151, 29lediv2d 13047 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘Œ โ‰ค (๐พโ†‘๐ฝ) โ†” (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ)))
314312, 313mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ))
315314adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘ / (๐พโ†‘๐ฝ)) โ‰ค (๐‘ / ๐‘Œ))
316284, 287, 291, 299, 315letrd 11378 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ ๐‘› โ‰ค (๐‘ / ๐‘Œ))
31769, 316jca 511 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ (๐‘› โˆˆ โ„• โˆง ๐‘› โ‰ค (๐‘ / ๐‘Œ)))
3181, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86pntlemn 27446 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โ‰ค (๐‘ / ๐‘Œ))) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
319317, 318syldan 590 . . . . . 6 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
320319adantr 480 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โˆง ยฌ ๐‘› โˆˆ ๐ผ) โ†’ 0 โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
321103, 104, 283, 320ifbothda 4566 . . . 4 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘‚) โ†’ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32252, 102, 82, 321fsumle 15752 . . 3 (๐œ‘ โ†’ ฮฃ๐‘› โˆˆ ๐‘‚ if(๐‘› โˆˆ ๐ผ, ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))), 0) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32398, 322eqbrtrd 5170 . 2 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
32436, 49, 83, 89, 323letrd 11378 1 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ฮฃ๐‘› โˆˆ ๐‘‚ (((๐‘ˆ / ๐‘›) โˆ’ (absโ€˜((๐‘…โ€˜(๐‘ / ๐‘›)) / ๐‘))) ยท (logโ€˜๐‘›)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1086   = wceq 1540   โˆˆ wcel 2105   โ‰  wne 2939  โˆ€wral 3060  โˆƒwrex 3069   โІ wss 3948  ifcif 4528   class class class wbr 5148   โ†ฆ cmpt 5231  โ€˜cfv 6543  (class class class)co 7412  Fincfn 8945  โ„‚cc 11114  โ„cr 11115  0cc0 11116  1c1 11117   + caddc 11119   ยท cmul 11121  +โˆžcpnf 11252   < clt 11255   โ‰ค cle 11256   โˆ’ cmin 11451   / cdiv 11878  โ„•cn 12219  2c2 12274  3c3 12275  4c4 12276  8c8 12280  โ„•0cn0 12479  โ„คcz 12565  cdc 12684  โ„คโ‰ฅcuz 12829  โ„+crp 12981  (,)cioo 13331  [,)cico 13333  [,]cicc 13334  ...cfz 13491  ..^cfzo 13634  โŒŠcfl 13762  โ†‘cexp 14034  โ™ฏchash 14297  โˆšcsqrt 15187  abscabs 15188  ฮฃcsu 15639  expce 16012  eceu 16013  logclog 26403  ฯˆcchp 26938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9642  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194  ax-addf 11195
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  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 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8152  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-2o 8473  df-oadd 8476  df-er 8709  df-map 8828  df-pm 8829  df-ixp 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9368  df-fi 9412  df-sup 9443  df-inf 9444  df-oi 9511  df-dju 9902  df-card 9940  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12480  df-z 12566  df-dec 12685  df-uz 12830  df-q 12940  df-rp 12982  df-xneg 13099  df-xadd 13100  df-xmul 13101  df-ioo 13335  df-ioc 13336  df-ico 13337  df-icc 13338  df-fz 13492  df-fzo 13635  df-fl 13764  df-mod 13842  df-seq 13974  df-exp 14035  df-fac 14241  df-bc 14270  df-hash 14298  df-shft 15021  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190  df-limsup 15422  df-clim 15439  df-rlim 15440  df-sum 15640  df-ef 16018  df-e 16019  df-sin 16020  df-cos 16021  df-pi 16023  df-dvds 16205  df-gcd 16443  df-prm 16616  df-pc 16777  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-rest 17375  df-topn 17376  df-0g 17394  df-gsum 17395  df-topgen 17396  df-pt 17397  df-prds 17400  df-xrs 17455  df-qtop 17460  df-imas 17461  df-xps 17463  df-mre 17537  df-mrc 17538  df-acs 17540  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-submnd 18712  df-mulg 18994  df-cntz 19229  df-cmn 19698  df-psmet 21225  df-xmet 21226  df-met 21227  df-bl 21228  df-mopn 21229  df-fbas 21230  df-fg 21231  df-cnfld 21234  df-top 22716  df-topon 22733  df-topsp 22755  df-bases 22769  df-cld 22843  df-ntr 22844  df-cls 22845  df-nei 22922  df-lp 22960  df-perf 22961  df-cn 23051  df-cnp 23052  df-haus 23139  df-tx 23386  df-hmeo 23579  df-fil 23670  df-fm 23762  df-flim 23763  df-flf 23764  df-xms 24146  df-ms 24147  df-tms 24148  df-cncf 24718  df-limc 25715  df-dv 25716  df-log 26405  df-vma 26943  df-chp 26944
This theorem is referenced by:  pntlemi  27450
  Copyright terms: Public domain W3C validator