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

Theorem rplogsumlem2 26849
Description: Lemma for rplogsum 26891. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.)
Assertion
Ref Expression
rplogsumlem2 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘› โˆˆ (1...๐ด)(((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) โ‰ค 2)
Distinct variable group:   ๐ด,๐‘›

Proof of Theorem rplogsumlem2
Dummy variables ๐‘˜ ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 flid 13720 . . . . 5 (๐ด โˆˆ โ„ค โ†’ (โŒŠโ€˜๐ด) = ๐ด)
21oveq2d 7378 . . . 4 (๐ด โˆˆ โ„ค โ†’ (1...(โŒŠโ€˜๐ด)) = (1...๐ด))
32sumeq1d 15593 . . 3 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))(((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) = ฮฃ๐‘› โˆˆ (1...๐ด)(((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›))
4 fveq2 6847 . . . . . 6 (๐‘› = (๐‘โ†‘๐‘˜) โ†’ (ฮ›โ€˜๐‘›) = (ฮ›โ€˜(๐‘โ†‘๐‘˜)))
5 eleq1 2826 . . . . . . 7 (๐‘› = (๐‘โ†‘๐‘˜) โ†’ (๐‘› โˆˆ โ„™ โ†” (๐‘โ†‘๐‘˜) โˆˆ โ„™))
6 fveq2 6847 . . . . . . 7 (๐‘› = (๐‘โ†‘๐‘˜) โ†’ (logโ€˜๐‘›) = (logโ€˜(๐‘โ†‘๐‘˜)))
75, 6ifbieq1d 4515 . . . . . 6 (๐‘› = (๐‘โ†‘๐‘˜) โ†’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0) = if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0))
84, 7oveq12d 7380 . . . . 5 (๐‘› = (๐‘โ†‘๐‘˜) โ†’ ((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) = ((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)))
9 id 22 . . . . 5 (๐‘› = (๐‘โ†‘๐‘˜) โ†’ ๐‘› = (๐‘โ†‘๐‘˜))
108, 9oveq12d 7380 . . . 4 (๐‘› = (๐‘โ†‘๐‘˜) โ†’ (((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) = (((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)))
11 zre 12510 . . . 4 (๐ด โˆˆ โ„ค โ†’ ๐ด โˆˆ โ„)
12 elfznn 13477 . . . . . . . . 9 (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โ†’ ๐‘› โˆˆ โ„•)
1312adantl 483 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ ๐‘› โˆˆ โ„•)
14 vmacl 26483 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (ฮ›โ€˜๐‘›) โˆˆ โ„)
1513, 14syl 17 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ (ฮ›โ€˜๐‘›) โˆˆ โ„)
1613nnrpd 12962 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ ๐‘› โˆˆ โ„+)
1716relogcld 25994 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
18 0re 11164 . . . . . . . 8 0 โˆˆ โ„
19 ifcl 4536 . . . . . . . 8 (((logโ€˜๐‘›) โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0) โˆˆ โ„)
2017, 18, 19sylancl 587 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0) โˆˆ โ„)
2115, 20resubcld 11590 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ ((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) โˆˆ โ„)
2221, 13nndivred 12214 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ (((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) โˆˆ โ„)
2322recnd 11190 . . . 4 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ (((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) โˆˆ โ„‚)
24 simprr 772 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ (ฮ›โ€˜๐‘›) = 0)
25 vmaprm 26482 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„™ โ†’ (ฮ›โ€˜๐‘›) = (logโ€˜๐‘›))
26 prmnn 16557 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„™ โ†’ ๐‘› โˆˆ โ„•)
2726nnred 12175 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„™ โ†’ ๐‘› โˆˆ โ„)
28 prmgt1 16580 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„™ โ†’ 1 < ๐‘›)
2927, 28rplogcld 26000 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„™ โ†’ (logโ€˜๐‘›) โˆˆ โ„+)
3025, 29eqeltrd 2838 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„™ โ†’ (ฮ›โ€˜๐‘›) โˆˆ โ„+)
3130rpne0d 12969 . . . . . . . . . . 11 (๐‘› โˆˆ โ„™ โ†’ (ฮ›โ€˜๐‘›) โ‰  0)
3231necon2bi 2975 . . . . . . . . . 10 ((ฮ›โ€˜๐‘›) = 0 โ†’ ยฌ ๐‘› โˆˆ โ„™)
3332ad2antll 728 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ ยฌ ๐‘› โˆˆ โ„™)
3433iffalsed 4502 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0) = 0)
3524, 34oveq12d 7380 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ ((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) = (0 โˆ’ 0))
36 0m0e0 12280 . . . . . . 7 (0 โˆ’ 0) = 0
3735, 36eqtrdi 2793 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ ((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) = 0)
3837oveq1d 7377 . . . . 5 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ (((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) = (0 / ๐‘›))
3912ad2antrl 727 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ ๐‘› โˆˆ โ„•)
4039nnrpd 12962 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ ๐‘› โˆˆ โ„+)
4140rpcnne0d 12973 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ (๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0))
42 div0 11850 . . . . . 6 ((๐‘› โˆˆ โ„‚ โˆง ๐‘› โ‰  0) โ†’ (0 / ๐‘›) = 0)
4341, 42syl 17 . . . . 5 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ (0 / ๐‘›) = 0)
4438, 43eqtrd 2777 . . . 4 ((๐ด โˆˆ โ„ค โˆง (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โˆง (ฮ›โ€˜๐‘›) = 0)) โ†’ (((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) = 0)
4510, 11, 23, 44fsumvma2 26578 . . 3 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))(((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) = ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)))
463, 45eqtr3d 2779 . 2 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘› โˆˆ (1...๐ด)(((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) = ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)))
47 fzfid 13885 . . . . 5 (๐ด โˆˆ โ„ค โ†’ (2...((absโ€˜๐ด) + 1)) โˆˆ Fin)
48 simpr 486 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™))
4948elin2d 4164 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โˆˆ โ„™)
50 prmnn 16557 . . . . . . . . . . 11 (๐‘ โˆˆ โ„™ โ†’ ๐‘ โˆˆ โ„•)
5149, 50syl 17 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โˆˆ โ„•)
5251nnred 12175 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โˆˆ โ„)
5311adantr 482 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐ด โˆˆ โ„)
54 zcn 12511 . . . . . . . . . . . 12 (๐ด โˆˆ โ„ค โ†’ ๐ด โˆˆ โ„‚)
5554abscld 15328 . . . . . . . . . . 11 (๐ด โˆˆ โ„ค โ†’ (absโ€˜๐ด) โˆˆ โ„)
56 peano2re 11335 . . . . . . . . . . 11 ((absโ€˜๐ด) โˆˆ โ„ โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„)
5755, 56syl 17 . . . . . . . . . 10 (๐ด โˆˆ โ„ค โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„)
5857adantr 482 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„)
59 elinel1 4160 . . . . . . . . . . . 12 (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โ†’ ๐‘ โˆˆ (0[,]๐ด))
60 elicc2 13336 . . . . . . . . . . . . 13 ((0 โˆˆ โ„ โˆง ๐ด โˆˆ โ„) โ†’ (๐‘ โˆˆ (0[,]๐ด) โ†” (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ โˆง ๐‘ โ‰ค ๐ด)))
6118, 11, 60sylancr 588 . . . . . . . . . . . 12 (๐ด โˆˆ โ„ค โ†’ (๐‘ โˆˆ (0[,]๐ด) โ†” (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ โˆง ๐‘ โ‰ค ๐ด)))
6259, 61imbitrid 243 . . . . . . . . . . 11 (๐ด โˆˆ โ„ค โ†’ (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โ†’ (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ โˆง ๐‘ โ‰ค ๐ด)))
6362imp 408 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ โˆง ๐‘ โ‰ค ๐ด))
6463simp3d 1145 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โ‰ค ๐ด)
6554adantr 482 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐ด โˆˆ โ„‚)
6665abscld 15328 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (absโ€˜๐ด) โˆˆ โ„)
6753leabsd 15306 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐ด โ‰ค (absโ€˜๐ด))
6866lep1d 12093 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (absโ€˜๐ด) โ‰ค ((absโ€˜๐ด) + 1))
6953, 66, 58, 67, 68letrd 11319 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐ด โ‰ค ((absโ€˜๐ด) + 1))
7052, 53, 58, 64, 69letrd 11319 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โ‰ค ((absโ€˜๐ด) + 1))
71 prmuz2 16579 . . . . . . . . . 10 (๐‘ โˆˆ โ„™ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2))
7249, 71syl 17 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2))
73 nn0abscl 15204 . . . . . . . . . . . 12 (๐ด โˆˆ โ„ค โ†’ (absโ€˜๐ด) โˆˆ โ„•0)
74 nn0p1nn 12459 . . . . . . . . . . . 12 ((absโ€˜๐ด) โˆˆ โ„•0 โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„•)
7573, 74syl 17 . . . . . . . . . . 11 (๐ด โˆˆ โ„ค โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„•)
7675nnzd 12533 . . . . . . . . . 10 (๐ด โˆˆ โ„ค โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„ค)
7776adantr 482 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((absโ€˜๐ด) + 1) โˆˆ โ„ค)
78 elfz5 13440 . . . . . . . . 9 ((๐‘ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ((absโ€˜๐ด) + 1) โˆˆ โ„ค) โ†’ (๐‘ โˆˆ (2...((absโ€˜๐ด) + 1)) โ†” ๐‘ โ‰ค ((absโ€˜๐ด) + 1)))
7972, 77, 78syl2anc 585 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ โˆˆ (2...((absโ€˜๐ด) + 1)) โ†” ๐‘ โ‰ค ((absโ€˜๐ด) + 1)))
8070, 79mpbird 257 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1)))
8180ex 414 . . . . . 6 (๐ด โˆˆ โ„ค โ†’ (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โ†’ ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))))
8281ssrdv 3955 . . . . 5 (๐ด โˆˆ โ„ค โ†’ ((0[,]๐ด) โˆฉ โ„™) โŠ† (2...((absโ€˜๐ด) + 1)))
8347, 82ssfid 9218 . . . 4 (๐ด โˆˆ โ„ค โ†’ ((0[,]๐ด) โˆฉ โ„™) โˆˆ Fin)
84 fzfid 13885 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) โˆˆ Fin)
85 simprl 770 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™))
8685elin2d 4164 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ ๐‘ โˆˆ โ„™)
87 elfznn 13477 . . . . . . . . . . 11 (๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) โ†’ ๐‘˜ โˆˆ โ„•)
8887ad2antll 728 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ ๐‘˜ โˆˆ โ„•)
89 vmappw 26481 . . . . . . . . . 10 ((๐‘ โˆˆ โ„™ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (ฮ›โ€˜(๐‘โ†‘๐‘˜)) = (logโ€˜๐‘))
9086, 88, 89syl2anc 585 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ (ฮ›โ€˜(๐‘โ†‘๐‘˜)) = (logโ€˜๐‘))
9151adantrr 716 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ ๐‘ โˆˆ โ„•)
9291nnrpd 12962 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ ๐‘ โˆˆ โ„+)
9392relogcld 25994 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ (logโ€˜๐‘) โˆˆ โ„)
9490, 93eqeltrd 2838 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ (ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆˆ โ„)
9588nnnn0d 12480 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ ๐‘˜ โˆˆ โ„•0)
96 nnexpcl 13987 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐‘โ†‘๐‘˜) โˆˆ โ„•)
9791, 95, 96syl2anc 585 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ (๐‘โ†‘๐‘˜) โˆˆ โ„•)
9897nnrpd 12962 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ (๐‘โ†‘๐‘˜) โˆˆ โ„+)
9998relogcld 25994 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ (logโ€˜(๐‘โ†‘๐‘˜)) โˆˆ โ„)
100 ifcl 4536 . . . . . . . . 9 (((logโ€˜(๐‘โ†‘๐‘˜)) โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0) โˆˆ โ„)
10199, 18, 100sylancl 587 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0) โˆˆ โ„)
10294, 101resubcld 11590 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ ((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) โˆˆ โ„)
103102, 97nndivred 12214 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ (((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โˆˆ โ„)
104103anassrs 469 . . . . 5 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ (((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โˆˆ โ„)
10584, 104fsumrecl 15626 . . . 4 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โˆˆ โ„)
10683, 105fsumrecl 15626 . . 3 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โˆˆ โ„)
10751nnrpd 12962 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โˆˆ โ„+)
108107relogcld 25994 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (logโ€˜๐‘) โˆˆ โ„)
109 uz2m1nn 12855 . . . . . . 7 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
11072, 109syl 17 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
11151, 110nnmulcld 12213 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ ยท (๐‘ โˆ’ 1)) โˆˆ โ„•)
112108, 111nndivred 12214 . . . 4 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โˆˆ โ„)
11383, 112fsumrecl 15626 . . 3 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โˆˆ โ„)
114 2re 12234 . . . 4 2 โˆˆ โ„
115114a1i 11 . . 3 (๐ด โˆˆ โ„ค โ†’ 2 โˆˆ โ„)
11618a1i 11 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 0 โˆˆ โ„)
11751nngt0d 12209 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 0 < ๐‘)
118116, 52, 53, 117, 64ltletrd 11322 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 0 < ๐ด)
11953, 118elrpd 12961 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐ด โˆˆ โ„+)
120119relogcld 25994 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (logโ€˜๐ด) โˆˆ โ„)
121 prmgt1 16580 . . . . . . . . . . . 12 (๐‘ โˆˆ โ„™ โ†’ 1 < ๐‘)
12249, 121syl 17 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 1 < ๐‘)
12352, 122rplogcld 26000 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (logโ€˜๐‘) โˆˆ โ„+)
124120, 123rerpdivcld 12995 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((logโ€˜๐ด) / (logโ€˜๐‘)) โˆˆ โ„)
125123rpcnd 12966 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (logโ€˜๐‘) โˆˆ โ„‚)
126125mulid2d 11180 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 ยท (logโ€˜๐‘)) = (logโ€˜๐‘))
127107, 119logled 25998 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ โ‰ค ๐ด โ†” (logโ€˜๐‘) โ‰ค (logโ€˜๐ด)))
12864, 127mpbid 231 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (logโ€˜๐‘) โ‰ค (logโ€˜๐ด))
129126, 128eqbrtrd 5132 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 ยท (logโ€˜๐‘)) โ‰ค (logโ€˜๐ด))
130 1re 11162 . . . . . . . . . . . 12 1 โˆˆ โ„
131130a1i 11 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 1 โˆˆ โ„)
132131, 120, 123lemuldivd 13013 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 ยท (logโ€˜๐‘)) โ‰ค (logโ€˜๐ด) โ†” 1 โ‰ค ((logโ€˜๐ด) / (logโ€˜๐‘))))
133129, 132mpbid 231 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 1 โ‰ค ((logโ€˜๐ด) / (logโ€˜๐‘)))
134 flge1nn 13733 . . . . . . . . 9 ((((logโ€˜๐ด) / (logโ€˜๐‘)) โˆˆ โ„ โˆง 1 โ‰ค ((logโ€˜๐ด) / (logโ€˜๐‘))) โ†’ (โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) โˆˆ โ„•)
135124, 133, 134syl2anc 585 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) โˆˆ โ„•)
136 nnuz 12813 . . . . . . . 8 โ„• = (โ„คโ‰ฅโ€˜1)
137135, 136eleqtrdi 2848 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) โˆˆ (โ„คโ‰ฅโ€˜1))
138103recnd 11190 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง (๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))) โ†’ (((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โˆˆ โ„‚)
139138anassrs 469 . . . . . . 7 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ (((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โˆˆ โ„‚)
140 oveq2 7370 . . . . . . . . . 10 (๐‘˜ = 1 โ†’ (๐‘โ†‘๐‘˜) = (๐‘โ†‘1))
141140fveq2d 6851 . . . . . . . . 9 (๐‘˜ = 1 โ†’ (ฮ›โ€˜(๐‘โ†‘๐‘˜)) = (ฮ›โ€˜(๐‘โ†‘1)))
142140eleq1d 2823 . . . . . . . . . 10 (๐‘˜ = 1 โ†’ ((๐‘โ†‘๐‘˜) โˆˆ โ„™ โ†” (๐‘โ†‘1) โˆˆ โ„™))
143140fveq2d 6851 . . . . . . . . . 10 (๐‘˜ = 1 โ†’ (logโ€˜(๐‘โ†‘๐‘˜)) = (logโ€˜(๐‘โ†‘1)))
144142, 143ifbieq1d 4515 . . . . . . . . 9 (๐‘˜ = 1 โ†’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0) = if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0))
145141, 144oveq12d 7380 . . . . . . . 8 (๐‘˜ = 1 โ†’ ((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) = ((ฮ›โ€˜(๐‘โ†‘1)) โˆ’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0)))
146145, 140oveq12d 7380 . . . . . . 7 (๐‘˜ = 1 โ†’ (((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) = (((ฮ›โ€˜(๐‘โ†‘1)) โˆ’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0)) / (๐‘โ†‘1)))
147137, 139, 146fsum1p 15645 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) = ((((ฮ›โ€˜(๐‘โ†‘1)) โˆ’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0)) / (๐‘โ†‘1)) + ฮฃ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜))))
14851nncnd 12176 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โˆˆ โ„‚)
149148exp1d 14053 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘โ†‘1) = ๐‘)
150149fveq2d 6851 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (ฮ›โ€˜(๐‘โ†‘1)) = (ฮ›โ€˜๐‘))
151 vmaprm 26482 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„™ โ†’ (ฮ›โ€˜๐‘) = (logโ€˜๐‘))
15249, 151syl 17 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (ฮ›โ€˜๐‘) = (logโ€˜๐‘))
153150, 152eqtrd 2777 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (ฮ›โ€˜(๐‘โ†‘1)) = (logโ€˜๐‘))
154149, 49eqeltrd 2838 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘โ†‘1) โˆˆ โ„™)
155154iftrued 4499 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0) = (logโ€˜(๐‘โ†‘1)))
156149fveq2d 6851 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (logโ€˜(๐‘โ†‘1)) = (logโ€˜๐‘))
157155, 156eqtrd 2777 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0) = (logโ€˜๐‘))
158153, 157oveq12d 7380 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((ฮ›โ€˜(๐‘โ†‘1)) โˆ’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0)) = ((logโ€˜๐‘) โˆ’ (logโ€˜๐‘)))
159125subidd 11507 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((logโ€˜๐‘) โˆ’ (logโ€˜๐‘)) = 0)
160158, 159eqtrd 2777 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((ฮ›โ€˜(๐‘โ†‘1)) โˆ’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0)) = 0)
161160, 149oveq12d 7380 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((ฮ›โ€˜(๐‘โ†‘1)) โˆ’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0)) / (๐‘โ†‘1)) = (0 / ๐‘))
162107rpcnne0d 12973 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0))
163 div0 11850 . . . . . . . . 9 ((๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0) โ†’ (0 / ๐‘) = 0)
164162, 163syl 17 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (0 / ๐‘) = 0)
165161, 164eqtrd 2777 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((ฮ›โ€˜(๐‘โ†‘1)) โˆ’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0)) / (๐‘โ†‘1)) = 0)
166 1p1e2 12285 . . . . . . . . . 10 (1 + 1) = 2
167166oveq1i 7372 . . . . . . . . 9 ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) = (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))
168167a1i 11 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) = (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))))
169 elfzuz 13444 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2))
170 eluz2nn 12816 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘˜ โˆˆ โ„•)
171169, 170syl 17 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) โ†’ ๐‘˜ โˆˆ โ„•)
172171, 167eleq2s 2856 . . . . . . . . . . . 12 (๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) โ†’ ๐‘˜ โˆˆ โ„•)
17349, 172, 89syl2an 597 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ (ฮ›โ€˜(๐‘โ†‘๐‘˜)) = (logโ€˜๐‘))
17451adantr 482 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ๐‘ โˆˆ โ„•)
175 nnq 12894 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„š)
176174, 175syl 17 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ๐‘ โˆˆ โ„š)
177169, 167eleq2s 2856 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2))
178177adantl 483 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2))
179 expnprm 16781 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„š โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ยฌ (๐‘โ†‘๐‘˜) โˆˆ โ„™)
180176, 178, 179syl2anc 585 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ยฌ (๐‘โ†‘๐‘˜) โˆˆ โ„™)
181180iffalsed 4502 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0) = 0)
182173, 181oveq12d 7380 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) = ((logโ€˜๐‘) โˆ’ 0))
183125subid1d 11508 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((logโ€˜๐‘) โˆ’ 0) = (logโ€˜๐‘))
184183adantr 482 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ((logโ€˜๐‘) โˆ’ 0) = (logโ€˜๐‘))
185182, 184eqtrd 2777 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) = (logโ€˜๐‘))
186185oveq1d 7377 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ (((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) = ((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)))
187168, 186sumeq12dv 15598 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) = ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)))
188165, 187oveq12d 7380 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((((ฮ›โ€˜(๐‘โ†‘1)) โˆ’ if((๐‘โ†‘1) โˆˆ โ„™, (logโ€˜(๐‘โ†‘1)), 0)) / (๐‘โ†‘1)) + ฮฃ๐‘˜ โˆˆ ((1 + 1)...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜))) = (0 + ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜))))
189 fzfid 13885 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) โˆˆ Fin)
190108adantr 482 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (logโ€˜๐‘) โˆˆ โ„)
191 nnnn0 12427 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„•0)
19251, 191, 96syl2an 597 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘โ†‘๐‘˜) โˆˆ โ„•)
193190, 192nndivred 12214 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) โˆˆ โ„)
194171, 193sylan2 594 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) โˆˆ โ„)
195189, 194fsumrecl 15626 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) โˆˆ โ„)
196195recnd 11190 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) โˆˆ โ„‚)
197196addid2d 11363 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (0 + ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)))
198147, 188, 1973eqtrd 2781 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) = ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)))
199107rpreccld 12974 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 / ๐‘) โˆˆ โ„+)
200124flcld 13710 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) โˆˆ โ„ค)
201200peano2zd 12617 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1) โˆˆ โ„ค)
202199, 201rpexpcld 14157 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1)) โˆˆ โ„+)
203202rpge0d 12968 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 0 โ‰ค ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1)))
20451nnrecred 12211 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 / ๐‘) โˆˆ โ„)
205204resqcld 14037 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 / ๐‘)โ†‘2) โˆˆ โ„)
206135peano2nnd 12177 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1) โˆˆ โ„•)
207206nnnn0d 12480 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1) โˆˆ โ„•0)
208204, 207reexpcld 14075 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1)) โˆˆ โ„)
209205, 208subge02d 11754 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (0 โ‰ค ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1)) โ†” (((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) โ‰ค ((1 / ๐‘)โ†‘2)))
210203, 209mpbid 231 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) โ‰ค ((1 / ๐‘)โ†‘2))
211110nnrpd 12962 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„+)
212211rpcnne0d 12973 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((๐‘ โˆ’ 1) โˆˆ โ„‚ โˆง (๐‘ โˆ’ 1) โ‰  0))
213199rpcnd 12966 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 / ๐‘) โˆˆ โ„‚)
214 dmdcan 11872 . . . . . . . . . . 11 ((((๐‘ โˆ’ 1) โˆˆ โ„‚ โˆง (๐‘ โˆ’ 1) โ‰  0) โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0) โˆง (1 / ๐‘) โˆˆ โ„‚) โ†’ (((๐‘ โˆ’ 1) / ๐‘) ยท ((1 / ๐‘) / (๐‘ โˆ’ 1))) = ((1 / ๐‘) / ๐‘))
215212, 162, 213, 214syl3anc 1372 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((๐‘ โˆ’ 1) / ๐‘) ยท ((1 / ๐‘) / (๐‘ โˆ’ 1))) = ((1 / ๐‘) / ๐‘))
216131recnd 11190 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 1 โˆˆ โ„‚)
217 divsubdir 11856 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0)) โ†’ ((๐‘ โˆ’ 1) / ๐‘) = ((๐‘ / ๐‘) โˆ’ (1 / ๐‘)))
218148, 216, 162, 217syl3anc 1372 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((๐‘ โˆ’ 1) / ๐‘) = ((๐‘ / ๐‘) โˆ’ (1 / ๐‘)))
219 divid 11849 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0) โ†’ (๐‘ / ๐‘) = 1)
220162, 219syl 17 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ / ๐‘) = 1)
221220oveq1d 7377 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((๐‘ / ๐‘) โˆ’ (1 / ๐‘)) = (1 โˆ’ (1 / ๐‘)))
222218, 221eqtrd 2777 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((๐‘ โˆ’ 1) / ๐‘) = (1 โˆ’ (1 / ๐‘)))
223 divdiv1 11873 . . . . . . . . . . . 12 ((1 โˆˆ โ„‚ โˆง (๐‘ โˆˆ โ„‚ โˆง ๐‘ โ‰  0) โˆง ((๐‘ โˆ’ 1) โˆˆ โ„‚ โˆง (๐‘ โˆ’ 1) โ‰  0)) โ†’ ((1 / ๐‘) / (๐‘ โˆ’ 1)) = (1 / (๐‘ ยท (๐‘ โˆ’ 1))))
224216, 162, 212, 223syl3anc 1372 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 / ๐‘) / (๐‘ โˆ’ 1)) = (1 / (๐‘ ยท (๐‘ โˆ’ 1))))
225222, 224oveq12d 7380 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((๐‘ โˆ’ 1) / ๐‘) ยท ((1 / ๐‘) / (๐‘ โˆ’ 1))) = ((1 โˆ’ (1 / ๐‘)) ยท (1 / (๐‘ ยท (๐‘ โˆ’ 1)))))
22651nnne0d 12210 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ๐‘ โ‰  0)
227213, 148, 226divrecd 11941 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 / ๐‘) / ๐‘) = ((1 / ๐‘) ยท (1 / ๐‘)))
228213sqvald 14055 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 / ๐‘)โ†‘2) = ((1 / ๐‘) ยท (1 / ๐‘)))
229227, 228eqtr4d 2780 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 / ๐‘) / ๐‘) = ((1 / ๐‘)โ†‘2))
230215, 225, 2293eqtr3d 2785 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 โˆ’ (1 / ๐‘)) ยท (1 / (๐‘ ยท (๐‘ โˆ’ 1)))) = ((1 / ๐‘)โ†‘2))
231210, 230breqtrrd 5138 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) โ‰ค ((1 โˆ’ (1 / ๐‘)) ยท (1 / (๐‘ ยท (๐‘ โˆ’ 1)))))
232205, 208resubcld 11590 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) โˆˆ โ„)
233111nnrecred 12211 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 / (๐‘ ยท (๐‘ โˆ’ 1))) โˆˆ โ„)
234 resubcl 11472 . . . . . . . . . 10 ((1 โˆˆ โ„ โˆง (1 / ๐‘) โˆˆ โ„) โ†’ (1 โˆ’ (1 / ๐‘)) โˆˆ โ„)
235130, 204, 234sylancr 588 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 โˆ’ (1 / ๐‘)) โˆˆ โ„)
236 recgt1 12058 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„ โˆง 0 < ๐‘) โ†’ (1 < ๐‘ โ†” (1 / ๐‘) < 1))
23752, 117, 236syl2anc 585 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 < ๐‘ โ†” (1 / ๐‘) < 1))
238122, 237mpbid 231 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 / ๐‘) < 1)
239 posdif 11655 . . . . . . . . . . 11 (((1 / ๐‘) โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ ((1 / ๐‘) < 1 โ†” 0 < (1 โˆ’ (1 / ๐‘))))
240204, 130, 239sylancl 587 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((1 / ๐‘) < 1 โ†” 0 < (1 โˆ’ (1 / ๐‘))))
241238, 240mpbid 231 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 0 < (1 โˆ’ (1 / ๐‘)))
242 ledivmul 12038 . . . . . . . . 9 (((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) โˆˆ โ„ โˆง (1 / (๐‘ ยท (๐‘ โˆ’ 1))) โˆˆ โ„ โˆง ((1 โˆ’ (1 / ๐‘)) โˆˆ โ„ โˆง 0 < (1 โˆ’ (1 / ๐‘)))) โ†’ (((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘))) โ‰ค (1 / (๐‘ ยท (๐‘ โˆ’ 1))) โ†” (((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) โ‰ค ((1 โˆ’ (1 / ๐‘)) ยท (1 / (๐‘ ยท (๐‘ โˆ’ 1))))))
243232, 233, 235, 241, 242syl112anc 1375 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘))) โ‰ค (1 / (๐‘ ยท (๐‘ โˆ’ 1))) โ†” (((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) โ‰ค ((1 โˆ’ (1 / ๐‘)) ยท (1 / (๐‘ ยท (๐‘ โˆ’ 1))))))
244231, 243mpbird 257 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘))) โ‰ค (1 / (๐‘ ยท (๐‘ โˆ’ 1))))
245235, 241elrpd 12961 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 โˆ’ (1 / ๐‘)) โˆˆ โ„+)
246232, 245rerpdivcld 12995 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘))) โˆˆ โ„)
247246, 233, 123lemul2d 13008 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘))) โ‰ค (1 / (๐‘ ยท (๐‘ โˆ’ 1))) โ†” ((logโ€˜๐‘) ยท ((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘)))) โ‰ค ((logโ€˜๐‘) ยท (1 / (๐‘ ยท (๐‘ โˆ’ 1))))))
248244, 247mpbid 231 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((logโ€˜๐‘) ยท ((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘)))) โ‰ค ((logโ€˜๐‘) ยท (1 / (๐‘ ยท (๐‘ โˆ’ 1)))))
249125adantr 482 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (logโ€˜๐‘) โˆˆ โ„‚)
250192nncnd 12176 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘โ†‘๐‘˜) โˆˆ โ„‚)
251192nnne0d 12210 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘โ†‘๐‘˜) โ‰  0)
252249, 250, 251divrecd 11941 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) = ((logโ€˜๐‘) ยท (1 / (๐‘โ†‘๐‘˜))))
253148adantr 482 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„‚)
25451adantr 482 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„•)
255254nnne0d 12210 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘ โ‰  0)
256 nnz 12527 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„ค)
257256adantl 483 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„ค)
258253, 255, 257exprecd 14066 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((1 / ๐‘)โ†‘๐‘˜) = (1 / (๐‘โ†‘๐‘˜)))
259258oveq2d 7378 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((logโ€˜๐‘) ยท ((1 / ๐‘)โ†‘๐‘˜)) = ((logโ€˜๐‘) ยท (1 / (๐‘โ†‘๐‘˜))))
260252, 259eqtr4d 2780 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) = ((logโ€˜๐‘) ยท ((1 / ๐‘)โ†‘๐‘˜)))
261171, 260sylan2 594 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) = ((logโ€˜๐‘) ยท ((1 / ๐‘)โ†‘๐‘˜)))
262261sumeq2dv 15595 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) = ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) ยท ((1 / ๐‘)โ†‘๐‘˜)))
263171nnnn0d 12480 . . . . . . . . 9 (๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) โ†’ ๐‘˜ โˆˆ โ„•0)
264 expcl 13992 . . . . . . . . 9 (((1 / ๐‘) โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((1 / ๐‘)โ†‘๐‘˜) โˆˆ โ„‚)
265213, 263, 264syl2an 597 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โˆง ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))) โ†’ ((1 / ๐‘)โ†‘๐‘˜) โˆˆ โ„‚)
266189, 125, 265fsummulc2 15676 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((logโ€˜๐‘) ยท ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((1 / ๐‘)โ†‘๐‘˜)) = ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) ยท ((1 / ๐‘)โ†‘๐‘˜)))
267 fzval3 13648 . . . . . . . . . . 11 ((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) โˆˆ โ„ค โ†’ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) = (2..^((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1)))
268200, 267syl 17 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘)))) = (2..^((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1)))
269268sumeq1d 15593 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((1 / ๐‘)โ†‘๐‘˜) = ฮฃ๐‘˜ โˆˆ (2..^((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))((1 / ๐‘)โ†‘๐‘˜))
270204, 238ltned 11298 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (1 / ๐‘) โ‰  1)
271 2nn0 12437 . . . . . . . . . . 11 2 โˆˆ โ„•0
272271a1i 11 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ 2 โˆˆ โ„•0)
273 eluzp1p1 12798 . . . . . . . . . . . 12 ((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ ((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1) โˆˆ (โ„คโ‰ฅโ€˜(1 + 1)))
274137, 273syl 17 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1) โˆˆ (โ„คโ‰ฅโ€˜(1 + 1)))
275 df-2 12223 . . . . . . . . . . . 12 2 = (1 + 1)
276275fveq2i 6850 . . . . . . . . . . 11 (โ„คโ‰ฅโ€˜2) = (โ„คโ‰ฅโ€˜(1 + 1))
277274, 276eleqtrrdi 2849 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1) โˆˆ (โ„คโ‰ฅโ€˜2))
278213, 270, 272, 277geoserg 15758 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (2..^((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))((1 / ๐‘)โ†‘๐‘˜) = ((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘))))
279269, 278eqtrd 2777 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((1 / ๐‘)โ†‘๐‘˜) = ((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘))))
280279oveq2d 7378 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((logโ€˜๐‘) ยท ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((1 / ๐‘)โ†‘๐‘˜)) = ((logโ€˜๐‘) ยท ((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘)))))
281262, 266, 2803eqtr2d 2783 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) = ((logโ€˜๐‘) ยท ((((1 / ๐‘)โ†‘2) โˆ’ ((1 / ๐‘)โ†‘((โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))) + 1))) / (1 โˆ’ (1 / ๐‘)))))
282111nncnd 12176 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ ยท (๐‘ โˆ’ 1)) โˆˆ โ„‚)
283111nnne0d 12210 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ (๐‘ ยท (๐‘ โˆ’ 1)) โ‰  0)
284125, 282, 283divrecd 11941 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) = ((logโ€˜๐‘) ยท (1 / (๐‘ ยท (๐‘ โˆ’ 1)))))
285248, 281, 2843brtr4d 5142 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (2...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))((logโ€˜๐‘) / (๐‘โ†‘๐‘˜)) โ‰ค ((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))))
286198, 285eqbrtrd 5132 . . . 4 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)) โ†’ ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โ‰ค ((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))))
28783, 105, 112, 286fsumle 15691 . . 3 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โ‰ค ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))))
288 elfzuz 13444 . . . . . . . . . . 11 (๐‘ โˆˆ (2...((absโ€˜๐ด) + 1)) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2))
289 eluz2nn 12816 . . . . . . . . . . 11 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ โˆˆ โ„•)
290288, 289syl 17 . . . . . . . . . 10 (๐‘ โˆˆ (2...((absโ€˜๐ด) + 1)) โ†’ ๐‘ โˆˆ โ„•)
291290adantl 483 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ ๐‘ โˆˆ โ„•)
292291nnred 12175 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ ๐‘ โˆˆ โ„)
293288adantl 483 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2))
294 eluz2gt1 12852 . . . . . . . . 9 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ 1 < ๐‘)
295293, 294syl 17 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ 1 < ๐‘)
296292, 295rplogcld 26000 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ (logโ€˜๐‘) โˆˆ โ„+)
297293, 109syl 17 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
298291, 297nnmulcld 12213 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ (๐‘ ยท (๐‘ โˆ’ 1)) โˆˆ โ„•)
299298nnrpd 12962 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ (๐‘ ยท (๐‘ โˆ’ 1)) โˆˆ โ„+)
300296, 299rpdivcld 12981 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ ((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โˆˆ โ„+)
301300rpred 12964 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ ((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โˆˆ โ„)
30247, 301fsumrecl 15626 . . . 4 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โˆˆ โ„)
303300rpge0d 12968 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))) โ†’ 0 โ‰ค ((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))))
30447, 301, 303, 82fsumless 15688 . . . 4 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โ‰ค ฮฃ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))))
305 rplogsumlem1 26848 . . . . 5 (((absโ€˜๐ด) + 1) โˆˆ โ„• โ†’ ฮฃ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โ‰ค 2)
30675, 305syl 17 . . . 4 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘ โˆˆ (2...((absโ€˜๐ด) + 1))((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โ‰ค 2)
307113, 302, 115, 304, 306letrd 11319 . . 3 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)((logโ€˜๐‘) / (๐‘ ยท (๐‘ โˆ’ 1))) โ‰ค 2)
308106, 113, 115, 287, 307letrd 11319 . 2 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘ โˆˆ ((0[,]๐ด) โˆฉ โ„™)ฮฃ๐‘˜ โˆˆ (1...(โŒŠโ€˜((logโ€˜๐ด) / (logโ€˜๐‘))))(((ฮ›โ€˜(๐‘โ†‘๐‘˜)) โˆ’ if((๐‘โ†‘๐‘˜) โˆˆ โ„™, (logโ€˜(๐‘โ†‘๐‘˜)), 0)) / (๐‘โ†‘๐‘˜)) โ‰ค 2)
30946, 308eqbrtrd 5132 1 (๐ด โˆˆ โ„ค โ†’ ฮฃ๐‘› โˆˆ (1...๐ด)(((ฮ›โ€˜๐‘›) โˆ’ if(๐‘› โˆˆ โ„™, (logโ€˜๐‘›), 0)) / ๐‘›) โ‰ค 2)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944   โˆฉ cin 3914  ifcif 4491   class class class wbr 5110  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392   / cdiv 11819  โ„•cn 12160  2c2 12215  โ„•0cn0 12420  โ„คcz 12506  โ„คโ‰ฅcuz 12770  โ„šcq 12880  โ„+crp 12922  [,]cicc 13274  ...cfz 13431  ..^cfzo 13574  โŒŠcfl 13702  โ†‘cexp 13974  abscabs 15126  ฮฃcsu 15577  โ„™cprime 16554  logclog 25926  ฮ›cvma 26457
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-tan 15961  df-pi 15962  df-dvds 16144  df-gcd 16382  df-prm 16555  df-pc 16716  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  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-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-cxp 25929  df-vma 26463
This theorem is referenced by:  rplogsum  26891
  Copyright terms: Public domain W3C validator