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

Theorem log2sumbnd 26915
Description: Bound on the difference between ฮฃ๐‘› โ‰ค ๐ด, logโ†‘2(๐‘›) and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016.)
Assertion
Ref Expression
log2sumbnd ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โ‰ค (((logโ€˜๐ด)โ†‘2) + 2))
Distinct variable group:   ๐ด,๐‘›

Proof of Theorem log2sumbnd
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 13887 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (1...(โŒŠโ€˜๐ด)) โˆˆ Fin)
2 elfznn 13479 . . . . . . . . . . . 12 (๐‘› โˆˆ (1...(โŒŠโ€˜๐ด)) โ†’ ๐‘› โˆˆ โ„•)
32adantl 483 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ ๐‘› โˆˆ โ„•)
43nnrpd 12963 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ ๐‘› โˆˆ โ„+)
54relogcld 26001 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
65resqcld 14039 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))) โ†’ ((logโ€˜๐‘›)โ†‘2) โˆˆ โ„)
71, 6fsumrecl 15627 . . . . . . 7 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆˆ โ„)
8 rpre 12931 . . . . . . . . 9 (๐ด โˆˆ โ„+ โ†’ ๐ด โˆˆ โ„)
98adantr 482 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ๐ด โˆˆ โ„)
10 relogcl 25954 . . . . . . . . . . 11 (๐ด โˆˆ โ„+ โ†’ (logโ€˜๐ด) โˆˆ โ„)
1110adantr 482 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (logโ€˜๐ด) โˆˆ โ„)
1211resqcld 14039 . . . . . . . . 9 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ((logโ€˜๐ด)โ†‘2) โˆˆ โ„)
13 2re 12235 . . . . . . . . . 10 2 โˆˆ โ„
14 remulcl 11144 . . . . . . . . . . 11 ((2 โˆˆ โ„ โˆง (logโ€˜๐ด) โˆˆ โ„) โ†’ (2 ยท (logโ€˜๐ด)) โˆˆ โ„)
1513, 11, 14sylancr 588 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (2 ยท (logโ€˜๐ด)) โˆˆ โ„)
16 resubcl 11473 . . . . . . . . . 10 ((2 โˆˆ โ„ โˆง (2 ยท (logโ€˜๐ด)) โˆˆ โ„) โ†’ (2 โˆ’ (2 ยท (logโ€˜๐ด))) โˆˆ โ„)
1713, 15, 16sylancr 588 . . . . . . . . 9 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (2 โˆ’ (2 ยท (logโ€˜๐ด))) โˆˆ โ„)
1812, 17readdcld 11192 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))) โˆˆ โ„)
199, 18remulcld 11193 . . . . . . 7 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))) โˆˆ โ„)
207, 19resubcld 11591 . . . . . 6 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆˆ โ„)
2120recnd 11191 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆˆ โ„‚)
2221abscld 15330 . . . 4 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆˆ โ„)
23 resubcl 11473 . . . 4 (((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆˆ โ„ โˆง 2 โˆˆ โ„) โ†’ ((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ 2) โˆˆ โ„)
2422, 13, 23sylancl 587 . . 3 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ 2) โˆˆ โ„)
25 2cn 12236 . . . . . 6 2 โˆˆ โ„‚
2625negcli 11477 . . . . 5 -2 โˆˆ โ„‚
27 subcl 11408 . . . . 5 (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆˆ โ„‚ โˆง -2 โˆˆ โ„‚) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2) โˆˆ โ„‚)
2821, 26, 27sylancl 587 . . . 4 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2) โˆˆ โ„‚)
2928abscld 15330 . . 3 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (absโ€˜((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2)) โˆˆ โ„)
3025absnegi 15294 . . . . . 6 (absโ€˜-2) = (absโ€˜2)
31 0le2 12263 . . . . . . 7 0 โ‰ค 2
32 absid 15190 . . . . . . 7 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ (absโ€˜2) = 2)
3313, 31, 32mp2an 691 . . . . . 6 (absโ€˜2) = 2
3430, 33eqtri 2761 . . . . 5 (absโ€˜-2) = 2
3534oveq2i 7372 . . . 4 ((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ (absโ€˜-2)) = ((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ 2)
36 abs2dif 15226 . . . . 5 (((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆˆ โ„‚ โˆง -2 โˆˆ โ„‚) โ†’ ((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ (absโ€˜-2)) โ‰ค (absโ€˜((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2)))
3721, 26, 36sylancl 587 . . . 4 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ (absโ€˜-2)) โ‰ค (absโ€˜((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2)))
3835, 37eqbrtrrid 5145 . . 3 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ 2) โ‰ค (absโ€˜((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2)))
39 fveq2 6846 . . . . . . . . . . 11 (๐‘ฅ = ๐ด โ†’ (โŒŠโ€˜๐‘ฅ) = (โŒŠโ€˜๐ด))
4039oveq2d 7377 . . . . . . . . . 10 (๐‘ฅ = ๐ด โ†’ (1...(โŒŠโ€˜๐‘ฅ)) = (1...(โŒŠโ€˜๐ด)))
4140sumeq1d 15594 . . . . . . . . 9 (๐‘ฅ = ๐ด โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) = ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2))
42 id 22 . . . . . . . . . 10 (๐‘ฅ = ๐ด โ†’ ๐‘ฅ = ๐ด)
43 fveq2 6846 . . . . . . . . . . . 12 (๐‘ฅ = ๐ด โ†’ (logโ€˜๐‘ฅ) = (logโ€˜๐ด))
4443oveq1d 7376 . . . . . . . . . . 11 (๐‘ฅ = ๐ด โ†’ ((logโ€˜๐‘ฅ)โ†‘2) = ((logโ€˜๐ด)โ†‘2))
4543oveq2d 7377 . . . . . . . . . . . 12 (๐‘ฅ = ๐ด โ†’ (2 ยท (logโ€˜๐‘ฅ)) = (2 ยท (logโ€˜๐ด)))
4645oveq2d 7377 . . . . . . . . . . 11 (๐‘ฅ = ๐ด โ†’ (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))) = (2 โˆ’ (2 ยท (logโ€˜๐ด))))
4744, 46oveq12d 7379 . . . . . . . . . 10 (๐‘ฅ = ๐ด โ†’ (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))) = (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))
4842, 47oveq12d 7379 . . . . . . . . 9 (๐‘ฅ = ๐ด โ†’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) = (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))
4941, 48oveq12d 7379 . . . . . . . 8 (๐‘ฅ = ๐ด โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))))
50 eqid 2733 . . . . . . . 8 (๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))
51 ovex 7394 . . . . . . . 8 (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))) โˆˆ V
5249, 50, 51fvmpt3i 6957 . . . . . . 7 (๐ด โˆˆ โ„+ โ†’ ((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜๐ด) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))))
5352adantr 482 . . . . . 6 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜๐ด) = (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))))
54 1rp 12927 . . . . . . 7 1 โˆˆ โ„+
55 fveq2 6846 . . . . . . . . . . . . . 14 (๐‘ฅ = 1 โ†’ (โŒŠโ€˜๐‘ฅ) = (โŒŠโ€˜1))
56 1z 12541 . . . . . . . . . . . . . . 15 1 โˆˆ โ„ค
57 flid 13722 . . . . . . . . . . . . . . 15 (1 โˆˆ โ„ค โ†’ (โŒŠโ€˜1) = 1)
5856, 57ax-mp 5 . . . . . . . . . . . . . 14 (โŒŠโ€˜1) = 1
5955, 58eqtrdi 2789 . . . . . . . . . . . . 13 (๐‘ฅ = 1 โ†’ (โŒŠโ€˜๐‘ฅ) = 1)
6059oveq2d 7377 . . . . . . . . . . . 12 (๐‘ฅ = 1 โ†’ (1...(โŒŠโ€˜๐‘ฅ)) = (1...1))
6160sumeq1d 15594 . . . . . . . . . . 11 (๐‘ฅ = 1 โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) = ฮฃ๐‘› โˆˆ (1...1)((logโ€˜๐‘›)โ†‘2))
62 0cn 11155 . . . . . . . . . . . 12 0 โˆˆ โ„‚
63 fveq2 6846 . . . . . . . . . . . . . . 15 (๐‘› = 1 โ†’ (logโ€˜๐‘›) = (logโ€˜1))
64 log1 25964 . . . . . . . . . . . . . . 15 (logโ€˜1) = 0
6563, 64eqtrdi 2789 . . . . . . . . . . . . . 14 (๐‘› = 1 โ†’ (logโ€˜๐‘›) = 0)
6665sq0id 14107 . . . . . . . . . . . . 13 (๐‘› = 1 โ†’ ((logโ€˜๐‘›)โ†‘2) = 0)
6766fsum1 15640 . . . . . . . . . . . 12 ((1 โˆˆ โ„ค โˆง 0 โˆˆ โ„‚) โ†’ ฮฃ๐‘› โˆˆ (1...1)((logโ€˜๐‘›)โ†‘2) = 0)
6856, 62, 67mp2an 691 . . . . . . . . . . 11 ฮฃ๐‘› โˆˆ (1...1)((logโ€˜๐‘›)โ†‘2) = 0
6961, 68eqtrdi 2789 . . . . . . . . . 10 (๐‘ฅ = 1 โ†’ ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) = 0)
70 id 22 . . . . . . . . . . . 12 (๐‘ฅ = 1 โ†’ ๐‘ฅ = 1)
71 fveq2 6846 . . . . . . . . . . . . . . . 16 (๐‘ฅ = 1 โ†’ (logโ€˜๐‘ฅ) = (logโ€˜1))
7271, 64eqtrdi 2789 . . . . . . . . . . . . . . 15 (๐‘ฅ = 1 โ†’ (logโ€˜๐‘ฅ) = 0)
7372sq0id 14107 . . . . . . . . . . . . . 14 (๐‘ฅ = 1 โ†’ ((logโ€˜๐‘ฅ)โ†‘2) = 0)
7472oveq2d 7377 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = 1 โ†’ (2 ยท (logโ€˜๐‘ฅ)) = (2 ยท 0))
75 2t0e0 12330 . . . . . . . . . . . . . . . . 17 (2 ยท 0) = 0
7674, 75eqtrdi 2789 . . . . . . . . . . . . . . . 16 (๐‘ฅ = 1 โ†’ (2 ยท (logโ€˜๐‘ฅ)) = 0)
7776oveq2d 7377 . . . . . . . . . . . . . . 15 (๐‘ฅ = 1 โ†’ (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))) = (2 โˆ’ 0))
7825subid1i 11481 . . . . . . . . . . . . . . 15 (2 โˆ’ 0) = 2
7977, 78eqtrdi 2789 . . . . . . . . . . . . . 14 (๐‘ฅ = 1 โ†’ (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))) = 2)
8073, 79oveq12d 7379 . . . . . . . . . . . . 13 (๐‘ฅ = 1 โ†’ (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))) = (0 + 2))
8125addid2i 11351 . . . . . . . . . . . . 13 (0 + 2) = 2
8280, 81eqtrdi 2789 . . . . . . . . . . . 12 (๐‘ฅ = 1 โ†’ (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))) = 2)
8370, 82oveq12d 7379 . . . . . . . . . . 11 (๐‘ฅ = 1 โ†’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) = (1 ยท 2))
8425mulid2i 11168 . . . . . . . . . . 11 (1 ยท 2) = 2
8583, 84eqtrdi 2789 . . . . . . . . . 10 (๐‘ฅ = 1 โ†’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) = 2)
8669, 85oveq12d 7379 . . . . . . . . 9 (๐‘ฅ = 1 โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))) = (0 โˆ’ 2))
87 df-neg 11396 . . . . . . . . 9 -2 = (0 โˆ’ 2)
8886, 87eqtr4di 2791 . . . . . . . 8 (๐‘ฅ = 1 โ†’ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))) = -2)
8988, 50, 51fvmpt3i 6957 . . . . . . 7 (1 โˆˆ โ„+ โ†’ ((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜1) = -2)
9054, 89mp1i 13 . . . . . 6 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜1) = -2)
9153, 90oveq12d 7379 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜๐ด) โˆ’ ((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜1)) = ((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2))
9291fveq2d 6850 . . . 4 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (absโ€˜(((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜๐ด) โˆ’ ((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜1))) = (absโ€˜((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2)))
93 ioorp 13351 . . . . . 6 (0(,)+โˆž) = โ„+
9493eqcomi 2742 . . . . 5 โ„+ = (0(,)+โˆž)
95 nnuz 12814 . . . . 5 โ„• = (โ„คโ‰ฅโ€˜1)
9656a1i 11 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 1 โˆˆ โ„ค)
97 1red 11164 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 1 โˆˆ โ„)
98 pnfxr 11217 . . . . . 6 +โˆž โˆˆ โ„*
9998a1i 11 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ +โˆž โˆˆ โ„*)
100 1re 11163 . . . . . . 7 1 โˆˆ โ„
101 1nn0 12437 . . . . . . 7 1 โˆˆ โ„•0
102100, 101nn0addge1i 12469 . . . . . 6 1 โ‰ค (1 + 1)
103102a1i 11 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 1 โ‰ค (1 + 1))
104 0red 11166 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 0 โˆˆ โ„)
105 rpre 12931 . . . . . . 7 (๐‘ฅ โˆˆ โ„+ โ†’ ๐‘ฅ โˆˆ โ„)
106105adantl 483 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ๐‘ฅ โˆˆ โ„)
107 simpr 486 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ๐‘ฅ โˆˆ โ„+)
108107relogcld 26001 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (logโ€˜๐‘ฅ) โˆˆ โ„)
109108resqcld 14039 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((logโ€˜๐‘ฅ)โ†‘2) โˆˆ โ„)
110 remulcl 11144 . . . . . . . . 9 ((2 โˆˆ โ„ โˆง (logโ€˜๐‘ฅ) โˆˆ โ„) โ†’ (2 ยท (logโ€˜๐‘ฅ)) โˆˆ โ„)
11113, 108, 110sylancr 588 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (2 ยท (logโ€˜๐‘ฅ)) โˆˆ โ„)
112 resubcl 11473 . . . . . . . 8 ((2 โˆˆ โ„ โˆง (2 ยท (logโ€˜๐‘ฅ)) โˆˆ โ„) โ†’ (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))) โˆˆ โ„)
11313, 111, 112sylancr 588 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))) โˆˆ โ„)
114109, 113readdcld 11192 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))) โˆˆ โ„)
115106, 114remulcld 11193 . . . . 5 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) โˆˆ โ„)
116 nnrp 12934 . . . . . 6 (๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„+)
117116, 109sylan2 594 . . . . 5 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„•) โ†’ ((logโ€˜๐‘ฅ)โ†‘2) โˆˆ โ„)
118 reelprrecn 11151 . . . . . . . 8 โ„ โˆˆ {โ„, โ„‚}
119118a1i 11 . . . . . . 7 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ โ„ โˆˆ {โ„, โ„‚})
120106recnd 11191 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ๐‘ฅ โˆˆ โ„‚)
121 1red 11164 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ 1 โˆˆ โ„)
122 recn 11149 . . . . . . . . 9 (๐‘ฅ โˆˆ โ„ โ†’ ๐‘ฅ โˆˆ โ„‚)
123122adantl 483 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„) โ†’ ๐‘ฅ โˆˆ โ„‚)
124 1red 11164 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„) โ†’ 1 โˆˆ โ„)
125119dvmptid 25344 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„ โ†ฆ ๐‘ฅ)) = (๐‘ฅ โˆˆ โ„ โ†ฆ 1))
126 rpssre 12930 . . . . . . . . 9 โ„+ โŠ† โ„
127126a1i 11 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ โ„+ โŠ† โ„)
128 eqid 2733 . . . . . . . . 9 (TopOpenโ€˜โ„‚fld) = (TopOpenโ€˜โ„‚fld)
129128tgioo2 24189 . . . . . . . 8 (topGenโ€˜ran (,)) = ((TopOpenโ€˜โ„‚fld) โ†พt โ„)
130 iooretop 24152 . . . . . . . . . 10 (0(,)+โˆž) โˆˆ (topGenโ€˜ran (,))
13193, 130eqeltrri 2831 . . . . . . . . 9 โ„+ โˆˆ (topGenโ€˜ran (,))
132131a1i 11 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ โ„+ โˆˆ (topGenโ€˜ran (,)))
133119, 123, 124, 125, 127, 129, 128, 132dvmptres 25350 . . . . . . 7 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ ๐‘ฅ)) = (๐‘ฅ โˆˆ โ„+ โ†ฆ 1))
134114recnd 11191 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))) โˆˆ โ„‚)
135 resubcl 11473 . . . . . . . . 9 (((2 ยท (logโ€˜๐‘ฅ)) โˆˆ โ„ โˆง 2 โˆˆ โ„) โ†’ ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) โˆˆ โ„)
136111, 13, 135sylancl 587 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) โˆˆ โ„)
137136, 107rerpdivcld 12996 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ) โˆˆ โ„)
138109recnd 11191 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((logโ€˜๐‘ฅ)โ†‘2) โˆˆ โ„‚)
139111recnd 11191 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (2 ยท (logโ€˜๐‘ฅ)) โˆˆ โ„‚)
140107rpreccld 12975 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (1 / ๐‘ฅ) โˆˆ โ„+)
141140rpcnd 12967 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (1 / ๐‘ฅ) โˆˆ โ„‚)
142139, 141mulcld 11183 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) โˆˆ โ„‚)
143 cnelprrecn 11152 . . . . . . . . . . 11 โ„‚ โˆˆ {โ„, โ„‚}
144143a1i 11 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ โ„‚ โˆˆ {โ„, โ„‚})
145108recnd 11191 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (logโ€˜๐‘ฅ) โˆˆ โ„‚)
146 sqcl 14032 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„‚ โ†’ (๐‘ฆโ†‘2) โˆˆ โ„‚)
147146adantl 483 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘ฆโ†‘2) โˆˆ โ„‚)
148 simpr 486 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ๐‘ฆ โˆˆ โ„‚)
149 mulcl 11143 . . . . . . . . . . 11 ((2 โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„‚)
15025, 148, 149sylancr 588 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„‚)
151 relogf1o 25945 . . . . . . . . . . . . . . 15 (log โ†พ โ„+):โ„+โ€“1-1-ontoโ†’โ„
152 f1of 6788 . . . . . . . . . . . . . . 15 ((log โ†พ โ„+):โ„+โ€“1-1-ontoโ†’โ„ โ†’ (log โ†พ โ„+):โ„+โŸถโ„)
153151, 152mp1i 13 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (log โ†พ โ„+):โ„+โŸถโ„)
154153feqmptd 6914 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (log โ†พ โ„+) = (๐‘ฅ โˆˆ โ„+ โ†ฆ ((log โ†พ โ„+)โ€˜๐‘ฅ)))
155 fvres 6865 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ โ„+ โ†’ ((log โ†พ โ„+)โ€˜๐‘ฅ) = (logโ€˜๐‘ฅ))
156155mpteq2ia 5212 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ โ„+ โ†ฆ ((log โ†พ โ„+)โ€˜๐‘ฅ)) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (logโ€˜๐‘ฅ))
157154, 156eqtrdi 2789 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (log โ†พ โ„+) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (logโ€˜๐‘ฅ)))
158157oveq2d 7377 . . . . . . . . . . 11 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (log โ†พ โ„+)) = (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ (logโ€˜๐‘ฅ))))
159 dvrelog 26015 . . . . . . . . . . 11 (โ„ D (log โ†พ โ„+)) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (1 / ๐‘ฅ))
160158, 159eqtr3di 2788 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ (logโ€˜๐‘ฅ))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (1 / ๐‘ฅ)))
161 2nn 12234 . . . . . . . . . . . 12 2 โˆˆ โ„•
162 dvexp 25340 . . . . . . . . . . . 12 (2 โˆˆ โ„• โ†’ (โ„‚ D (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘2))) = (๐‘ฆ โˆˆ โ„‚ โ†ฆ (2 ยท (๐‘ฆโ†‘(2 โˆ’ 1)))))
163161, 162mp1i 13 . . . . . . . . . . 11 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„‚ D (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘2))) = (๐‘ฆ โˆˆ โ„‚ โ†ฆ (2 ยท (๐‘ฆโ†‘(2 โˆ’ 1)))))
164 2m1e1 12287 . . . . . . . . . . . . . . 15 (2 โˆ’ 1) = 1
165164oveq2i 7372 . . . . . . . . . . . . . 14 (๐‘ฆโ†‘(2 โˆ’ 1)) = (๐‘ฆโ†‘1)
166 exp1 13982 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„‚ โ†’ (๐‘ฆโ†‘1) = ๐‘ฆ)
167165, 166eqtrid 2785 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„‚ โ†’ (๐‘ฆโ†‘(2 โˆ’ 1)) = ๐‘ฆ)
168167oveq2d 7377 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„‚ โ†’ (2 ยท (๐‘ฆโ†‘(2 โˆ’ 1))) = (2 ยท ๐‘ฆ))
169168mpteq2ia 5212 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„‚ โ†ฆ (2 ยท (๐‘ฆโ†‘(2 โˆ’ 1)))) = (๐‘ฆ โˆˆ โ„‚ โ†ฆ (2 ยท ๐‘ฆ))
170163, 169eqtrdi 2789 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„‚ D (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘2))) = (๐‘ฆ โˆˆ โ„‚ โ†ฆ (2 ยท ๐‘ฆ)))
171 oveq1 7368 . . . . . . . . . 10 (๐‘ฆ = (logโ€˜๐‘ฅ) โ†’ (๐‘ฆโ†‘2) = ((logโ€˜๐‘ฅ)โ†‘2))
172 oveq2 7369 . . . . . . . . . 10 (๐‘ฆ = (logโ€˜๐‘ฅ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท (logโ€˜๐‘ฅ)))
173119, 144, 145, 140, 147, 150, 160, 170, 171, 172dvmptco 25359 . . . . . . . . 9 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ ((logโ€˜๐‘ฅ)โ†‘2))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ ((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ))))
174113recnd 11191 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))) โˆˆ โ„‚)
175 ovexd 7396 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (0 โˆ’ (2 ยท (1 / ๐‘ฅ))) โˆˆ V)
176 2cnd 12239 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ 2 โˆˆ โ„‚)
177 0red 11166 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ 0 โˆˆ โ„)
178 2cnd 12239 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„) โ†’ 2 โˆˆ โ„‚)
179 0red 11166 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„) โ†’ 0 โˆˆ โ„)
180 2cnd 12239 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 2 โˆˆ โ„‚)
181119, 180dvmptc 25345 . . . . . . . . . . 11 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„ โ†ฆ 2)) = (๐‘ฅ โˆˆ โ„ โ†ฆ 0))
182119, 178, 179, 181, 127, 129, 128, 132dvmptres 25350 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ 2)) = (๐‘ฅ โˆˆ โ„+ โ†ฆ 0))
183 mulcl 11143 . . . . . . . . . . 11 ((2 โˆˆ โ„‚ โˆง (1 / ๐‘ฅ) โˆˆ โ„‚) โ†’ (2 ยท (1 / ๐‘ฅ)) โˆˆ โ„‚)
18425, 141, 183sylancr 588 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (2 ยท (1 / ๐‘ฅ)) โˆˆ โ„‚)
185119, 145, 140, 160, 180dvmptcmul 25351 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ (2 ยท (logโ€˜๐‘ฅ)))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (2 ยท (1 / ๐‘ฅ))))
186119, 176, 177, 182, 139, 184, 185dvmptsub 25354 . . . . . . . . 9 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (0 โˆ’ (2 ยท (1 / ๐‘ฅ)))))
187119, 138, 142, 173, 174, 175, 186dvmptadd 25347 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) + (0 โˆ’ (2 ยท (1 / ๐‘ฅ))))))
188139, 176, 141subdird 11620 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) ยท (1 / ๐‘ฅ)) = (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) โˆ’ (2 ยท (1 / ๐‘ฅ))))
189136recnd 11191 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) โˆˆ โ„‚)
190 rpne0 12939 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ โ„+ โ†’ ๐‘ฅ โ‰  0)
191190adantl 483 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ๐‘ฅ โ‰  0)
192189, 120, 191divrecd 11942 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ) = (((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) ยท (1 / ๐‘ฅ)))
193 df-neg 11396 . . . . . . . . . . . 12 -(2 ยท (1 / ๐‘ฅ)) = (0 โˆ’ (2 ยท (1 / ๐‘ฅ)))
194193oveq2i 7372 . . . . . . . . . . 11 (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) + -(2 ยท (1 / ๐‘ฅ))) = (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) + (0 โˆ’ (2 ยท (1 / ๐‘ฅ))))
195142, 184negsubd 11526 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) + -(2 ยท (1 / ๐‘ฅ))) = (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) โˆ’ (2 ยท (1 / ๐‘ฅ))))
196194, 195eqtr3id 2787 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) + (0 โˆ’ (2 ยท (1 / ๐‘ฅ)))) = (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) โˆ’ (2 ยท (1 / ๐‘ฅ))))
197188, 192, 1963eqtr4rd 2784 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) + (0 โˆ’ (2 ยท (1 / ๐‘ฅ)))) = (((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ))
198197mpteq2dva 5209 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (๐‘ฅ โˆˆ โ„+ โ†ฆ (((2 ยท (logโ€˜๐‘ฅ)) ยท (1 / ๐‘ฅ)) + (0 โˆ’ (2 ยท (1 / ๐‘ฅ))))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ)))
199187, 198eqtrd 2773 . . . . . . 7 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ (((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ)))
200119, 120, 121, 133, 134, 137, 199dvmptmul 25348 . . . . . 6 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ ((1 ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) + ((((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ) ยท ๐‘ฅ))))
201134mulid2d 11181 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (1 ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) = (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))
202138, 139, 176subsub2d 11549 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (((logโ€˜๐‘ฅ)โ†‘2) โˆ’ ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2)) = (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))
203201, 202eqtr4d 2776 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (1 ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) = (((logโ€˜๐‘ฅ)โ†‘2) โˆ’ ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2)))
204189, 120, 191divcan1d 11940 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ) ยท ๐‘ฅ) = ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2))
205203, 204oveq12d 7379 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((1 ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) + ((((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ) ยท ๐‘ฅ)) = ((((logโ€˜๐‘ฅ)โ†‘2) โˆ’ ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2)) + ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2)))
206138, 189npcand 11524 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((((logโ€˜๐‘ฅ)โ†‘2) โˆ’ ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2)) + ((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2)) = ((logโ€˜๐‘ฅ)โ†‘2))
207205, 206eqtrd 2773 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง ๐‘ฅ โˆˆ โ„+) โ†’ ((1 ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) + ((((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ) ยท ๐‘ฅ)) = ((logโ€˜๐‘ฅ)โ†‘2))
208207mpteq2dva 5209 . . . . . 6 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (๐‘ฅ โˆˆ โ„+ โ†ฆ ((1 ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))) + ((((2 ยท (logโ€˜๐‘ฅ)) โˆ’ 2) / ๐‘ฅ) ยท ๐‘ฅ))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ ((logโ€˜๐‘ฅ)โ†‘2)))
209200, 208eqtrd 2773 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (โ„ D (๐‘ฅ โˆˆ โ„+ โ†ฆ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ))))))) = (๐‘ฅ โˆˆ โ„+ โ†ฆ ((logโ€˜๐‘ฅ)โ†‘2)))
210 fveq2 6846 . . . . . 6 (๐‘ฅ = ๐‘› โ†’ (logโ€˜๐‘ฅ) = (logโ€˜๐‘›))
211210oveq1d 7376 . . . . 5 (๐‘ฅ = ๐‘› โ†’ ((logโ€˜๐‘ฅ)โ†‘2) = ((logโ€˜๐‘›)โ†‘2))
212 simp32 1211 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ ๐‘ฅ โ‰ค ๐‘›)
213 simp2l 1200 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ ๐‘ฅ โˆˆ โ„+)
214 simp2r 1201 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ ๐‘› โˆˆ โ„+)
215213, 214logled 26005 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ (๐‘ฅ โ‰ค ๐‘› โ†” (logโ€˜๐‘ฅ) โ‰ค (logโ€˜๐‘›)))
216212, 215mpbid 231 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ (logโ€˜๐‘ฅ) โ‰ค (logโ€˜๐‘›))
217213relogcld 26001 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ (logโ€˜๐‘ฅ) โˆˆ โ„)
218214relogcld 26001 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
219 simp31 1210 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ 1 โ‰ค ๐‘ฅ)
220 logleb 25981 . . . . . . . . . 10 ((1 โˆˆ โ„+ โˆง ๐‘ฅ โˆˆ โ„+) โ†’ (1 โ‰ค ๐‘ฅ โ†” (logโ€˜1) โ‰ค (logโ€˜๐‘ฅ)))
22154, 213, 220sylancr 588 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ (1 โ‰ค ๐‘ฅ โ†” (logโ€˜1) โ‰ค (logโ€˜๐‘ฅ)))
222219, 221mpbid 231 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ (logโ€˜1) โ‰ค (logโ€˜๐‘ฅ))
22364, 222eqbrtrrid 5145 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ 0 โ‰ค (logโ€˜๐‘ฅ))
224214rpred 12965 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ ๐‘› โˆˆ โ„)
225 1red 11164 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ 1 โˆˆ โ„)
226213rpred 12965 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ ๐‘ฅ โˆˆ โ„)
227225, 226, 224, 219, 212letrd 11320 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ 1 โ‰ค ๐‘›)
228224, 227logge0d 26008 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ 0 โ‰ค (logโ€˜๐‘›))
229217, 218, 223, 228le2sqd 14169 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ ((logโ€˜๐‘ฅ) โ‰ค (logโ€˜๐‘›) โ†” ((logโ€˜๐‘ฅ)โ†‘2) โ‰ค ((logโ€˜๐‘›)โ†‘2)))
230216, 229mpbid 231 . . . . 5 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง ๐‘› โˆˆ โ„+) โˆง (1 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘› โˆง ๐‘› โ‰ค +โˆž)) โ†’ ((logโ€˜๐‘ฅ)โ†‘2) โ‰ค ((logโ€˜๐‘›)โ†‘2))
231 relogcl 25954 . . . . . . 7 (๐‘ฅ โˆˆ โ„+ โ†’ (logโ€˜๐‘ฅ) โˆˆ โ„)
232231ad2antrl 727 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง 1 โ‰ค ๐‘ฅ)) โ†’ (logโ€˜๐‘ฅ) โˆˆ โ„)
233232sqge0d 14051 . . . . 5 (((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โˆง (๐‘ฅ โˆˆ โ„+ โˆง 1 โ‰ค ๐‘ฅ)) โ†’ 0 โ‰ค ((logโ€˜๐‘ฅ)โ†‘2))
23454a1i 11 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 1 โˆˆ โ„+)
235 simpl 484 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ๐ด โˆˆ โ„+)
236 1le1 11791 . . . . . 6 1 โ‰ค 1
237236a1i 11 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 1 โ‰ค 1)
238 simpr 486 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 1 โ‰ค ๐ด)
2399rexrd 11213 . . . . . 6 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ๐ด โˆˆ โ„*)
240 pnfge 13059 . . . . . 6 (๐ด โˆˆ โ„* โ†’ ๐ด โ‰ค +โˆž)
241239, 240syl 17 . . . . 5 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ๐ด โ‰ค +โˆž)
24294, 95, 96, 97, 99, 103, 104, 115, 109, 117, 209, 211, 230, 50, 233, 234, 235, 237, 238, 241, 44dvfsum2 25421 . . . 4 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (absโ€˜(((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜๐ด) โˆ’ ((๐‘ฅ โˆˆ โ„+ โ†ฆ (ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐‘ฅ))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐‘ฅ ยท (((logโ€˜๐‘ฅ)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐‘ฅ)))))))โ€˜1))) โ‰ค ((logโ€˜๐ด)โ†‘2))
24392, 242eqbrtrrd 5133 . . 3 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (absโ€˜((ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด)))))) โˆ’ -2)) โ‰ค ((logโ€˜๐ด)โ†‘2))
24424, 29, 12, 38, 243letrd 11320 . 2 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ ((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ 2) โ‰ค ((logโ€˜๐ด)โ†‘2))
24513a1i 11 . . 3 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ 2 โˆˆ โ„)
24622, 245, 12lesubaddd 11760 . 2 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (((absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โˆ’ 2) โ‰ค ((logโ€˜๐ด)โ†‘2) โ†” (absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โ‰ค (((logโ€˜๐ด)โ†‘2) + 2)))
247244, 246mpbid 231 1 ((๐ด โˆˆ โ„+ โˆง 1 โ‰ค ๐ด) โ†’ (absโ€˜(ฮฃ๐‘› โˆˆ (1...(โŒŠโ€˜๐ด))((logโ€˜๐‘›)โ†‘2) โˆ’ (๐ด ยท (((logโ€˜๐ด)โ†‘2) + (2 โˆ’ (2 ยท (logโ€˜๐ด))))))) โ‰ค (((logโ€˜๐ด)โ†‘2) + 2))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  Vcvv 3447   โŠ† wss 3914  {cpr 4592   class class class wbr 5109   โ†ฆ cmpt 5192  ran crn 5638   โ†พ cres 5639  โŸถwf 6496  โ€“1-1-ontoโ†’wf1o 6499  โ€˜cfv 6500  (class class class)co 7361  โ„‚cc 11057  โ„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   ยท cmul 11064  +โˆžcpnf 11194  โ„*cxr 11196   โ‰ค cle 11198   โˆ’ cmin 11393  -cneg 11394   / cdiv 11820  โ„•cn 12161  2c2 12216  โ„คcz 12507  โ„+crp 12923  (,)cioo 13273  ...cfz 13433  โŒŠcfl 13704  โ†‘cexp 13976  abscabs 15128  ฮฃcsu 15579  TopOpenctopn 17311  topGenctg 17327  โ„‚fldccnfld 20819   D cdv 25250  logclog 25933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137  ax-addf 11138  ax-mulf 11139
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7621  df-om 7807  df-1st 7925  df-2nd 7926  df-supp 8097  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-er 8654  df-map 8773  df-pm 8774  df-ixp 8842  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fsupp 9312  df-fi 9355  df-sup 9386  df-inf 9387  df-oi 9454  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-4 12226  df-5 12227  df-6 12228  df-7 12229  df-8 12230  df-9 12231  df-n0 12422  df-z 12508  df-dec 12627  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-ioo 13277  df-ioc 13278  df-ico 13279  df-icc 13280  df-fz 13434  df-fzo 13577  df-fl 13706  df-mod 13784  df-seq 13916  df-exp 13977  df-fac 14183  df-bc 14212  df-hash 14240  df-shft 14961  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-limsup 15362  df-clim 15379  df-rlim 15380  df-sum 15580  df-ef 15958  df-sin 15960  df-cos 15961  df-pi 15963  df-struct 17027  df-sets 17044  df-slot 17062  df-ndx 17074  df-base 17092  df-ress 17121  df-plusg 17154  df-mulr 17155  df-starv 17156  df-sca 17157  df-vsca 17158  df-ip 17159  df-tset 17160  df-ple 17161  df-ds 17163  df-unif 17164  df-hom 17165  df-cco 17166  df-rest 17312  df-topn 17313  df-0g 17331  df-gsum 17332  df-topgen 17333  df-pt 17334  df-prds 17337  df-xrs 17392  df-qtop 17397  df-imas 17398  df-xps 17400  df-mre 17474  df-mrc 17475  df-acs 17477  df-mgm 18505  df-sgrp 18554  df-mnd 18565  df-submnd 18610  df-mulg 18881  df-cntz 19105  df-cmn 19572  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-fbas 20816  df-fg 20817  df-cnfld 20820  df-top 22266  df-topon 22283  df-topsp 22305  df-bases 22319  df-cld 22393  df-ntr 22394  df-cls 22395  df-nei 22472  df-lp 22510  df-perf 22511  df-cn 22601  df-cnp 22602  df-haus 22689  df-cmp 22761  df-tx 22936  df-hmeo 23129  df-fil 23220  df-fm 23312  df-flim 23313  df-flf 23314  df-xms 23696  df-ms 23697  df-tms 23698  df-cncf 24264  df-limc 25253  df-dv 25254  df-log 25935
This theorem is referenced by:  selberglem2  26917
  Copyright terms: Public domain W3C validator