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

Theorem pntlemr 26966
Description: Lemma for pntlemj 26967. (Contributed by Mario Carneiro, 7-Jun-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
pntlemr (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
Distinct variable groups:   ๐‘ง,๐ถ   ๐‘ฆ,๐‘ง,๐ฝ   ๐‘ฆ,๐‘ข,๐‘ง,๐ฟ   ๐‘ฆ,๐พ,๐‘ง   ๐‘ง,๐‘€   ๐‘ง,๐‘‚   ๐‘ง,๐‘   ๐‘ข,๐‘…,๐‘ฆ,๐‘ง   ๐‘ข,๐‘‰   ๐‘ง,๐‘ˆ   ๐‘ง,๐‘Š   ๐‘ฆ,๐‘‹,๐‘ง   ๐‘ง,๐‘Œ   ๐‘ข,๐‘Ž,๐‘ฆ,๐‘ง,๐ธ   ๐‘ข,๐‘,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘ฆ,๐‘ง,๐‘ข,๐‘Ž)   ๐ด(๐‘ฆ,๐‘ง,๐‘ข,๐‘Ž)   ๐ต(๐‘ฆ,๐‘ง,๐‘ข,๐‘Ž)   ๐ถ(๐‘ฆ,๐‘ข,๐‘Ž)   ๐ท(๐‘ฆ,๐‘ง,๐‘ข,๐‘Ž)   ๐‘…(๐‘Ž)   ๐‘ˆ(๐‘ฆ,๐‘ข,๐‘Ž)   ๐น(๐‘ฆ,๐‘ง,๐‘ข,๐‘Ž)   ๐ผ(๐‘ฆ,๐‘ง,๐‘ข,๐‘Ž)   ๐ฝ(๐‘ข,๐‘Ž)   ๐พ(๐‘ข,๐‘Ž)   ๐ฟ(๐‘Ž)   ๐‘€(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘‚(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘‰(๐‘ฆ,๐‘ง,๐‘Ž)   ๐‘Š(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘‹(๐‘ข,๐‘Ž)   ๐‘Œ(๐‘ฆ,๐‘ข,๐‘Ž)   ๐‘(๐‘ฆ,๐‘Ž)

Proof of Theorem pntlemr
StepHypRef Expression
1 pntlem1.r . . . . . . . . . . . . 13 ๐‘… = (๐‘Ž โˆˆ โ„+ โ†ฆ ((ฯˆโ€˜๐‘Ž) โˆ’ ๐‘Ž))
2 pntlem1.a . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ด โˆˆ โ„+)
3 pntlem1.b . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ต โˆˆ โ„+)
4 pntlem1.l . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ฟ โˆˆ (0(,)1))
5 pntlem1.d . . . . . . . . . . . . 13 ๐ท = (๐ด + 1)
6 pntlem1.f . . . . . . . . . . . . 13 ๐น = ((1 โˆ’ (1 / ๐ท)) ยท ((๐ฟ / (32 ยท ๐ต)) / (๐ทโ†‘2)))
71, 2, 3, 4, 5, 6pntlemd 26958 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ฟ โˆˆ โ„+ โˆง ๐ท โˆˆ โ„+ โˆง ๐น โˆˆ โ„+))
87simp1d 1143 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„+)
9 pntlem1.u . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„+)
10 pntlem1.u2 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ˆ โ‰ค ๐ด)
11 pntlem1.e . . . . . . . . . . . . 13 ๐ธ = (๐‘ˆ / ๐ท)
12 pntlem1.k . . . . . . . . . . . . 13 ๐พ = (expโ€˜(๐ต / ๐ธ))
131, 2, 3, 4, 5, 6, 9, 10, 11, 12pntlemc 26959 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ธ โˆˆ โ„+ โˆง ๐พ โˆˆ โ„+ โˆง (๐ธ โˆˆ (0(,)1) โˆง 1 < ๐พ โˆง (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+)))
1413simp1d 1143 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
158, 14rpmulcld 12978 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) โˆˆ โ„+)
16 4re 12242 . . . . . . . . . . 11 4 โˆˆ โ„
17 4pos 12265 . . . . . . . . . . 11 0 < 4
1816, 17elrpii 12923 . . . . . . . . . 10 4 โˆˆ โ„+
19 rpdivcl 12945 . . . . . . . . . 10 (((๐ฟ ยท ๐ธ) โˆˆ โ„+ โˆง 4 โˆˆ โ„+) โ†’ ((๐ฟ ยท ๐ธ) / 4) โˆˆ โ„+)
2015, 18, 19sylancl 587 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 4) โˆˆ โ„+)
2120rpred 12962 . . . . . . . 8 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 4) โˆˆ โ„)
22 pntlem1.y . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘Œ โˆˆ โ„+ โˆง 1 โ‰ค ๐‘Œ))
23 pntlem1.x . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘‹ โˆˆ โ„+ โˆง ๐‘Œ < ๐‘‹))
24 pntlem1.c . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ถ โˆˆ โ„+)
25 pntlem1.w . . . . . . . . . . . 12 ๐‘Š = (((๐‘Œ + (4 / (๐ฟ ยท ๐ธ)))โ†‘2) + (((๐‘‹ ยท (๐พโ†‘2))โ†‘4) + (expโ€˜(((32 ยท ๐ต) / ((๐‘ˆ โˆ’ ๐ธ) ยท (๐ฟ ยท (๐ธโ†‘2)))) ยท ((๐‘ˆ ยท 3) + ๐ถ)))))
26 pntlem1.z . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ โˆˆ (๐‘Š[,)+โˆž))
271, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26pntlemb 26961 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ โˆˆ โ„+ โˆง (1 < ๐‘ โˆง e โ‰ค (โˆšโ€˜๐‘) โˆง (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘Œ)) โˆง ((4 / (๐ฟ ยท ๐ธ)) โ‰ค (โˆšโ€˜๐‘) โˆง (((logโ€˜๐‘‹) / (logโ€˜๐พ)) + 2) โ‰ค (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โˆง ((๐‘ˆ ยท 3) + ๐ถ) โ‰ค (((๐‘ˆ โˆ’ ๐ธ) ยท ((๐ฟ ยท (๐ธโ†‘2)) / (32 ยท ๐ต))) ยท (logโ€˜๐‘)))))
2827simp1d 1143 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ โ„+)
29 pntlem1.v . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„+)
3028, 29rpdivcld 12979 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„+)
3130rpred 12962 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„)
3221, 31remulcld 11190 . . . . . . 7 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) โˆˆ โ„)
33 pntlem1.i . . . . . . . . . 10 ๐ผ = (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰)))
34 fzfid 13884 . . . . . . . . . 10 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) โˆˆ Fin)
3533, 34eqeltrid 2838 . . . . . . . . 9 (๐œ‘ โ†’ ๐ผ โˆˆ Fin)
36 hashcl 14262 . . . . . . . . 9 (๐ผ โˆˆ Fin โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„•0)
3735, 36syl 17 . . . . . . . 8 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„•0)
3837nn0red 12479 . . . . . . 7 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„)
3932recnd 11188 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) โˆˆ โ„‚)
40 1rp 12924 . . . . . . . . . . . . . . . . . 18 1 โˆˆ โ„+
41 rpaddcl 12942 . . . . . . . . . . . . . . . . . 18 ((1 โˆˆ โ„+ โˆง (๐ฟ ยท ๐ธ) โˆˆ โ„+) โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
4240, 15, 41sylancr 588 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
4342, 29rpmulcld 12978 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„+)
4428, 43rpdivcld 12979 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„+)
4544rpred 12962 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„)
46 reflcl 13707 . . . . . . . . . . . . . 14 ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„)
4745, 46syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„)
4847recnd 11188 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„‚)
49 1cnd 11155 . . . . . . . . . . . 12 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
5039, 48, 49add32d 11387 . . . . . . . . . . 11 (๐œ‘ โ†’ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) + 1) = (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))))
51 peano2re 11333 . . . . . . . . . . . . . 14 ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) โˆˆ โ„ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1) โˆˆ โ„)
5232, 51syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1) โˆˆ โ„)
5352, 47readdcld 11189 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) โˆˆ โ„)
54 reflcl 13707 . . . . . . . . . . . . . 14 ((๐‘ / ๐‘‰) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„)
5531, 54syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„)
56 peano2re 11333 . . . . . . . . . . . . 13 ((โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„ โ†’ ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1) โˆˆ โ„)
5755, 56syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1) โˆˆ โ„)
5815rphalfcld 12974 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 2) โˆˆ โ„+)
5958, 30rpmulcld 12978 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) โˆˆ โ„+)
6059rpred 12962 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) โˆˆ โ„)
6160, 45readdcld 11189 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) + (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โˆˆ โ„)
62 rpdivcl 12945 . . . . . . . . . . . . . . . . . . . 20 ((4 โˆˆ โ„+ โˆง (๐ฟ ยท ๐ธ) โˆˆ โ„+) โ†’ (4 / (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
6318, 15, 62sylancr 588 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (4 / (๐ฟ ยท ๐ธ)) โˆˆ โ„+)
6463rpred 12962 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (4 / (๐ฟ ยท ๐ธ)) โˆˆ โ„)
6528rpsqrtcld 15302 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„+)
6665rpred 12962 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„)
6727simp3d 1145 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((4 / (๐ฟ ยท ๐ธ)) โ‰ค (โˆšโ€˜๐‘) โˆง (((logโ€˜๐‘‹) / (logโ€˜๐พ)) + 2) โ‰ค (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โˆง ((๐‘ˆ ยท 3) + ๐ถ) โ‰ค (((๐‘ˆ โˆ’ ๐ธ) ยท ((๐ฟ ยท (๐ธโ†‘2)) / (32 ยท ๐ต))) ยท (logโ€˜๐‘))))
6867simp1d 1143 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (4 / (๐ฟ ยท ๐ธ)) โ‰ค (โˆšโ€˜๐‘))
6943rpred 12962 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โˆˆ โ„)
7013simp2d 1144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ ๐พ โˆˆ โ„+)
71 pntlem1.j . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ ๐ฝ โˆˆ (๐‘€..^๐‘))
72 elfzoelz 13578 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ โ„ค)
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค)
7473peano2zd 12615 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (๐ฝ + 1) โˆˆ โ„ค)
7570, 74rpexpcld 14156 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โˆˆ โ„+)
7675rpred 12962 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โˆˆ โ„)
77 pntlem1.V . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐œ‘ โ†’ (((๐พโ†‘๐ฝ) < ๐‘‰ โˆง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ))) โˆง โˆ€๐‘ข โˆˆ (๐‘‰[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))(absโ€˜((๐‘…โ€˜๐‘ข) / ๐‘ข)) โ‰ค ๐ธ))
7877simplrd 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พ ยท (๐พโ†‘๐ฝ)))
7970rpcnd 12964 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ ๐พ โˆˆ โ„‚)
8070, 73rpexpcld 14156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„+)
8180rpcnd 12964 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ (๐พโ†‘๐ฝ) โˆˆ โ„‚)
8279, 81mulcomd 11181 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐œ‘ โ†’ (๐พ ยท (๐พโ†‘๐ฝ)) = ((๐พโ†‘๐ฝ) ยท ๐พ))
83 pntlem1.m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ๐‘€ = ((โŒŠโ€˜((logโ€˜๐‘‹) / (logโ€˜๐พ))) + 1)
84 pntlem1.n . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ๐‘ = (โŒŠโ€˜(((logโ€˜๐‘) / (logโ€˜๐พ)) / 2))
851, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84pntlemg 26962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐œ‘ โ†’ (๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง (((logโ€˜๐‘) / (logโ€˜๐พ)) / 4) โ‰ค (๐‘ โˆ’ ๐‘€)))
8685simp1d 1143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
87 elfzouz 13582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
8871, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐œ‘ โ†’ ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
89 eluznn 12848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐‘€ โˆˆ โ„• โˆง ๐ฝ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐ฝ โˆˆ โ„•)
9086, 88, 89syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•)
9190nnnn0d 12478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•0)
9279, 91expp1d 14058 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) = ((๐พโ†‘๐ฝ) ยท ๐พ))
9382, 92eqtr4d 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (๐พ ยท (๐พโ†‘๐ฝ)) = (๐พโ†‘(๐ฝ + 1)))
9478, 93breqtrd 5132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (๐พโ†‘(๐ฝ + 1)))
9569, 76, 94ltled 11308 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (๐พโ†‘(๐ฝ + 1)))
96 fzofzp1 13675 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐ฝ โˆˆ (๐‘€..^๐‘) โ†’ (๐ฝ + 1) โˆˆ (๐‘€...๐‘))
9771, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (๐ฝ + 1) โˆˆ (๐‘€...๐‘))
981, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84pntlemh 26963 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐ฝ + 1) โˆˆ (๐‘€...๐‘)) โ†’ (๐‘‹ < (๐พโ†‘(๐ฝ + 1)) โˆง (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘)))
9997, 98mpdan 686 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐œ‘ โ†’ (๐‘‹ < (๐พโ†‘(๐ฝ + 1)) โˆง (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘)))
10099simprd 497 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (๐พโ†‘(๐ฝ + 1)) โ‰ค (โˆšโ€˜๐‘))
10169, 76, 66, 95, 100letrd 11317 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (โˆšโ€˜๐‘))
10269, 66, 65lemul2d 13006 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ‰ค (โˆšโ€˜๐‘) โ†” ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘))))
103101, 102mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)))
10428rprege0d 12969 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘))
105 remsqsqrt 15147 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘) โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
107103, 106breqtrd 5132 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘)
10828rpred 12962 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
10966, 108, 43lemuldivd 13011 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (((โˆšโ€˜๐‘) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค ๐‘ โ†” (โˆšโ€˜๐‘) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
110107, 109mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
11129rpcnd 12964 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„‚)
112111mulid2d 11178 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (1 ยท ๐‘‰) = ๐‘‰)
113 1red 11161 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ 1 โˆˆ โ„)
11442rpred 12962 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„)
115 1re 11160 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 โˆˆ โ„
116 ltaddrp 12957 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 โˆˆ โ„ โˆง (๐ฟ ยท ๐ธ) โˆˆ โ„+) โ†’ 1 < (1 + (๐ฟ ยท ๐ธ)))
117115, 15, 116sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ 1 < (1 + (๐ฟ ยท ๐ธ)))
118113, 114, 29, 117ltmul1dd 13017 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (1 ยท ๐‘‰) < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))
119112, 118eqbrtrrd 5130 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐‘‰ < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))
12029, 43, 28ltdiv2d 12985 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‰ < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) โ†” (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) < (๐‘ / ๐‘‰)))
121119, 120mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) < (๐‘ / ๐‘‰))
12245, 31, 121ltled 11308 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค (๐‘ / ๐‘‰))
12366, 45, 31, 110, 122letrd 11317 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘‰))
12464, 66, 31, 68, 123letrd 11317 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (4 / (๐ฟ ยท ๐ธ)) โ‰ค (๐‘ / ๐‘‰))
12564, 31, 31, 124leadd2dd 11775 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐‘ / ๐‘‰) + (4 / (๐ฟ ยท ๐ธ))) โ‰ค ((๐‘ / ๐‘‰) + (๐‘ / ๐‘‰)))
12630rpcnd 12964 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โˆˆ โ„‚)
1271262timesd 12401 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2 ยท (๐‘ / ๐‘‰)) = ((๐‘ / ๐‘‰) + (๐‘ / ๐‘‰)))
128125, 127breqtrrd 5134 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐‘ / ๐‘‰) + (4 / (๐ฟ ยท ๐ธ))) โ‰ค (2 ยท (๐‘ / ๐‘‰)))
12931, 64readdcld 11189 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐‘ / ๐‘‰) + (4 / (๐ฟ ยท ๐ธ))) โˆˆ โ„)
130 2re 12232 . . . . . . . . . . . . . . . . . 18 2 โˆˆ โ„
131 remulcl 11141 . . . . . . . . . . . . . . . . . 18 ((2 โˆˆ โ„ โˆง (๐‘ / ๐‘‰) โˆˆ โ„) โ†’ (2 ยท (๐‘ / ๐‘‰)) โˆˆ โ„)
132130, 31, 131sylancr 588 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2 ยท (๐‘ / ๐‘‰)) โˆˆ โ„)
133129, 132, 20lemul2d 13006 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((๐‘ / ๐‘‰) + (4 / (๐ฟ ยท ๐ธ))) โ‰ค (2 ยท (๐‘ / ๐‘‰)) โ†” (((๐ฟ ยท ๐ธ) / 4) ยท ((๐‘ / ๐‘‰) + (4 / (๐ฟ ยท ๐ธ)))) โ‰ค (((๐ฟ ยท ๐ธ) / 4) ยท (2 ยท (๐‘ / ๐‘‰)))))
134128, 133mpbid 231 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท ((๐‘ / ๐‘‰) + (4 / (๐ฟ ยท ๐ธ)))) โ‰ค (((๐ฟ ยท ๐ธ) / 4) ยท (2 ยท (๐‘ / ๐‘‰))))
13520rpcnd 12964 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 4) โˆˆ โ„‚)
13663rpcnd 12964 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (4 / (๐ฟ ยท ๐ธ)) โˆˆ โ„‚)
137135, 126, 136adddid 11184 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท ((๐‘ / ๐‘‰) + (4 / (๐ฟ ยท ๐ธ)))) = ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (((๐ฟ ยท ๐ธ) / 4) ยท (4 / (๐ฟ ยท ๐ธ)))))
13815rpcnne0d 12971 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) โˆˆ โ„‚ โˆง (๐ฟ ยท ๐ธ) โ‰  0))
139 rpcnne0 12938 . . . . . . . . . . . . . . . . . . 19 (4 โˆˆ โ„+ โ†’ (4 โˆˆ โ„‚ โˆง 4 โ‰  0))
14018, 139mp1i 13 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (4 โˆˆ โ„‚ โˆง 4 โ‰  0))
141 divcan6 11867 . . . . . . . . . . . . . . . . . 18 ((((๐ฟ ยท ๐ธ) โˆˆ โ„‚ โˆง (๐ฟ ยท ๐ธ) โ‰  0) โˆง (4 โˆˆ โ„‚ โˆง 4 โ‰  0)) โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท (4 / (๐ฟ ยท ๐ธ))) = 1)
142138, 140, 141syl2anc 585 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท (4 / (๐ฟ ยท ๐ธ))) = 1)
143142oveq2d 7374 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (((๐ฟ ยท ๐ธ) / 4) ยท (4 / (๐ฟ ยท ๐ธ)))) = ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1))
144137, 143eqtrd 2773 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท ((๐‘ / ๐‘‰) + (4 / (๐ฟ ยท ๐ธ)))) = ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1))
145 2cnd 12236 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
146135, 145, 126mulassd 11183 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท 2) ยท (๐‘ / ๐‘‰)) = (((๐ฟ ยท ๐ธ) / 4) ยท (2 ยท (๐‘ / ๐‘‰))))
14715rpcnd 12964 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) โˆˆ โ„‚)
148 2rp 12925 . . . . . . . . . . . . . . . . . . . . . 22 2 โˆˆ โ„+
149 rpcnne0 12938 . . . . . . . . . . . . . . . . . . . . . 22 (2 โˆˆ โ„+ โ†’ (2 โˆˆ โ„‚ โˆง 2 โ‰  0))
150148, 149mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (2 โˆˆ โ„‚ โˆง 2 โ‰  0))
151 divdiv1 11871 . . . . . . . . . . . . . . . . . . . . 21 (((๐ฟ ยท ๐ธ) โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0) โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ (((๐ฟ ยท ๐ธ) / 2) / 2) = ((๐ฟ ยท ๐ธ) / (2 ยท 2)))
152147, 150, 150, 151syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 2) / 2) = ((๐ฟ ยท ๐ธ) / (2 ยท 2)))
153 2t2e4 12322 . . . . . . . . . . . . . . . . . . . . 21 (2 ยท 2) = 4
154153oveq2i 7369 . . . . . . . . . . . . . . . . . . . 20 ((๐ฟ ยท ๐ธ) / (2 ยท 2)) = ((๐ฟ ยท ๐ธ) / 4)
155152, 154eqtr2di 2790 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 4) = (((๐ฟ ยท ๐ธ) / 2) / 2))
156155oveq1d 7373 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท 2) = ((((๐ฟ ยท ๐ธ) / 2) / 2) ยท 2))
157147halfcld 12403 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 2) โˆˆ โ„‚)
158150simprd 497 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 2 โ‰  0)
159157, 145, 158divcan1d 11937 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 2) / 2) ยท 2) = ((๐ฟ ยท ๐ธ) / 2))
160156, 159eqtrd 2773 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท 2) = ((๐ฟ ยท ๐ธ) / 2))
161160oveq1d 7373 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท 2) ยท (๐‘ / ๐‘‰)) = (((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)))
162146, 161eqtr3d 2775 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท (2 ยท (๐‘ / ๐‘‰))) = (((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)))
163134, 144, 1623brtr3d 5137 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1) โ‰ค (((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)))
164 flle 13710 . . . . . . . . . . . . . . 15 ((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
16545, 164syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) โ‰ค (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))
16652, 47, 60, 45, 163, 165le2addd 11779 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) โ‰ค ((((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) + (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
16758rpred 12962 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 2) โˆˆ โ„)
16842rprecred 12973 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (1 / (1 + (๐ฟ ยท ๐ธ))) โˆˆ โ„)
169167, 168readdcld 11189 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) โˆˆ โ„)
17015rpred 12962 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) โˆˆ โ„)
17114rpred 12962 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
1728rpred 12962 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐ฟ โˆˆ โ„)
173 eliooord 13329 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ฟ โˆˆ (0(,)1) โ†’ (0 < ๐ฟ โˆง ๐ฟ < 1))
1744, 173syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (0 < ๐ฟ โˆง ๐ฟ < 1))
175174simprd 497 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐ฟ < 1)
176172, 113, 14, 175ltmul1dd 13017 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) < (1 ยท ๐ธ))
17714rpcnd 12964 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐ธ โˆˆ โ„‚)
178177mulid2d 11178 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (1 ยท ๐ธ) = ๐ธ)
179176, 178breqtrd 5132 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) < ๐ธ)
18013simp3d 1145 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (๐ธ โˆˆ (0(,)1) โˆง 1 < ๐พ โˆง (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+))
181180simp1d 1143 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ๐ธ โˆˆ (0(,)1))
182 eliooord 13329 . . . . . . . . . . . . . . . . . . . . . . 23 (๐ธ โˆˆ (0(,)1) โ†’ (0 < ๐ธ โˆง ๐ธ < 1))
183181, 182syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (0 < ๐ธ โˆง ๐ธ < 1))
184183simprd 497 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ธ < 1)
185170, 171, 113, 179, 184lttrd 11321 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐ฟ ยท ๐ธ) < 1)
186170, 113, 113, 185ltadd2dd 11319 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) < (1 + 1))
187 df-2 12221 . . . . . . . . . . . . . . . . . . 19 2 = (1 + 1)
188186, 187breqtrrdi 5148 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) < 2)
18942rpregt0d 12968 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„ โˆง 0 < (1 + (๐ฟ ยท ๐ธ))))
190130a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 2 โˆˆ โ„)
191 2pos 12261 . . . . . . . . . . . . . . . . . . . 20 0 < 2
192191a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 < 2)
19315rpregt0d 12968 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) โˆˆ โ„ โˆง 0 < (๐ฟ ยท ๐ธ)))
194 ltdiv2 12046 . . . . . . . . . . . . . . . . . . 19 ((((1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„ โˆง 0 < (1 + (๐ฟ ยท ๐ธ))) โˆง (2 โˆˆ โ„ โˆง 0 < 2) โˆง ((๐ฟ ยท ๐ธ) โˆˆ โ„ โˆง 0 < (๐ฟ ยท ๐ธ))) โ†’ ((1 + (๐ฟ ยท ๐ธ)) < 2 โ†” ((๐ฟ ยท ๐ธ) / 2) < ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ)))))
195189, 190, 192, 193, 194syl121anc 1376 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) < 2 โ†” ((๐ฟ ยท ๐ธ) / 2) < ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ)))))
196188, 195mpbid 231 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 2) < ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ))))
19742rpcnd 12964 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„‚)
19842rpcnne0d 12971 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„‚ โˆง (1 + (๐ฟ ยท ๐ธ)) โ‰  0))
199 divsubdir 11854 . . . . . . . . . . . . . . . . . . 19 (((1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง ((1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„‚ โˆง (1 + (๐ฟ ยท ๐ธ)) โ‰  0)) โ†’ (((1 + (๐ฟ ยท ๐ธ)) โˆ’ 1) / (1 + (๐ฟ ยท ๐ธ))) = (((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) โˆ’ (1 / (1 + (๐ฟ ยท ๐ธ)))))
200197, 49, 198, 199syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) โˆ’ 1) / (1 + (๐ฟ ยท ๐ธ))) = (((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) โˆ’ (1 / (1 + (๐ฟ ยท ๐ธ)))))
201 ax-1cn 11114 . . . . . . . . . . . . . . . . . . . 20 1 โˆˆ โ„‚
202 pncan2 11413 . . . . . . . . . . . . . . . . . . . 20 ((1 โˆˆ โ„‚ โˆง (๐ฟ ยท ๐ธ) โˆˆ โ„‚) โ†’ ((1 + (๐ฟ ยท ๐ธ)) โˆ’ 1) = (๐ฟ ยท ๐ธ))
203201, 147, 202sylancr 588 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) โˆ’ 1) = (๐ฟ ยท ๐ธ))
204203oveq1d 7373 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) โˆ’ 1) / (1 + (๐ฟ ยท ๐ธ))) = ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ))))
205 divid 11847 . . . . . . . . . . . . . . . . . . . 20 (((1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„‚ โˆง (1 + (๐ฟ ยท ๐ธ)) โ‰  0) โ†’ ((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) = 1)
206198, 205syl 17 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) = 1)
207206oveq1d 7373 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) โˆ’ (1 / (1 + (๐ฟ ยท ๐ธ)))) = (1 โˆ’ (1 / (1 + (๐ฟ ยท ๐ธ)))))
208200, 204, 2073eqtr3d 2781 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ))) = (1 โˆ’ (1 / (1 + (๐ฟ ยท ๐ธ)))))
209196, 208breqtrd 5132 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 2) < (1 โˆ’ (1 / (1 + (๐ฟ ยท ๐ธ)))))
210167, 168, 113ltaddsubd 11760 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) < 1 โ†” ((๐ฟ ยท ๐ธ) / 2) < (1 โˆ’ (1 / (1 + (๐ฟ ยท ๐ธ))))))
211209, 210mpbird 257 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) < 1)
212169, 113, 30, 211ltmul1dd 13017 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) ยท (๐‘ / ๐‘‰)) < (1 ยท (๐‘ / ๐‘‰)))
213 reccl 11825 . . . . . . . . . . . . . . . . 17 (((1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„‚ โˆง (1 + (๐ฟ ยท ๐ธ)) โ‰  0) โ†’ (1 / (1 + (๐ฟ ยท ๐ธ))) โˆˆ โ„‚)
214198, 213syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (1 / (1 + (๐ฟ ยท ๐ธ))) โˆˆ โ„‚)
215157, 214, 126adddird 11185 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) ยท (๐‘ / ๐‘‰)) = ((((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) + ((1 / (1 + (๐ฟ ยท ๐ธ))) ยท (๐‘ / ๐‘‰))))
216197, 111mulcomd 11181 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) = (๐‘‰ ยท (1 + (๐ฟ ยท ๐ธ))))
217216oveq2d 7374 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) = (๐‘ / (๐‘‰ ยท (1 + (๐ฟ ยท ๐ธ)))))
21828rpcnd 12964 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
21929rpcnne0d 12971 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘‰ โˆˆ โ„‚ โˆง ๐‘‰ โ‰  0))
220 divdiv1 11871 . . . . . . . . . . . . . . . . . 18 ((๐‘ โˆˆ โ„‚ โˆง (๐‘‰ โˆˆ โ„‚ โˆง ๐‘‰ โ‰  0) โˆง ((1 + (๐ฟ ยท ๐ธ)) โˆˆ โ„‚ โˆง (1 + (๐ฟ ยท ๐ธ)) โ‰  0)) โ†’ ((๐‘ / ๐‘‰) / (1 + (๐ฟ ยท ๐ธ))) = (๐‘ / (๐‘‰ ยท (1 + (๐ฟ ยท ๐ธ)))))
221218, 219, 198, 220syl3anc 1372 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐‘ / ๐‘‰) / (1 + (๐ฟ ยท ๐ธ))) = (๐‘ / (๐‘‰ ยท (1 + (๐ฟ ยท ๐ธ)))))
22242rpne0d 12967 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (1 + (๐ฟ ยท ๐ธ)) โ‰  0)
223126, 197, 222divrec2d 11940 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐‘ / ๐‘‰) / (1 + (๐ฟ ยท ๐ธ))) = ((1 / (1 + (๐ฟ ยท ๐ธ))) ยท (๐‘ / ๐‘‰)))
224217, 221, 2233eqtr2d 2779 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) = ((1 / (1 + (๐ฟ ยท ๐ธ))) ยท (๐‘ / ๐‘‰)))
225224oveq2d 7374 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) + (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) = ((((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) + ((1 / (1 + (๐ฟ ยท ๐ธ))) ยท (๐‘ / ๐‘‰))))
226215, 225eqtr4d 2776 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) ยท (๐‘ / ๐‘‰)) = ((((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) + (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))
227126mulid2d 11178 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1 ยท (๐‘ / ๐‘‰)) = (๐‘ / ๐‘‰))
228212, 226, 2273brtr3d 5137 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 2) ยท (๐‘ / ๐‘‰)) + (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) < (๐‘ / ๐‘‰))
22953, 61, 31, 166, 228lelttrd 11318 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) < (๐‘ / ๐‘‰))
230 fllep1 13712 . . . . . . . . . . . . 13 ((๐‘ / ๐‘‰) โˆˆ โ„ โ†’ (๐‘ / ๐‘‰) โ‰ค ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1))
23131, 230syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ / ๐‘‰) โ‰ค ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1))
23253, 31, 57, 229, 231ltletrd 11320 . . . . . . . . . . 11 (๐œ‘ โ†’ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + 1) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) < ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1))
23350, 232eqbrtrd 5128 . . . . . . . . . 10 (๐œ‘ โ†’ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) + 1) < ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1))
23432, 47readdcld 11189 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) โˆˆ โ„)
235234, 55, 113ltadd1d 11753 . . . . . . . . . 10 (๐œ‘ โ†’ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) < (โŒŠโ€˜(๐‘ / ๐‘‰)) โ†” (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) + 1) < ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1)))
236233, 235mpbird 257 . . . . . . . . 9 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) < (โŒŠโ€˜(๐‘ / ๐‘‰)))
23732, 47, 55ltaddsubd 11760 . . . . . . . . 9 (๐œ‘ โ†’ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) + (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) < (โŒŠโ€˜(๐‘ / ๐‘‰)) โ†” (((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) < ((โŒŠโ€˜(๐‘ / ๐‘‰)) โˆ’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))))))
238236, 237mpbid 231 . . . . . . . 8 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) < ((โŒŠโ€˜(๐‘ / ๐‘‰)) โˆ’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))))
23931flcld 13709 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„ค)
240 fzval3 13647 . . . . . . . . . . . 12 ((โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„ค โ†’ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) = (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)..^((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1)))
241239, 240syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)...(โŒŠโ€˜(๐‘ / ๐‘‰))) = (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)..^((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1)))
24233, 241eqtrid 2785 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ผ = (((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)..^((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1)))
243242fveq2d 6847 . . . . . . . . 9 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) = (โ™ฏโ€˜(((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)..^((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1))))
244 flword2 13724 . . . . . . . . . . . 12 (((๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โˆˆ โ„ โˆง (๐‘ / ๐‘‰) โˆˆ โ„ โˆง (๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)) โ‰ค (๐‘ / ๐‘‰)) โ†’ (โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ (โ„คโ‰ฅโ€˜(โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))))
24545, 31, 122, 244syl3anc 1372 . . . . . . . . . . 11 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ (โ„คโ‰ฅโ€˜(โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))))
246 eluzp1p1 12796 . . . . . . . . . . 11 ((โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ (โ„คโ‰ฅโ€˜(โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))) โ†’ ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1) โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
247245, 246syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1) โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
248 hashfzo 14335 . . . . . . . . . 10 (((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1) โˆˆ (โ„คโ‰ฅโ€˜((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)) โ†’ (โ™ฏโ€˜(((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)..^((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1))) = (((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1) โˆ’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
249247, 248syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (โ™ฏโ€˜(((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)..^((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1))) = (((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1) โˆ’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)))
25055recnd 11188 . . . . . . . . . 10 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„‚)
251250, 48, 49pnpcan2d 11555 . . . . . . . . 9 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘ / ๐‘‰)) + 1) โˆ’ ((โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰))) + 1)) = ((โŒŠโ€˜(๐‘ / ๐‘‰)) โˆ’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))))
252243, 249, 2513eqtrd 2777 . . . . . . . 8 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) = ((โŒŠโ€˜(๐‘ / ๐‘‰)) โˆ’ (โŒŠโ€˜(๐‘ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰)))))
253238, 252breqtrrd 5134 . . . . . . 7 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) < (โ™ฏโ€˜๐ผ))
25432, 38, 253ltled 11308 . . . . . 6 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) โ‰ค (โ™ฏโ€˜๐ผ))
25521, 38, 30lemuldivd 13011 . . . . . 6 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐‘ / ๐‘‰)) โ‰ค (โ™ฏโ€˜๐ผ) โ†” ((๐ฟ ยท ๐ธ) / 4) โ‰ค ((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰))))
256254, 255mpbid 231 . . . . 5 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 4) โ‰ค ((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)))
25729rpred 12962 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‰ โˆˆ โ„)
25869, 76, 66, 94, 100ltletrd 11320 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐‘‰) < (โˆšโ€˜๐‘))
259257, 69, 66, 119, 258lttrd 11321 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‰ < (โˆšโ€˜๐‘))
260257, 66, 259ltled 11308 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘‰ โ‰ค (โˆšโ€˜๐‘))
26129rprege0d 12969 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰))
26265rprege0d 12969 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) โˆˆ โ„ โˆง 0 โ‰ค (โˆšโ€˜๐‘)))
263 le2sq 14045 . . . . . . . . . . . . . . 15 (((๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰) โˆง ((โˆšโ€˜๐‘) โˆˆ โ„ โˆง 0 โ‰ค (โˆšโ€˜๐‘))) โ†’ (๐‘‰ โ‰ค (โˆšโ€˜๐‘) โ†” (๐‘‰โ†‘2) โ‰ค ((โˆšโ€˜๐‘)โ†‘2)))
264261, 262, 263syl2anc 585 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‰ โ‰ค (โˆšโ€˜๐‘) โ†” (๐‘‰โ†‘2) โ‰ค ((โˆšโ€˜๐‘)โ†‘2)))
265260, 264mpbid 231 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‰โ†‘2) โ‰ค ((โˆšโ€˜๐‘)โ†‘2))
266 resqrtth 15146 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘) โ†’ ((โˆšโ€˜๐‘)โ†‘2) = ๐‘)
267104, 266syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โˆšโ€˜๐‘)โ†‘2) = ๐‘)
268265, 267breqtrd 5132 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘‰โ†‘2) โ‰ค ๐‘)
269 2z 12540 . . . . . . . . . . . . . . 15 2 โˆˆ โ„ค
270 rpexpcl 13992 . . . . . . . . . . . . . . 15 ((๐‘‰ โˆˆ โ„+ โˆง 2 โˆˆ โ„ค) โ†’ (๐‘‰โ†‘2) โˆˆ โ„+)
27129, 269, 270sylancl 587 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‰โ†‘2) โˆˆ โ„+)
272271rpred 12962 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‰โ†‘2) โˆˆ โ„)
273272, 108, 28lemul2d 13006 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‰โ†‘2) โ‰ค ๐‘ โ†” (๐‘ ยท (๐‘‰โ†‘2)) โ‰ค (๐‘ ยท ๐‘)))
274268, 273mpbid 231 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ ยท (๐‘‰โ†‘2)) โ‰ค (๐‘ ยท ๐‘))
275218sqvald 14054 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘โ†‘2) = (๐‘ ยท ๐‘))
276274, 275breqtrrd 5134 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ ยท (๐‘‰โ†‘2)) โ‰ค (๐‘โ†‘2))
277108resqcld 14036 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘โ†‘2) โˆˆ โ„)
278108, 277, 271lemuldivd 13011 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ ยท (๐‘‰โ†‘2)) โ‰ค (๐‘โ†‘2) โ†” ๐‘ โ‰ค ((๐‘โ†‘2) / (๐‘‰โ†‘2))))
279276, 278mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โ‰ค ((๐‘โ†‘2) / (๐‘‰โ†‘2)))
28029rpne0d 12967 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘‰ โ‰  0)
281218, 111, 280sqdivd 14070 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ / ๐‘‰)โ†‘2) = ((๐‘โ†‘2) / (๐‘‰โ†‘2)))
282279, 281breqtrrd 5134 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โ‰ค ((๐‘ / ๐‘‰)โ†‘2))
283 rpexpcl 13992 . . . . . . . . . 10 (((๐‘ / ๐‘‰) โˆˆ โ„+ โˆง 2 โˆˆ โ„ค) โ†’ ((๐‘ / ๐‘‰)โ†‘2) โˆˆ โ„+)
28430, 269, 283sylancl 587 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ / ๐‘‰)โ†‘2) โˆˆ โ„+)
28528, 284logled 25998 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ โ‰ค ((๐‘ / ๐‘‰)โ†‘2) โ†” (logโ€˜๐‘) โ‰ค (logโ€˜((๐‘ / ๐‘‰)โ†‘2))))
286282, 285mpbid 231 . . . . . . 7 (๐œ‘ โ†’ (logโ€˜๐‘) โ‰ค (logโ€˜((๐‘ / ๐‘‰)โ†‘2)))
287 relogexp 25967 . . . . . . . 8 (((๐‘ / ๐‘‰) โˆˆ โ„+ โˆง 2 โˆˆ โ„ค) โ†’ (logโ€˜((๐‘ / ๐‘‰)โ†‘2)) = (2 ยท (logโ€˜(๐‘ / ๐‘‰))))
28830, 269, 287sylancl 587 . . . . . . 7 (๐œ‘ โ†’ (logโ€˜((๐‘ / ๐‘‰)โ†‘2)) = (2 ยท (logโ€˜(๐‘ / ๐‘‰))))
289286, 288breqtrd 5132 . . . . . 6 (๐œ‘ โ†’ (logโ€˜๐‘) โ‰ค (2 ยท (logโ€˜(๐‘ / ๐‘‰))))
29028relogcld 25994 . . . . . . 7 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„)
29130relogcld 25994 . . . . . . 7 (๐œ‘ โ†’ (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„)
292 ledivmul 12036 . . . . . . 7 (((logโ€˜๐‘) โˆˆ โ„ โˆง (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ (((logโ€˜๐‘) / 2) โ‰ค (logโ€˜(๐‘ / ๐‘‰)) โ†” (logโ€˜๐‘) โ‰ค (2 ยท (logโ€˜(๐‘ / ๐‘‰)))))
293290, 291, 190, 192, 292syl112anc 1375 . . . . . 6 (๐œ‘ โ†’ (((logโ€˜๐‘) / 2) โ‰ค (logโ€˜(๐‘ / ๐‘‰)) โ†” (logโ€˜๐‘) โ‰ค (2 ยท (logโ€˜(๐‘ / ๐‘‰)))))
294289, 293mpbird 257 . . . . 5 (๐œ‘ โ†’ ((logโ€˜๐‘) / 2) โ‰ค (logโ€˜(๐‘ / ๐‘‰)))
29520rprege0d 12969 . . . . . 6 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) โˆˆ โ„ โˆง 0 โ‰ค ((๐ฟ ยท ๐ธ) / 4)))
29638, 30rerpdivcld 12993 . . . . . 6 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) โˆˆ โ„)
29727simp2d 1144 . . . . . . . . . 10 (๐œ‘ โ†’ (1 < ๐‘ โˆง e โ‰ค (โˆšโ€˜๐‘) โˆง (โˆšโ€˜๐‘) โ‰ค (๐‘ / ๐‘Œ)))
298297simp1d 1143 . . . . . . . . 9 (๐œ‘ โ†’ 1 < ๐‘)
299108, 298rplogcld 26000 . . . . . . . 8 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„+)
300299rphalfcld 12974 . . . . . . 7 (๐œ‘ โ†’ ((logโ€˜๐‘) / 2) โˆˆ โ„+)
301300rprege0d 12969 . . . . . 6 (๐œ‘ โ†’ (((logโ€˜๐‘) / 2) โˆˆ โ„ โˆง 0 โ‰ค ((logโ€˜๐‘) / 2)))
302 lemul12a 12018 . . . . . 6 ((((((๐ฟ ยท ๐ธ) / 4) โˆˆ โ„ โˆง 0 โ‰ค ((๐ฟ ยท ๐ธ) / 4)) โˆง ((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) โˆˆ โ„) โˆง ((((logโ€˜๐‘) / 2) โˆˆ โ„ โˆง 0 โ‰ค ((logโ€˜๐‘) / 2)) โˆง (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„)) โ†’ ((((๐ฟ ยท ๐ธ) / 4) โ‰ค ((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) โˆง ((logโ€˜๐‘) / 2) โ‰ค (logโ€˜(๐‘ / ๐‘‰))) โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ€˜๐‘) / 2)) โ‰ค (((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) ยท (logโ€˜(๐‘ / ๐‘‰)))))
303295, 296, 301, 291, 302syl22anc 838 . . . . 5 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 4) โ‰ค ((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) โˆง ((logโ€˜๐‘) / 2) โ‰ค (logโ€˜(๐‘ / ๐‘‰))) โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ€˜๐‘) / 2)) โ‰ค (((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) ยท (logโ€˜(๐‘ / ๐‘‰)))))
304256, 294, 303mp2and 698 . . . 4 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ€˜๐‘) / 2)) โ‰ค (((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) ยท (logโ€˜(๐‘ / ๐‘‰))))
305299rpcnd 12964 . . . . . 6 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„‚)
306 8nn 12253 . . . . . . . 8 8 โˆˆ โ„•
307 nnrp 12931 . . . . . . . 8 (8 โˆˆ โ„• โ†’ 8 โˆˆ โ„+)
308306, 307ax-mp 5 . . . . . . 7 8 โˆˆ โ„+
309 rpcnne0 12938 . . . . . . 7 (8 โˆˆ โ„+ โ†’ (8 โˆˆ โ„‚ โˆง 8 โ‰  0))
310308, 309mp1i 13 . . . . . 6 (๐œ‘ โ†’ (8 โˆˆ โ„‚ โˆง 8 โ‰  0))
311 div23 11837 . . . . . 6 (((๐ฟ ยท ๐ธ) โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚ โˆง (8 โˆˆ โ„‚ โˆง 8 โ‰  0)) โ†’ (((๐ฟ ยท ๐ธ) ยท (logโ€˜๐‘)) / 8) = (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)))
312147, 305, 310, 311syl3anc 1372 . . . . 5 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) ยท (logโ€˜๐‘)) / 8) = (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)))
313 divmuldiv 11860 . . . . . . 7 ((((๐ฟ ยท ๐ธ) โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚) โˆง ((4 โˆˆ โ„‚ โˆง 4 โ‰  0) โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0))) โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ€˜๐‘) / 2)) = (((๐ฟ ยท ๐ธ) ยท (logโ€˜๐‘)) / (4 ยท 2)))
314147, 305, 140, 150, 313syl22anc 838 . . . . . 6 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ€˜๐‘) / 2)) = (((๐ฟ ยท ๐ธ) ยท (logโ€˜๐‘)) / (4 ยท 2)))
315 4t2e8 12326 . . . . . . 7 (4 ยท 2) = 8
316315oveq2i 7369 . . . . . 6 (((๐ฟ ยท ๐ธ) ยท (logโ€˜๐‘)) / (4 ยท 2)) = (((๐ฟ ยท ๐ธ) ยท (logโ€˜๐‘)) / 8)
317314, 316eqtr2di 2790 . . . . 5 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) ยท (logโ€˜๐‘)) / 8) = (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ€˜๐‘) / 2)))
318312, 317eqtr3d 2775 . . . 4 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)) = (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ€˜๐‘) / 2)))
31938recnd 11188 . . . . 5 (๐œ‘ โ†’ (โ™ฏโ€˜๐ผ) โˆˆ โ„‚)
320291recnd 11188 . . . . 5 (๐œ‘ โ†’ (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„‚)
32130rpcnne0d 12971 . . . . 5 (๐œ‘ โ†’ ((๐‘ / ๐‘‰) โˆˆ โ„‚ โˆง (๐‘ / ๐‘‰) โ‰  0))
322 divass 11836 . . . . . 6 (((โ™ฏโ€˜๐ผ) โˆˆ โ„‚ โˆง (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„‚ โˆง ((๐‘ / ๐‘‰) โˆˆ โ„‚ โˆง (๐‘ / ๐‘‰) โ‰  0)) โ†’ (((โ™ฏโ€˜๐ผ) ยท (logโ€˜(๐‘ / ๐‘‰))) / (๐‘ / ๐‘‰)) = ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))))
323 div23 11837 . . . . . 6 (((โ™ฏโ€˜๐ผ) โˆˆ โ„‚ โˆง (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„‚ โˆง ((๐‘ / ๐‘‰) โˆˆ โ„‚ โˆง (๐‘ / ๐‘‰) โ‰  0)) โ†’ (((โ™ฏโ€˜๐ผ) ยท (logโ€˜(๐‘ / ๐‘‰))) / (๐‘ / ๐‘‰)) = (((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) ยท (logโ€˜(๐‘ / ๐‘‰))))
324322, 323eqtr3d 2775 . . . . 5 (((โ™ฏโ€˜๐ผ) โˆˆ โ„‚ โˆง (logโ€˜(๐‘ / ๐‘‰)) โˆˆ โ„‚ โˆง ((๐‘ / ๐‘‰) โˆˆ โ„‚ โˆง (๐‘ / ๐‘‰) โ‰  0)) โ†’ ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = (((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) ยท (logโ€˜(๐‘ / ๐‘‰))))
325319, 320, 321, 324syl3anc 1372 . . . 4 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) = (((โ™ฏโ€˜๐ผ) / (๐‘ / ๐‘‰)) ยท (logโ€˜(๐‘ / ๐‘‰))))
326304, 318, 3253brtr4d 5138 . . 3 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)) โ‰ค ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))))
327 rpdivcl 12945 . . . . . . 7 (((๐ฟ ยท ๐ธ) โˆˆ โ„+ โˆง 8 โˆˆ โ„+) โ†’ ((๐ฟ ยท ๐ธ) / 8) โˆˆ โ„+)
32815, 308, 327sylancl 587 . . . . . 6 (๐œ‘ โ†’ ((๐ฟ ยท ๐ธ) / 8) โˆˆ โ„+)
329328, 299rpmulcld 12978 . . . . 5 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)) โˆˆ โ„+)
330329rpred 12962 . . . 4 (๐œ‘ โ†’ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)) โˆˆ โ„)
331291, 30rerpdivcld 12993 . . . . 5 (๐œ‘ โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„)
33238, 331remulcld 11190 . . . 4 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โˆˆ โ„)
333180simp3d 1145 . . . 4 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„+)
334330, 332, 333lemul2d 13006 . . 3 (๐œ‘ โ†’ ((((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘)) โ‰ค ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))) โ†” ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰))))))
335326, 334mpbid 231 . 2 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ((๐‘ˆ โˆ’ ๐ธ) ยท ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
336333rpcnd 12964 . . 3 (๐œ‘ โ†’ (๐‘ˆ โˆ’ ๐ธ) โˆˆ โ„‚)
337331recnd 11188 . . 3 (๐œ‘ โ†’ ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)) โˆˆ โ„‚)
338336, 319, 337mul12d 11369 . 2 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท ((โ™ฏโ€˜๐ผ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))) = ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
339335, 338breqtrd 5132 1 (๐œ‘ โ†’ ((๐‘ˆ โˆ’ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ€˜๐‘))) โ‰ค ((โ™ฏโ€˜๐ผ) ยท ((๐‘ˆ โˆ’ ๐ธ) ยท ((logโ€˜(๐‘ / ๐‘‰)) / (๐‘ / ๐‘‰)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070   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  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-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-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-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
This theorem is referenced by:  pntlemj  26967
  Copyright terms: Public domain W3C validator