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

Theorem rplogsumlem1 26987
Description: Lemma for rplogsum 27030. (Contributed by Mario Carneiro, 2-May-2016.)
Assertion
Ref Expression
rplogsumlem1 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((logโ€˜๐‘›) / (๐‘› ยท (๐‘› โˆ’ 1))) โ‰ค 2)
Distinct variable group:   ๐ด,๐‘›

Proof of Theorem rplogsumlem1
Dummy variable ๐‘˜ is distinct from all other variables.
StepHypRef Expression
1 fzfid 13938 . . 3 (๐ด โˆˆ โ„• โ†’ (2...๐ด) โˆˆ Fin)
2 elfzuz 13497 . . . . . . . 8 (๐‘› โˆˆ (2...๐ด) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜2))
3 eluz2nn 12868 . . . . . . . 8 (๐‘› โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘› โˆˆ โ„•)
42, 3syl 17 . . . . . . 7 (๐‘› โˆˆ (2...๐ด) โ†’ ๐‘› โˆˆ โ„•)
54adantl 483 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ๐‘› โˆˆ โ„•)
65nnrpd 13014 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ๐‘› โˆˆ โ„+)
76relogcld 26131 . . . 4 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (logโ€˜๐‘›) โˆˆ โ„)
82adantl 483 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜2))
9 uz2m1nn 12907 . . . . . 6 (๐‘› โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„•)
108, 9syl 17 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„•)
115, 10nnmulcld 12265 . . . 4 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› ยท (๐‘› โˆ’ 1)) โˆˆ โ„•)
127, 11nndivred 12266 . . 3 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((logโ€˜๐‘›) / (๐‘› ยท (๐‘› โˆ’ 1))) โˆˆ โ„)
131, 12fsumrecl 15680 . 2 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((logโ€˜๐‘›) / (๐‘› ยท (๐‘› โˆ’ 1))) โˆˆ โ„)
14 2re 12286 . . . . 5 2 โˆˆ โ„
1510nnrpd 13014 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„+)
1615rpsqrtcld 15358 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜(๐‘› โˆ’ 1)) โˆˆ โ„+)
17 rerpdivcl 13004 . . . . 5 ((2 โˆˆ โ„ โˆง (โˆšโ€˜(๐‘› โˆ’ 1)) โˆˆ โ„+) โ†’ (2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆˆ โ„)
1814, 16, 17sylancr 588 . . . 4 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆˆ โ„)
196rpsqrtcld 15358 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜๐‘›) โˆˆ โ„+)
20 rerpdivcl 13004 . . . . 5 ((2 โˆˆ โ„ โˆง (โˆšโ€˜๐‘›) โˆˆ โ„+) โ†’ (2 / (โˆšโ€˜๐‘›)) โˆˆ โ„)
2114, 19, 20sylancr 588 . . . 4 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (2 / (โˆšโ€˜๐‘›)) โˆˆ โ„)
2218, 21resubcld 11642 . . 3 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) โˆˆ โ„)
231, 22fsumrecl 15680 . 2 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) โˆˆ โ„)
2414a1i 11 . 2 (๐ด โˆˆ โ„• โ†’ 2 โˆˆ โ„)
2516rpred 13016 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜(๐‘› โˆ’ 1)) โˆˆ โ„)
265nnred 12227 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ๐‘› โˆˆ โ„)
27 peano2rem 11527 . . . . . . . 8 (๐‘› โˆˆ โ„ โ†’ (๐‘› โˆ’ 1) โˆˆ โ„)
2826, 27syl 17 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„)
2926, 28remulcld 11244 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› ยท (๐‘› โˆ’ 1)) โˆˆ โ„)
3029, 22remulcld 11244 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((๐‘› ยท (๐‘› โˆ’ 1)) ยท ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›)))) โˆˆ โ„)
315nncnd 12228 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ๐‘› โˆˆ โ„‚)
32 ax-1cn 11168 . . . . . . . 8 1 โˆˆ โ„‚
33 npcan 11469 . . . . . . . 8 ((๐‘› โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘› โˆ’ 1) + 1) = ๐‘›)
3431, 32, 33sylancl 587 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((๐‘› โˆ’ 1) + 1) = ๐‘›)
3534fveq2d 6896 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (logโ€˜((๐‘› โˆ’ 1) + 1)) = (logโ€˜๐‘›))
3615rpge0d 13020 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ 0 โ‰ค (๐‘› โˆ’ 1))
37 loglesqrt 26266 . . . . . . 7 (((๐‘› โˆ’ 1) โˆˆ โ„ โˆง 0 โ‰ค (๐‘› โˆ’ 1)) โ†’ (logโ€˜((๐‘› โˆ’ 1) + 1)) โ‰ค (โˆšโ€˜(๐‘› โˆ’ 1)))
3828, 36, 37syl2anc 585 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (logโ€˜((๐‘› โˆ’ 1) + 1)) โ‰ค (โˆšโ€˜(๐‘› โˆ’ 1)))
3935, 38eqbrtrrd 5173 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (logโ€˜๐‘›) โ‰ค (โˆšโ€˜(๐‘› โˆ’ 1)))
4019rpred 13016 . . . . . . . . . . 11 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜๐‘›) โˆˆ โ„)
4140, 25readdcld 11243 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) + (โˆšโ€˜(๐‘› โˆ’ 1))) โˆˆ โ„)
42 remulcl 11195 . . . . . . . . . . 11 (((โˆšโ€˜๐‘›) โˆˆ โ„ โˆง 2 โˆˆ โ„) โ†’ ((โˆšโ€˜๐‘›) ยท 2) โˆˆ โ„)
4340, 14, 42sylancl 587 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) ยท 2) โˆˆ โ„)
4440, 25resubcld 11642 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))) โˆˆ โ„)
4526lem1d 12147 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› โˆ’ 1) โ‰ค ๐‘›)
466rpge0d 13020 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ 0 โ‰ค ๐‘›)
4728, 36, 26, 46sqrtled 15373 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((๐‘› โˆ’ 1) โ‰ค ๐‘› โ†” (โˆšโ€˜(๐‘› โˆ’ 1)) โ‰ค (โˆšโ€˜๐‘›)))
4845, 47mpbid 231 . . . . . . . . . . 11 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜(๐‘› โˆ’ 1)) โ‰ค (โˆšโ€˜๐‘›))
4940, 25subge0d 11804 . . . . . . . . . . 11 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (0 โ‰ค ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))) โ†” (โˆšโ€˜(๐‘› โˆ’ 1)) โ‰ค (โˆšโ€˜๐‘›)))
5048, 49mpbird 257 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ 0 โ‰ค ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))
5125, 40, 40, 48leadd2dd 11829 . . . . . . . . . . 11 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) + (โˆšโ€˜(๐‘› โˆ’ 1))) โ‰ค ((โˆšโ€˜๐‘›) + (โˆšโ€˜๐‘›)))
5219rpcnd 13018 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜๐‘›) โˆˆ โ„‚)
5352times2d 12456 . . . . . . . . . . 11 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) ยท 2) = ((โˆšโ€˜๐‘›) + (โˆšโ€˜๐‘›)))
5451, 53breqtrrd 5177 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) + (โˆšโ€˜(๐‘› โˆ’ 1))) โ‰ค ((โˆšโ€˜๐‘›) ยท 2))
5541, 43, 44, 50, 54lemul1ad 12153 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›) + (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) โ‰ค (((โˆšโ€˜๐‘›) ยท 2) ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))))
5631sqsqrtd 15386 . . . . . . . . . . 11 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›)โ†‘2) = ๐‘›)
57 subcl 11459 . . . . . . . . . . . . 13 ((๐‘› โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„‚)
5831, 32, 57sylancl 587 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› โˆ’ 1) โˆˆ โ„‚)
5958sqsqrtd 15386 . . . . . . . . . . 11 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜(๐‘› โˆ’ 1))โ†‘2) = (๐‘› โˆ’ 1))
6056, 59oveq12d 7427 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›)โ†‘2) โˆ’ ((โˆšโ€˜(๐‘› โˆ’ 1))โ†‘2)) = (๐‘› โˆ’ (๐‘› โˆ’ 1)))
6116rpcnd 13018 . . . . . . . . . . 11 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜(๐‘› โˆ’ 1)) โˆˆ โ„‚)
62 subsq 14174 . . . . . . . . . . 11 (((โˆšโ€˜๐‘›) โˆˆ โ„‚ โˆง (โˆšโ€˜(๐‘› โˆ’ 1)) โˆˆ โ„‚) โ†’ (((โˆšโ€˜๐‘›)โ†‘2) โˆ’ ((โˆšโ€˜(๐‘› โˆ’ 1))โ†‘2)) = (((โˆšโ€˜๐‘›) + (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))))
6352, 61, 62syl2anc 585 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›)โ†‘2) โˆ’ ((โˆšโ€˜(๐‘› โˆ’ 1))โ†‘2)) = (((โˆšโ€˜๐‘›) + (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))))
64 nncan 11489 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (๐‘› โˆ’ (๐‘› โˆ’ 1)) = 1)
6531, 32, 64sylancl 587 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› โˆ’ (๐‘› โˆ’ 1)) = 1)
6660, 63, 653eqtr3d 2781 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›) + (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) = 1)
67 2cn 12287 . . . . . . . . . . 11 2 โˆˆ โ„‚
6867a1i 11 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ 2 โˆˆ โ„‚)
6944recnd 11242 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))) โˆˆ โ„‚)
7052, 68, 69mulassd 11237 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›) ยท 2) ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) = ((โˆšโ€˜๐‘›) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))))
7155, 66, 703brtr3d 5180 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ 1 โ‰ค ((โˆšโ€˜๐‘›) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))))
72 1red 11215 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ 1 โˆˆ โ„)
73 remulcl 11195 . . . . . . . . . . 11 ((2 โˆˆ โ„ โˆง ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))) โˆˆ โ„) โ†’ (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) โˆˆ โ„)
7414, 44, 73sylancr 588 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) โˆˆ โ„)
7540, 74remulcld 11244 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))) โˆˆ โ„)
7672, 75, 16lemul1d 13059 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (1 โ‰ค ((โˆšโ€˜๐‘›) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))) โ†” (1 ยท (โˆšโ€˜(๐‘› โˆ’ 1))) โ‰ค (((โˆšโ€˜๐‘›) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))))
7771, 76mpbid 231 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (1 ยท (โˆšโ€˜(๐‘› โˆ’ 1))) โ‰ค (((โˆšโ€˜๐‘›) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))) ยท (โˆšโ€˜(๐‘› โˆ’ 1))))
7861mullidd 11232 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (1 ยท (โˆšโ€˜(๐‘› โˆ’ 1))) = (โˆšโ€˜(๐‘› โˆ’ 1)))
7974recnd 11242 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) โˆˆ โ„‚)
8052, 79, 61mul32d 11424 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) = (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))))
8177, 78, 803brtr3d 5180 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜(๐‘› โˆ’ 1)) โ‰ค (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))))
82 remsqsqrt 15203 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„ โˆง 0 โ‰ค ๐‘›) โ†’ ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜๐‘›)) = ๐‘›)
8326, 46, 82syl2anc 585 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜๐‘›)) = ๐‘›)
84 remsqsqrt 15203 . . . . . . . . . . 11 (((๐‘› โˆ’ 1) โˆˆ โ„ โˆง 0 โ‰ค (๐‘› โˆ’ 1)) โ†’ ((โˆšโ€˜(๐‘› โˆ’ 1)) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) = (๐‘› โˆ’ 1))
8528, 36, 84syl2anc 585 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜(๐‘› โˆ’ 1)) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) = (๐‘› โˆ’ 1))
8683, 85oveq12d 7427 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜๐‘›)) ยท ((โˆšโ€˜(๐‘› โˆ’ 1)) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) = (๐‘› ยท (๐‘› โˆ’ 1)))
8752, 52, 61, 61mul4d 11426 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜๐‘›)) ยท ((โˆšโ€˜(๐‘› โˆ’ 1)) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) = (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))))
8886, 87eqtr3d 2775 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (๐‘› ยท (๐‘› โˆ’ 1)) = (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))))
8916rpcnne0d 13025 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜(๐‘› โˆ’ 1)) โˆˆ โ„‚ โˆง (โˆšโ€˜(๐‘› โˆ’ 1)) โ‰  0))
9019rpcnne0d 13025 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) โˆˆ โ„‚ โˆง (โˆšโ€˜๐‘›) โ‰  0))
91 divsubdiv 11930 . . . . . . . . . 10 (((2 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚) โˆง (((โˆšโ€˜(๐‘› โˆ’ 1)) โˆˆ โ„‚ โˆง (โˆšโ€˜(๐‘› โˆ’ 1)) โ‰  0) โˆง ((โˆšโ€˜๐‘›) โˆˆ โ„‚ โˆง (โˆšโ€˜๐‘›) โ‰  0))) โ†’ ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) = (((2 ยท (โˆšโ€˜๐‘›)) โˆ’ (2 ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜(๐‘› โˆ’ 1)) ยท (โˆšโ€˜๐‘›))))
9268, 68, 89, 90, 91syl22anc 838 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) = (((2 ยท (โˆšโ€˜๐‘›)) โˆ’ (2 ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜(๐‘› โˆ’ 1)) ยท (โˆšโ€˜๐‘›))))
9368, 52, 61subdid 11670 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) = ((2 ยท (โˆšโ€˜๐‘›)) โˆ’ (2 ยท (โˆšโ€˜(๐‘› โˆ’ 1)))))
9452, 61mulcomd 11235 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) = ((โˆšโ€˜(๐‘› โˆ’ 1)) ยท (โˆšโ€˜๐‘›)))
9593, 94oveq12d 7427 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) = (((2 ยท (โˆšโ€˜๐‘›)) โˆ’ (2 ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜(๐‘› โˆ’ 1)) ยท (โˆšโ€˜๐‘›))))
9692, 95eqtr4d 2776 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) = ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))))
9788, 96oveq12d 7427 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((๐‘› ยท (๐‘› โˆ’ 1)) ยท ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›)))) = ((((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) ยท ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))))))
9852, 61mulcld 11234 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) โˆˆ โ„‚)
9919, 16rpmulcld 13032 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) โˆˆ โ„+)
10074, 99rerpdivcld 13047 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) โˆˆ โ„)
101100recnd 11242 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) โˆˆ โ„‚)
10298, 98, 101mulassd 11237 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))) ยท ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))))) = (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))))))
10399rpne0d 13021 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) โ‰  0)
10479, 98, 103divcan2d 11992 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))))) = (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))))
105104oveq2d 7425 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท ((2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1)))) / ((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1)))))) = (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))))
10697, 102, 1053eqtrd 2777 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((๐‘› ยท (๐‘› โˆ’ 1)) ยท ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›)))) = (((โˆšโ€˜๐‘›) ยท (โˆšโ€˜(๐‘› โˆ’ 1))) ยท (2 ยท ((โˆšโ€˜๐‘›) โˆ’ (โˆšโ€˜(๐‘› โˆ’ 1))))))
10781, 106breqtrrd 5177 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜(๐‘› โˆ’ 1)) โ‰ค ((๐‘› ยท (๐‘› โˆ’ 1)) ยท ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›)))))
1087, 25, 30, 39, 107letrd 11371 . . . 4 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (logโ€˜๐‘›) โ‰ค ((๐‘› ยท (๐‘› โˆ’ 1)) ยท ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›)))))
10911nngt0d 12261 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ 0 < (๐‘› ยท (๐‘› โˆ’ 1)))
110 ledivmul 12090 . . . . 5 (((logโ€˜๐‘›) โˆˆ โ„ โˆง ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) โˆˆ โ„ โˆง ((๐‘› ยท (๐‘› โˆ’ 1)) โˆˆ โ„ โˆง 0 < (๐‘› ยท (๐‘› โˆ’ 1)))) โ†’ (((logโ€˜๐‘›) / (๐‘› ยท (๐‘› โˆ’ 1))) โ‰ค ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) โ†” (logโ€˜๐‘›) โ‰ค ((๐‘› ยท (๐‘› โˆ’ 1)) ยท ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))))))
1117, 22, 29, 109, 110syl112anc 1375 . . . 4 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (((logโ€˜๐‘›) / (๐‘› ยท (๐‘› โˆ’ 1))) โ‰ค ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) โ†” (logโ€˜๐‘›) โ‰ค ((๐‘› ยท (๐‘› โˆ’ 1)) ยท ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))))))
112108, 111mpbird 257 . . 3 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((logโ€˜๐‘›) / (๐‘› ยท (๐‘› โˆ’ 1))) โ‰ค ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))))
1131, 12, 22, 112fsumle 15745 . 2 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((logโ€˜๐‘›) / (๐‘› ยท (๐‘› โˆ’ 1))) โ‰ค ฮฃ๐‘› โˆˆ (2...๐ด)((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))))
114 fvoveq1 7432 . . . . . 6 (๐‘˜ = ๐‘› โ†’ (โˆšโ€˜(๐‘˜ โˆ’ 1)) = (โˆšโ€˜(๐‘› โˆ’ 1)))
115114oveq2d 7425 . . . . 5 (๐‘˜ = ๐‘› โ†’ (2 / (โˆšโ€˜(๐‘˜ โˆ’ 1))) = (2 / (โˆšโ€˜(๐‘› โˆ’ 1))))
116 fvoveq1 7432 . . . . . 6 (๐‘˜ = (๐‘› + 1) โ†’ (โˆšโ€˜(๐‘˜ โˆ’ 1)) = (โˆšโ€˜((๐‘› + 1) โˆ’ 1)))
117116oveq2d 7425 . . . . 5 (๐‘˜ = (๐‘› + 1) โ†’ (2 / (โˆšโ€˜(๐‘˜ โˆ’ 1))) = (2 / (โˆšโ€˜((๐‘› + 1) โˆ’ 1))))
118 oveq1 7416 . . . . . . . . . 10 (๐‘˜ = 2 โ†’ (๐‘˜ โˆ’ 1) = (2 โˆ’ 1))
119 2m1e1 12338 . . . . . . . . . 10 (2 โˆ’ 1) = 1
120118, 119eqtrdi 2789 . . . . . . . . 9 (๐‘˜ = 2 โ†’ (๐‘˜ โˆ’ 1) = 1)
121120fveq2d 6896 . . . . . . . 8 (๐‘˜ = 2 โ†’ (โˆšโ€˜(๐‘˜ โˆ’ 1)) = (โˆšโ€˜1))
122 sqrt1 15218 . . . . . . . 8 (โˆšโ€˜1) = 1
123121, 122eqtrdi 2789 . . . . . . 7 (๐‘˜ = 2 โ†’ (โˆšโ€˜(๐‘˜ โˆ’ 1)) = 1)
124123oveq2d 7425 . . . . . 6 (๐‘˜ = 2 โ†’ (2 / (โˆšโ€˜(๐‘˜ โˆ’ 1))) = (2 / 1))
12567div1i 11942 . . . . . 6 (2 / 1) = 2
126124, 125eqtrdi 2789 . . . . 5 (๐‘˜ = 2 โ†’ (2 / (โˆšโ€˜(๐‘˜ โˆ’ 1))) = 2)
127 fvoveq1 7432 . . . . . 6 (๐‘˜ = (๐ด + 1) โ†’ (โˆšโ€˜(๐‘˜ โˆ’ 1)) = (โˆšโ€˜((๐ด + 1) โˆ’ 1)))
128127oveq2d 7425 . . . . 5 (๐‘˜ = (๐ด + 1) โ†’ (2 / (โˆšโ€˜(๐‘˜ โˆ’ 1))) = (2 / (โˆšโ€˜((๐ด + 1) โˆ’ 1))))
129 nnz 12579 . . . . 5 (๐ด โˆˆ โ„• โ†’ ๐ด โˆˆ โ„ค)
130 eluzp1p1 12850 . . . . . . 7 (๐ด โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ (๐ด + 1) โˆˆ (โ„คโ‰ฅโ€˜(1 + 1)))
131 nnuz 12865 . . . . . . 7 โ„• = (โ„คโ‰ฅโ€˜1)
132130, 131eleq2s 2852 . . . . . 6 (๐ด โˆˆ โ„• โ†’ (๐ด + 1) โˆˆ (โ„คโ‰ฅโ€˜(1 + 1)))
133 df-2 12275 . . . . . . 7 2 = (1 + 1)
134133fveq2i 6895 . . . . . 6 (โ„คโ‰ฅโ€˜2) = (โ„คโ‰ฅโ€˜(1 + 1))
135132, 134eleqtrrdi 2845 . . . . 5 (๐ด โˆˆ โ„• โ†’ (๐ด + 1) โˆˆ (โ„คโ‰ฅโ€˜2))
136 elfzuz 13497 . . . . . . . . . . 11 (๐‘˜ โˆˆ (2...(๐ด + 1)) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2))
137 uz2m1nn 12907 . . . . . . . . . . 11 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„•)
138136, 137syl 17 . . . . . . . . . 10 (๐‘˜ โˆˆ (2...(๐ด + 1)) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„•)
139138adantl 483 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐‘˜ โˆˆ (2...(๐ด + 1))) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„•)
140139nnrpd 13014 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘˜ โˆˆ (2...(๐ด + 1))) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„+)
141140rpsqrtcld 15358 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘˜ โˆˆ (2...(๐ด + 1))) โ†’ (โˆšโ€˜(๐‘˜ โˆ’ 1)) โˆˆ โ„+)
142 rerpdivcl 13004 . . . . . . 7 ((2 โˆˆ โ„ โˆง (โˆšโ€˜(๐‘˜ โˆ’ 1)) โˆˆ โ„+) โ†’ (2 / (โˆšโ€˜(๐‘˜ โˆ’ 1))) โˆˆ โ„)
14314, 141, 142sylancr 588 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘˜ โˆˆ (2...(๐ด + 1))) โ†’ (2 / (โˆšโ€˜(๐‘˜ โˆ’ 1))) โˆˆ โ„)
144143recnd 11242 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘˜ โˆˆ (2...(๐ด + 1))) โ†’ (2 / (โˆšโ€˜(๐‘˜ โˆ’ 1))) โˆˆ โ„‚)
145115, 117, 126, 128, 129, 135, 144telfsum 15750 . . . 4 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜((๐‘› + 1) โˆ’ 1)))) = (2 โˆ’ (2 / (โˆšโ€˜((๐ด + 1) โˆ’ 1)))))
146 pncan 11466 . . . . . . . . 9 ((๐‘› โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘› + 1) โˆ’ 1) = ๐‘›)
14731, 32, 146sylancl 587 . . . . . . . 8 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((๐‘› + 1) โˆ’ 1) = ๐‘›)
148147fveq2d 6896 . . . . . . 7 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (โˆšโ€˜((๐‘› + 1) โˆ’ 1)) = (โˆšโ€˜๐‘›))
149148oveq2d 7425 . . . . . 6 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ (2 / (โˆšโ€˜((๐‘› + 1) โˆ’ 1))) = (2 / (โˆšโ€˜๐‘›)))
150149oveq2d 7425 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐‘› โˆˆ (2...๐ด)) โ†’ ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜((๐‘› + 1) โˆ’ 1)))) = ((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))))
151150sumeq2dv 15649 . . . 4 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜((๐‘› + 1) โˆ’ 1)))) = ฮฃ๐‘› โˆˆ (2...๐ด)((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))))
152 nncn 12220 . . . . . . . 8 (๐ด โˆˆ โ„• โ†’ ๐ด โˆˆ โ„‚)
153 pncan 11466 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐ด + 1) โˆ’ 1) = ๐ด)
154152, 32, 153sylancl 587 . . . . . . 7 (๐ด โˆˆ โ„• โ†’ ((๐ด + 1) โˆ’ 1) = ๐ด)
155154fveq2d 6896 . . . . . 6 (๐ด โˆˆ โ„• โ†’ (โˆšโ€˜((๐ด + 1) โˆ’ 1)) = (โˆšโ€˜๐ด))
156155oveq2d 7425 . . . . 5 (๐ด โˆˆ โ„• โ†’ (2 / (โˆšโ€˜((๐ด + 1) โˆ’ 1))) = (2 / (โˆšโ€˜๐ด)))
157156oveq2d 7425 . . . 4 (๐ด โˆˆ โ„• โ†’ (2 โˆ’ (2 / (โˆšโ€˜((๐ด + 1) โˆ’ 1)))) = (2 โˆ’ (2 / (โˆšโ€˜๐ด))))
158145, 151, 1573eqtr3d 2781 . . 3 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) = (2 โˆ’ (2 / (โˆšโ€˜๐ด))))
159 2rp 12979 . . . . . 6 2 โˆˆ โ„+
160 nnrp 12985 . . . . . . 7 (๐ด โˆˆ โ„• โ†’ ๐ด โˆˆ โ„+)
161160rpsqrtcld 15358 . . . . . 6 (๐ด โˆˆ โ„• โ†’ (โˆšโ€˜๐ด) โˆˆ โ„+)
162 rpdivcl 12999 . . . . . 6 ((2 โˆˆ โ„+ โˆง (โˆšโ€˜๐ด) โˆˆ โ„+) โ†’ (2 / (โˆšโ€˜๐ด)) โˆˆ โ„+)
163159, 161, 162sylancr 588 . . . . 5 (๐ด โˆˆ โ„• โ†’ (2 / (โˆšโ€˜๐ด)) โˆˆ โ„+)
164163rpge0d 13020 . . . 4 (๐ด โˆˆ โ„• โ†’ 0 โ‰ค (2 / (โˆšโ€˜๐ด)))
165163rpred 13016 . . . . 5 (๐ด โˆˆ โ„• โ†’ (2 / (โˆšโ€˜๐ด)) โˆˆ โ„)
166 subge02 11730 . . . . 5 ((2 โˆˆ โ„ โˆง (2 / (โˆšโ€˜๐ด)) โˆˆ โ„) โ†’ (0 โ‰ค (2 / (โˆšโ€˜๐ด)) โ†” (2 โˆ’ (2 / (โˆšโ€˜๐ด))) โ‰ค 2))
16714, 165, 166sylancr 588 . . . 4 (๐ด โˆˆ โ„• โ†’ (0 โ‰ค (2 / (โˆšโ€˜๐ด)) โ†” (2 โˆ’ (2 / (โˆšโ€˜๐ด))) โ‰ค 2))
168164, 167mpbid 231 . . 3 (๐ด โˆˆ โ„• โ†’ (2 โˆ’ (2 / (โˆšโ€˜๐ด))) โ‰ค 2)
169158, 168eqbrtrd 5171 . 2 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((2 / (โˆšโ€˜(๐‘› โˆ’ 1))) โˆ’ (2 / (โˆšโ€˜๐‘›))) โ‰ค 2)
17013, 23, 24, 113, 169letrd 11371 1 (๐ด โˆˆ โ„• โ†’ ฮฃ๐‘› โˆˆ (2...๐ด)((logโ€˜๐‘›) / (๐‘› ยท (๐‘› โˆ’ 1))) โ‰ค 2)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941   class class class wbr 5149  โ€˜cfv 6544  (class class class)co 7409  โ„‚cc 11108  โ„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   ยท cmul 11115   < clt 11248   โ‰ค cle 11249   โˆ’ cmin 11444   / cdiv 11871  โ„•cn 12212  2c2 12267  โ„คโ‰ฅcuz 12822  โ„+crp 12974  ...cfz 13484  โ†‘cexp 14027  โˆšcsqrt 15180  ฮฃcsu 15632  logclog 26063
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188  ax-addf 11189  ax-mulf 11190
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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-fi 9406  df-sup 9437  df-inf 9438  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-ioo 13328  df-ioc 13329  df-ico 13330  df-icc 13331  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-fac 14234  df-bc 14263  df-hash 14291  df-shft 15014  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-limsup 15415  df-clim 15432  df-rlim 15433  df-sum 15633  df-ef 16011  df-sin 16013  df-cos 16014  df-tan 16015  df-pi 16016  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-starv 17212  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-unif 17220  df-hom 17221  df-cco 17222  df-rest 17368  df-topn 17369  df-0g 17387  df-gsum 17388  df-topgen 17389  df-pt 17390  df-prds 17393  df-xrs 17448  df-qtop 17453  df-imas 17454  df-xps 17456  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-submnd 18672  df-mulg 18951  df-cntz 19181  df-cmn 19650  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-mopn 20940  df-fbas 20941  df-fg 20942  df-cnfld 20945  df-top 22396  df-topon 22413  df-topsp 22435  df-bases 22449  df-cld 22523  df-ntr 22524  df-cls 22525  df-nei 22602  df-lp 22640  df-perf 22641  df-cn 22731  df-cnp 22732  df-haus 22819  df-cmp 22891  df-tx 23066  df-hmeo 23259  df-fil 23350  df-fm 23442  df-flim 23443  df-flf 23444  df-xms 23826  df-ms 23827  df-tms 23828  df-cncf 24394  df-limc 25383  df-dv 25384  df-log 26065  df-cxp 26066
This theorem is referenced by:  rplogsumlem2  26988
  Copyright terms: Public domain W3C validator