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

Theorem selberg4lem1 26924
Description: Lemma for selberg4 26925. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Hypotheses
Ref Expression
selberg4lem1.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„+)
selberg4lem1.2 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ (1[,)+โˆž)(absโ€˜((ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) / ๐‘ฆ) โˆ’ (2 ยท (logโ€˜๐‘ฆ)))) โ‰ค ๐ด)
Assertion
Ref Expression
selberg4lem1 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
Distinct variable groups:   ๐‘–,๐‘š,๐‘›,๐‘ฅ,๐‘ฆ,๐ด   ๐œ‘,๐‘š,๐‘›,๐‘ฅ
Allowed substitution hints:   ๐œ‘(๐‘ฆ,๐‘–)

Proof of Theorem selberg4lem1
StepHypRef Expression
1 2cnd 12238 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 2 โˆˆ โ„‚)
2 fzfid 13885 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (1...(โŒŠโ€˜๐‘ฅ)) โˆˆ Fin)
3 elfznn 13477 . . . . . . . . . . . . 13 (๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ)) โ†’ ๐‘› โˆˆ โ„•)
43adantl 483 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘› โˆˆ โ„•)
5 vmacl 26483 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (ฮ›โ€˜๐‘›) โˆˆ โ„)
64, 5syl 17 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (ฮ›โ€˜๐‘›) โˆˆ โ„)
76, 4nndivred 12214 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) / ๐‘›) โˆˆ โ„)
8 elioore 13301 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ (1(,)+โˆž) โ†’ ๐‘ฅ โˆˆ โ„)
98adantl 483 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ๐‘ฅ โˆˆ โ„)
10 1rp 12926 . . . . . . . . . . . . . . 15 1 โˆˆ โ„+
1110a1i 11 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 1 โˆˆ โ„+)
12 1red 11163 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 1 โˆˆ โ„)
13 eliooord 13330 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ (1(,)+โˆž) โ†’ (1 < ๐‘ฅ โˆง ๐‘ฅ < +โˆž))
1413adantl 483 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (1 < ๐‘ฅ โˆง ๐‘ฅ < +โˆž))
1514simpld 496 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 1 < ๐‘ฅ)
1612, 9, 15ltled 11310 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 1 โ‰ค ๐‘ฅ)
179, 11, 16rpgecld 13003 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ๐‘ฅ โˆˆ โ„+)
1817adantr 482 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘ฅ โˆˆ โ„+)
194nnrpd 12962 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘› โˆˆ โ„+)
2018, 19rpdivcld 12981 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (๐‘ฅ / ๐‘›) โˆˆ โ„+)
2120relogcld 25994 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (logโ€˜(๐‘ฅ / ๐‘›)) โˆˆ โ„)
227, 21remulcld 11192 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) โˆˆ โ„)
232, 22fsumrecl 15626 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) โˆˆ โ„)
249, 15rplogcld 26000 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (logโ€˜๐‘ฅ) โˆˆ โ„+)
2523, 24rerpdivcld 12995 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆˆ โ„)
2625recnd 11190 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆˆ โ„‚)
2717relogcld 25994 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (logโ€˜๐‘ฅ) โˆˆ โ„)
2827rehalfcld 12407 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((logโ€˜๐‘ฅ) / 2) โˆˆ โ„)
2928recnd 11190 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((logโ€˜๐‘ฅ) / 2) โˆˆ โ„‚)
301, 26, 29subdid 11618 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (2 ยท ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / 2))) = ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (2 ยท ((logโ€˜๐‘ฅ) / 2))))
3127recnd 11190 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (logโ€˜๐‘ฅ) โˆˆ โ„‚)
32 2ne0 12264 . . . . . . . 8 2 โ‰  0
3332a1i 11 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 2 โ‰  0)
3431, 1, 33divcan2d 11940 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (2 ยท ((logโ€˜๐‘ฅ) / 2)) = (logโ€˜๐‘ฅ))
3534oveq2d 7378 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (2 ยท ((logโ€˜๐‘ฅ) / 2))) = ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)))
3630, 35eqtrd 2777 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (2 ยท ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / 2))) = ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)))
3736mpteq2dva 5210 . . 3 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (2 ยท ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / 2)))) = (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ))))
38 2re 12234 . . . . 5 2 โˆˆ โ„
3938a1i 11 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 2 โˆˆ โ„)
4025, 28resubcld 11590 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / 2)) โˆˆ โ„)
41 ioossre 13332 . . . . . 6 (1(,)+โˆž) โŠ† โ„
42 2cn 12235 . . . . . 6 2 โˆˆ โ„‚
43 o1const 15509 . . . . . 6 (((1(,)+โˆž) โŠ† โ„ โˆง 2 โˆˆ โ„‚) โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ 2) โˆˆ ๐‘‚(1))
4441, 42, 43mp2an 691 . . . . 5 (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ 2) โˆˆ ๐‘‚(1)
4544a1i 11 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ 2) โˆˆ ๐‘‚(1))
46 vmalogdivsum2 26902 . . . . 5 (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / 2))) โˆˆ ๐‘‚(1)
4746a1i 11 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / 2))) โˆˆ ๐‘‚(1))
4839, 40, 45, 47o1mul2 15514 . . 3 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (2 ยท ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / 2)))) โˆˆ ๐‘‚(1))
4937, 48eqeltrrd 2839 . 2 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
50 fzfid 13885 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›))) โˆˆ Fin)
51 elfznn 13477 . . . . . . . . . . . 12 (๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›))) โ†’ ๐‘š โˆˆ โ„•)
5251adantl 483 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ ๐‘š โˆˆ โ„•)
53 vmacl 26483 . . . . . . . . . . 11 (๐‘š โˆˆ โ„• โ†’ (ฮ›โ€˜๐‘š) โˆˆ โ„)
5452, 53syl 17 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ (ฮ›โ€˜๐‘š) โˆˆ โ„)
5552nnrpd 12962 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ ๐‘š โˆˆ โ„+)
5655relogcld 25994 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ (logโ€˜๐‘š) โˆˆ โ„)
579adantr 482 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘ฅ โˆˆ โ„)
5857, 4nndivred 12214 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (๐‘ฅ / ๐‘›) โˆˆ โ„)
5958adantr 482 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ (๐‘ฅ / ๐‘›) โˆˆ โ„)
6059, 52nndivred 12214 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ ((๐‘ฅ / ๐‘›) / ๐‘š) โˆˆ โ„)
61 chpcl 26489 . . . . . . . . . . . 12 (((๐‘ฅ / ๐‘›) / ๐‘š) โˆˆ โ„ โ†’ (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)) โˆˆ โ„)
6260, 61syl 17 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)) โˆˆ โ„)
6356, 62readdcld 11191 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))) โˆˆ โ„)
6454, 63remulcld 11192 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))) โ†’ ((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) โˆˆ โ„)
6550, 64fsumrecl 15626 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) โˆˆ โ„)
666, 65remulcld 11192 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) โˆˆ โ„)
672, 66fsumrecl 15626 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) โˆˆ โ„)
6817, 24rpmulcld 12980 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (๐‘ฅ ยท (logโ€˜๐‘ฅ)) โˆˆ โ„+)
6967, 68rerpdivcld 12995 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆˆ โ„)
7069, 27resubcld 11590 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)) โˆˆ โ„)
7170recnd 11190 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)) โˆˆ โ„‚)
7223recnd 11190 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) โˆˆ โ„‚)
7324rpne0d 12969 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (logโ€˜๐‘ฅ) โ‰  0)
7472, 31, 73divcld 11938 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)) โˆˆ โ„‚)
751, 74mulcld 11182 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆˆ โ„‚)
7675, 31subcld 11519 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)) โˆˆ โ„‚)
7769recnd 11190 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆˆ โ„‚)
7877, 75, 31nnncan2d 11554 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)) โˆ’ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ))) = ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)))))
7967recnd 11190 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) โˆˆ โ„‚)
809recnd 11190 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ๐‘ฅ โˆˆ โ„‚)
8117rpne0d 12969 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ๐‘ฅ โ‰  0)
8279, 80, 31, 81, 73divdiv1d 11969 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) / (logโ€˜๐‘ฅ)) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))))
831, 72, 31, 73divassd 11973 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) / (logโ€˜๐‘ฅ)) = (2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))))
8482, 83oveq12d 7380 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) / (logโ€˜๐‘ฅ)) โˆ’ ((2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) / (logโ€˜๐‘ฅ))) = ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ)))))
8567, 17rerpdivcld 12995 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆˆ โ„)
8685recnd 11190 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆˆ โ„‚)
871, 72mulcld 11182 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) โˆˆ โ„‚)
8886, 87, 31, 73divsubdird 11977 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ (2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))) / (logโ€˜๐‘ฅ)) = (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) / (logโ€˜๐‘ฅ)) โˆ’ ((2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) / (logโ€˜๐‘ฅ))))
8981adantr 482 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘ฅ โ‰  0)
9066, 57, 89redivcld 11990 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆˆ โ„)
9190recnd 11190 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆˆ โ„‚)
9238a1i 11 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ 2 โˆˆ โ„)
9392, 22remulcld 11192 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) โˆˆ โ„)
9493recnd 11190 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) โˆˆ โ„‚)
952, 91, 94fsumsub 15680 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ (2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))))
966recnd 11190 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (ฮ›โ€˜๐‘›) โˆˆ โ„‚)
9765, 57, 89redivcld 11990 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆˆ โ„)
9897recnd 11190 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆˆ โ„‚)
99 2cnd 12238 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ 2 โˆˆ โ„‚)
10021recnd 11190 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (logโ€˜(๐‘ฅ / ๐‘›)) โˆˆ โ„‚)
1014nncnd 12176 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘› โˆˆ โ„‚)
1024nnne0d 12210 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘› โ‰  0)
103100, 101, 102divcld 11938 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›) โˆˆ โ„‚)
10499, 103mulcld 11182 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)) โˆˆ โ„‚)
10596, 98, 104subdid 11618 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) = (((ฮ›โ€˜๐‘›) ยท (ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ)) โˆ’ ((ฮ›โ€˜๐‘›) ยท (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))))
10665recnd 11190 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) โˆˆ โ„‚)
10780adantr 482 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘ฅ โˆˆ โ„‚)
10896, 106, 107, 89divassd 11973 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) = ((ฮ›โ€˜๐‘›) ยท (ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ)))
10996, 101, 100, 102div32d 11961 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) = ((ฮ›โ€˜๐‘›) ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))
110109oveq2d 7378 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) = (2 ยท ((ฮ›โ€˜๐‘›) ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))
11199, 96, 103mul12d 11371 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท ((ฮ›โ€˜๐‘›) ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))) = ((ฮ›โ€˜๐‘›) ยท (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))
112110, 111eqtrd 2777 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) = ((ฮ›โ€˜๐‘›) ยท (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))
113108, 112oveq12d 7380 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ (2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))) = (((ฮ›โ€˜๐‘›) ยท (ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ)) โˆ’ ((ฮ›โ€˜๐‘›) ยท (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))))
114105, 113eqtr4d 2780 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) = ((((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ (2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))))
115114sumeq2dv 15595 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) = ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ (2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))))
11666recnd 11190 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) โˆˆ โ„‚)
1172, 80, 116, 81fsumdivc 15678 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) = ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ))
11822recnd 11190 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) โˆˆ โ„‚)
1192, 1, 118fsummulc2 15676 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) = ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))))
120117, 119oveq12d 7380 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ (2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(2 ยท (((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))))
12195, 115, 1203eqtr4rd 2788 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ (2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))) = ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))))
122121oveq1d 7377 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) โˆ’ (2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))))) / (logโ€˜๐‘ฅ)) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ)))
12388, 122eqtr3d 2779 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / ๐‘ฅ) / (logโ€˜๐‘ฅ)) โˆ’ ((2 ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›)))) / (logโ€˜๐‘ฅ))) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ)))
12478, 84, 1233eqtr2d 2783 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)) โˆ’ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ))) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ)))
125124mpteq2dva 5210 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)) โˆ’ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)))) = (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ))))
126 1red 11163 . . . . 5 (๐œ‘ โ†’ 1 โˆˆ โ„)
127 selberg4lem1.1 . . . . . . . 8 (๐œ‘ โ†’ ๐ด โˆˆ โ„+)
128127adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ๐ด โˆˆ โ„+)
129128rpred 12964 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ๐ด โˆˆ โ„)
1302, 7fsumrecl 15626 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆˆ โ„)
131130, 24rerpdivcld 12995 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)) โˆˆ โ„)
132127rpcnd 12966 . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
133 o1const 15509 . . . . . . 7 (((1(,)+โˆž) โŠ† โ„ โˆง ๐ด โˆˆ โ„‚) โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ๐ด) โˆˆ ๐‘‚(1))
13441, 132, 133sylancr 588 . . . . . 6 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ๐ด) โˆˆ ๐‘‚(1))
135 1cnd 11157 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
136 o1const 15509 . . . . . . . 8 (((1(,)+โˆž) โŠ† โ„ โˆง 1 โˆˆ โ„‚) โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ 1) โˆˆ ๐‘‚(1))
13741, 135, 136sylancr 588 . . . . . . 7 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ 1) โˆˆ ๐‘‚(1))
138131recnd 11190 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)) โˆˆ โ„‚)
139 1cnd 11157 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 1 โˆˆ โ„‚)
140130recnd 11190 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆˆ โ„‚)
141140, 31, 31, 73divsubdird 11977 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ)) / (logโ€˜๐‘ฅ)) = ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / (logโ€˜๐‘ฅ))))
142140, 31subcld 11519 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ)) โˆˆ โ„‚)
143142, 31, 73divrecd 11941 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ)) / (logโ€˜๐‘ฅ)) = ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ)) ยท (1 / (logโ€˜๐‘ฅ))))
14431, 73dividd 11936 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((logโ€˜๐‘ฅ) / (logโ€˜๐‘ฅ)) = 1)
145144oveq2d 7378 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)) โˆ’ ((logโ€˜๐‘ฅ) / (logโ€˜๐‘ฅ))) = ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)) โˆ’ 1))
146141, 143, 1453eqtr3d 2785 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ)) ยท (1 / (logโ€˜๐‘ฅ))) = ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)) โˆ’ 1))
147146mpteq2dva 5210 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ)) ยท (1 / (logโ€˜๐‘ฅ)))) = (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)) โˆ’ 1)))
148130, 27resubcld 11590 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ)) โˆˆ โ„)
14912, 24rerpdivcld 12995 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (1 / (logโ€˜๐‘ฅ)) โˆˆ โ„)
15017ex 414 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†’ ๐‘ฅ โˆˆ โ„+))
151150ssrdv 3955 . . . . . . . . . . 11 (๐œ‘ โ†’ (1(,)+โˆž) โŠ† โ„+)
152 vmadivsum 26846 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1)
153152a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
154151, 153o1res2 15452 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
155 divlogrlim 26006 . . . . . . . . . . 11 (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (1 / (logโ€˜๐‘ฅ))) โ‡๐‘Ÿ 0
156 rlimo1 15506 . . . . . . . . . . 11 ((๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (1 / (logโ€˜๐‘ฅ))) โ‡๐‘Ÿ 0 โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (1 / (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
157155, 156mp1i 13 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (1 / (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
158148, 149, 154, 157o1mul2 15514 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) โˆ’ (logโ€˜๐‘ฅ)) ยท (1 / (logโ€˜๐‘ฅ)))) โˆˆ ๐‘‚(1))
159147, 158eqeltrrd 2839 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)) โˆ’ 1)) โˆˆ ๐‘‚(1))
160138, 139, 159o1dif 15519 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1) โ†” (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ 1) โˆˆ ๐‘‚(1)))
161137, 160mpbird 257 . . . . . 6 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
162129, 131, 134, 161o1mul2 15514 . . . . 5 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)))) โˆˆ ๐‘‚(1))
163129, 131remulcld 11192 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ))) โˆˆ โ„)
16421, 4nndivred 12214 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›) โˆˆ โ„)
16592, 164remulcld 11192 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)) โˆˆ โ„)
16697, 165resubcld 11590 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))) โˆˆ โ„)
1676, 166remulcld 11192 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) โˆˆ โ„)
1682, 167fsumrecl 15626 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) โˆˆ โ„)
169168, 24rerpdivcld 12995 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ)) โˆˆ โ„)
170169recnd 11190 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ)) โˆˆ โ„‚)
171168recnd 11190 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) โˆˆ โ„‚)
172171abscld 15328 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โˆˆ โ„)
173129, 130remulcld 11192 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (๐ด ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›)) โˆˆ โ„)
17498, 104subcld 11519 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))) โˆˆ โ„‚)
17596, 174mulcld 11182 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) โˆˆ โ„‚)
176175abscld 15328 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โˆˆ โ„)
1772, 176fsumrecl 15626 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(absโ€˜((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โˆˆ โ„)
178167recnd 11190 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) โˆˆ โ„‚)
1792, 178fsumabs 15693 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โ‰ค ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(absโ€˜((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))))
180129adantr 482 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐ด โˆˆ โ„)
181180, 7remulcld 11192 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (๐ด ยท ((ฮ›โ€˜๐‘›) / ๐‘›)) โˆˆ โ„)
182174abscld 15328 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) โˆˆ โ„)
183180, 4nndivred 12214 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (๐ด / ๐‘›) โˆˆ โ„)
184 vmage0 26486 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ 0 โ‰ค (ฮ›โ€˜๐‘›))
1854, 184syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ 0 โ‰ค (ฮ›โ€˜๐‘›))
186106, 107, 101, 89, 102divdiv2d 11970 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) = ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) ยท ๐‘›) / ๐‘ฅ))
187106, 101, 107, 89div23d 11975 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) ยท ๐‘›) / ๐‘ฅ) = ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) ยท ๐‘›))
188186, 187eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) = ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) ยท ๐‘›))
18999, 103, 101mulassd 11185 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)) ยท ๐‘›) = (2 ยท (((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›) ยท ๐‘›)))
190100, 101, 102divcan1d 11939 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›) ยท ๐‘›) = (logโ€˜(๐‘ฅ / ๐‘›)))
191190oveq2d 7378 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท (((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›) ยท ๐‘›)) = (2 ยท (logโ€˜(๐‘ฅ / ๐‘›))))
192189, 191eqtr2d 2778 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›))) = ((2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)) ยท ๐‘›))
193188, 192oveq12d 7380 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) โˆ’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›)))) = (((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) ยท ๐‘›) โˆ’ ((2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)) ยท ๐‘›)))
19498, 104, 101subdird 11619 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))) ยท ๐‘›) = (((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) ยท ๐‘›) โˆ’ ((2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)) ยท ๐‘›)))
195193, 194eqtr4d 2780 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) โˆ’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›)))) = (((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))) ยท ๐‘›))
196195fveq2d 6851 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) โˆ’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›))))) = (absโ€˜(((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))) ยท ๐‘›)))
197174, 101absmuld 15346 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜(((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))) ยท ๐‘›)) = ((absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) ยท (absโ€˜๐‘›)))
1984nnred 12175 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘› โˆˆ โ„)
19919rpge0d 12968 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ 0 โ‰ค ๐‘›)
200198, 199absidd 15314 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜๐‘›) = ๐‘›)
201200oveq2d 7378 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) ยท (absโ€˜๐‘›)) = ((absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) ยท ๐‘›))
202196, 197, 2013eqtrd 2781 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) โˆ’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›))))) = ((absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) ยท ๐‘›))
203 fveq2 6847 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘– = ๐‘š โ†’ (ฮ›โ€˜๐‘–) = (ฮ›โ€˜๐‘š))
204 fveq2 6847 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘– = ๐‘š โ†’ (logโ€˜๐‘–) = (logโ€˜๐‘š))
205 oveq2 7370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘– = ๐‘š โ†’ (๐‘ฆ / ๐‘–) = (๐‘ฆ / ๐‘š))
206205fveq2d 6851 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘– = ๐‘š โ†’ (ฯˆโ€˜(๐‘ฆ / ๐‘–)) = (ฯˆโ€˜(๐‘ฆ / ๐‘š)))
207204, 206oveq12d 7380 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘– = ๐‘š โ†’ ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–))) = ((logโ€˜๐‘š) + (ฯˆโ€˜(๐‘ฆ / ๐‘š))))
208203, 207oveq12d 7380 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘– = ๐‘š โ†’ ((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) = ((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜(๐‘ฆ / ๐‘š)))))
209208cbvsumv 15588 . . . . . . . . . . . . . . . . . . . . . 22 ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) = ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜(๐‘ฆ / ๐‘š))))
210 fveq2 6847 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ (โŒŠโ€˜๐‘ฆ) = (โŒŠโ€˜(๐‘ฅ / ๐‘›)))
211210oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ (1...(โŒŠโ€˜๐‘ฆ)) = (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›))))
212 fvoveq1 7385 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ (ฯˆโ€˜(๐‘ฆ / ๐‘š)) = (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))
213212oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ ((logโ€˜๐‘š) + (ฯˆโ€˜(๐‘ฆ / ๐‘š))) = ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))
214213oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ ((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜(๐‘ฆ / ๐‘š)))) = ((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))))
215214adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฆ = (๐‘ฅ / ๐‘›) โˆง ๐‘š โˆˆ (1...(โŒŠโ€˜๐‘ฆ))) โ†’ ((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜(๐‘ฆ / ๐‘š)))) = ((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))))
216211, 215sumeq12dv 15598 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜(๐‘ฆ / ๐‘š)))) = ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))))
217209, 216eqtrid 2789 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) = ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))))
218 id 22 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ ๐‘ฆ = (๐‘ฅ / ๐‘›))
219217, 218oveq12d 7380 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ (ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) / ๐‘ฆ) = (ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)))
220 fveq2 6847 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ (logโ€˜๐‘ฆ) = (logโ€˜(๐‘ฅ / ๐‘›)))
221220oveq2d 7378 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ (2 ยท (logโ€˜๐‘ฆ)) = (2 ยท (logโ€˜(๐‘ฅ / ๐‘›))))
222219, 221oveq12d 7380 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ ((ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) / ๐‘ฆ) โˆ’ (2 ยท (logโ€˜๐‘ฆ))) = ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) โˆ’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›)))))
223222fveq2d 6851 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ (absโ€˜((ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) / ๐‘ฆ) โˆ’ (2 ยท (logโ€˜๐‘ฆ)))) = (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) โˆ’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›))))))
224223breq1d 5120 . . . . . . . . . . . . . . . . 17 (๐‘ฆ = (๐‘ฅ / ๐‘›) โ†’ ((absโ€˜((ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) / ๐‘ฆ) โˆ’ (2 ยท (logโ€˜๐‘ฆ)))) โ‰ค ๐ด โ†” (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) โˆ’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›))))) โ‰ค ๐ด))
225 selberg4lem1.2 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ (1[,)+โˆž)(absโ€˜((ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) / ๐‘ฆ) โˆ’ (2 ยท (logโ€˜๐‘ฆ)))) โ‰ค ๐ด)
226225ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ โˆ€๐‘ฆ โˆˆ (1[,)+โˆž)(absโ€˜((ฮฃ๐‘– โˆˆ (1...(โŒŠโ€˜๐‘ฆ))((ฮ›โ€˜๐‘–) ยท ((logโ€˜๐‘–) + (ฯˆโ€˜(๐‘ฆ / ๐‘–)))) / ๐‘ฆ) โˆ’ (2 ยท (logโ€˜๐‘ฆ)))) โ‰ค ๐ด)
227101mulid2d 11180 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (1 ยท ๐‘›) = ๐‘›)
228 fznnfl 13774 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„ โ†’ (๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ)) โ†” (๐‘› โˆˆ โ„• โˆง ๐‘› โ‰ค ๐‘ฅ)))
2299, 228syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ)) โ†” (๐‘› โˆˆ โ„• โˆง ๐‘› โ‰ค ๐‘ฅ)))
230229simplbda 501 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐‘› โ‰ค ๐‘ฅ)
231227, 230eqbrtrd 5132 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (1 ยท ๐‘›) โ‰ค ๐‘ฅ)
232 1red 11163 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ 1 โˆˆ โ„)
233232, 57, 19lemuldivd 13013 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((1 ยท ๐‘›) โ‰ค ๐‘ฅ โ†” 1 โ‰ค (๐‘ฅ / ๐‘›)))
234231, 233mpbid 231 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ 1 โ‰ค (๐‘ฅ / ๐‘›))
235 1re 11162 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ โ„
236 elicopnf 13369 . . . . . . . . . . . . . . . . . . 19 (1 โˆˆ โ„ โ†’ ((๐‘ฅ / ๐‘›) โˆˆ (1[,)+โˆž) โ†” ((๐‘ฅ / ๐‘›) โˆˆ โ„ โˆง 1 โ‰ค (๐‘ฅ / ๐‘›))))
237235, 236ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ / ๐‘›) โˆˆ (1[,)+โˆž) โ†” ((๐‘ฅ / ๐‘›) โˆˆ โ„ โˆง 1 โ‰ค (๐‘ฅ / ๐‘›)))
23858, 234, 237sylanbrc 584 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (๐‘ฅ / ๐‘›) โˆˆ (1[,)+โˆž))
239224, 226, 238rspcdva 3585 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / (๐‘ฅ / ๐‘›)) โˆ’ (2 ยท (logโ€˜(๐‘ฅ / ๐‘›))))) โ‰ค ๐ด)
240202, 239eqbrtrrd 5134 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) ยท ๐‘›) โ‰ค ๐ด)
241182, 180, 19lemuldivd 13013 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (((absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) ยท ๐‘›) โ‰ค ๐ด โ†” (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) โ‰ค (๐ด / ๐‘›)))
242240, 241mpbid 231 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) โ‰ค (๐ด / ๐‘›))
243182, 183, 6, 185, 242lemul2ad 12102 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) ยท (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โ‰ค ((ฮ›โ€˜๐‘›) ยท (๐ด / ๐‘›)))
24496, 174absmuld 15346 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) = ((absโ€˜(ฮ›โ€˜๐‘›)) ยท (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))))
2456, 185absidd 15314 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜(ฮ›โ€˜๐‘›)) = (ฮ›โ€˜๐‘›))
246245oveq1d 7377 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((absโ€˜(ฮ›โ€˜๐‘›)) ยท (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) = ((ฮ›โ€˜๐‘›) ยท (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))))
247244, 246eqtrd 2777 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) = ((ฮ›โ€˜๐‘›) ยท (absโ€˜((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))))
248132ad2antrr 725 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ๐ด โˆˆ โ„‚)
249248, 96, 101, 102div12d 11974 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (๐ด ยท ((ฮ›โ€˜๐‘›) / ๐‘›)) = ((ฮ›โ€˜๐‘›) ยท (๐ด / ๐‘›)))
250243, 247, 2493brtr4d 5142 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ (absโ€˜((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โ‰ค (๐ด ยท ((ฮ›โ€˜๐‘›) / ๐‘›)))
2512, 176, 181, 250fsumle 15691 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(absโ€˜((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โ‰ค ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(๐ด ยท ((ฮ›โ€˜๐‘›) / ๐‘›)))
252132adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ๐ด โˆˆ โ„‚)
2537recnd 11190 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ ((ฮ›โ€˜๐‘›) / ๐‘›) โˆˆ โ„‚)
2542, 252, 253fsummulc2 15676 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (๐ด ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›)) = ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(๐ด ยท ((ฮ›โ€˜๐‘›) / ๐‘›)))
255251, 254breqtrrd 5138 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(absโ€˜((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โ‰ค (๐ด ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›)))
256172, 177, 173, 179, 255letrd 11319 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) โ‰ค (๐ด ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›)))
257172, 173, 24, 256lediv1dd 13022 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) / (logโ€˜๐‘ฅ)) โ‰ค ((๐ด ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›)) / (logโ€˜๐‘ฅ)))
258252, 140, 31, 73divassd 11973 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((๐ด ยท ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›)) / (logโ€˜๐‘ฅ)) = (๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ))))
259257, 258breqtrd 5136 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) / (logโ€˜๐‘ฅ)) โ‰ค (๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ))))
260171, 31, 73absdivd 15347 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ))) = ((absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) / (absโ€˜(logโ€˜๐‘ฅ))))
26124rpge0d 12968 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 0 โ‰ค (logโ€˜๐‘ฅ))
26227, 261absidd 15314 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (absโ€˜(logโ€˜๐‘ฅ)) = (logโ€˜๐‘ฅ))
263262oveq2d 7378 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ ((absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) / (absโ€˜(logโ€˜๐‘ฅ))) = ((absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) / (logโ€˜๐‘ฅ)))
264260, 263eqtrd 2777 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ))) = ((absโ€˜ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›))))) / (logโ€˜๐‘ฅ)))
265128rpge0d 12968 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 0 โ‰ค ๐ด)
2666, 19, 185divge0d 13004 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))) โ†’ 0 โ‰ค ((ฮ›โ€˜๐‘›) / ๐‘›))
2672, 7, 266fsumge0 15687 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 0 โ‰ค ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›))
268130, 24, 267divge0d 13004 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 0 โ‰ค (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)))
269129, 131, 265, 268mulge0d 11739 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ 0 โ‰ค (๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ))))
270163, 269absidd 15314 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (absโ€˜(๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)))) = (๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ))))
271259, 264, 2703brtr4d 5142 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1(,)+โˆž)) โ†’ (absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ))) โ‰ค (absโ€˜(๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)))))
272271adantrr 716 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ โˆˆ (1(,)+โˆž) โˆง 1 โ‰ค ๐‘ฅ)) โ†’ (absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ))) โ‰ค (absโ€˜(๐ด ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) / ๐‘›) / (logโ€˜๐‘ฅ)))))
273126, 162, 163, 170, 272o1le 15544 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ((ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š)))) / ๐‘ฅ) โˆ’ (2 ยท ((logโ€˜(๐‘ฅ / ๐‘›)) / ๐‘›)))) / (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
274125, 273eqeltrd 2838 . . 3 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)) โˆ’ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ)))) โˆˆ ๐‘‚(1))
27571, 76, 274o1dif 15519 . 2 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1) โ†” (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((2 ยท (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))(((ฮ›โ€˜๐‘›) / ๐‘›) ยท (logโ€˜(๐‘ฅ / ๐‘›))) / (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1)))
27649, 275mpbird 257 1 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1(,)+โˆž) โ†ฆ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((ฮ›โ€˜๐‘›) ยท ฮฃ๐‘š โˆˆ (1...(โŒŠโ€˜(๐‘ฅ / ๐‘›)))((ฮ›โ€˜๐‘š) ยท ((logโ€˜๐‘š) + (ฯˆโ€˜((๐‘ฅ / ๐‘›) / ๐‘š))))) / (๐‘ฅ ยท (logโ€˜๐‘ฅ))) โˆ’ (logโ€˜๐‘ฅ))) โˆˆ ๐‘‚(1))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆ€wral 3065   โŠ† wss 3915   class class class wbr 5110   โ†ฆ cmpt 5193  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063  +โˆžcpnf 11193   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392   / cdiv 11819  โ„•cn 12160  2c2 12215  โ„+crp 12922  (,)cioo 13271  [,)cico 13273  ...cfz 13431  โŒŠcfl 13702  abscabs 15126   โ‡๐‘Ÿ crli 15374  ๐‘‚(1)co1 15375  ฮฃcsu 15577  logclog 25926  ฮ›cvma 26457  ฯˆ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 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-xnn0 12493  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-o1 15379  df-lo1 15380  df-sum 15578  df-ef 15957  df-e 15958  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-ulm 25752  df-log 25928  df-cxp 25929  df-atan 26233  df-em 26358  df-cht 26462  df-vma 26463  df-chp 26464  df-ppi 26465
This theorem is referenced by:  selberg4  26925
  Copyright terms: Public domain W3C validator