Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stirlinglem10 Structured version   Visualization version   GIF version

Theorem stirlinglem10 44410
Description: A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole ๐ต sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem10.1 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
stirlinglem10.2 ๐ต = (๐‘› โˆˆ โ„• โ†ฆ (logโ€˜(๐ดโ€˜๐‘›)))
stirlinglem10.4 ๐พ = (๐‘˜ โˆˆ โ„• โ†ฆ ((1 / ((2 ยท ๐‘˜) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘˜))))
stirlinglem10.5 ๐ฟ = (๐‘˜ โˆˆ โ„• โ†ฆ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘˜))
Assertion
Ref Expression
stirlinglem10 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜๐‘) โˆ’ (๐ตโ€˜(๐‘ + 1))) โ‰ค ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))))
Distinct variable groups:   ๐‘˜,๐‘›   ๐‘›,๐พ   ๐‘›,๐ฟ   ๐‘˜,๐‘,๐‘›
Allowed substitution hints:   ๐ด(๐‘˜,๐‘›)   ๐ต(๐‘˜,๐‘›)   ๐พ(๐‘˜)   ๐ฟ(๐‘˜)

Proof of Theorem stirlinglem10
Dummy variables ๐‘– ๐‘— are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12811 . 2 โ„• = (โ„คโ‰ฅโ€˜1)
2 1zzd 12539 . 2 (๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„ค)
3 stirlinglem10.1 . . 3 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
4 stirlinglem10.2 . . 3 ๐ต = (๐‘› โˆˆ โ„• โ†ฆ (logโ€˜(๐ดโ€˜๐‘›)))
5 eqid 2733 . . 3 (๐‘› โˆˆ โ„• โ†ฆ ((((1 + (2 ยท ๐‘›)) / 2) ยท (logโ€˜((๐‘› + 1) / ๐‘›))) โˆ’ 1)) = (๐‘› โˆˆ โ„• โ†ฆ ((((1 + (2 ยท ๐‘›)) / 2) ยท (logโ€˜((๐‘› + 1) / ๐‘›))) โˆ’ 1))
6 stirlinglem10.4 . . 3 ๐พ = (๐‘˜ โˆˆ โ„• โ†ฆ ((1 / ((2 ยท ๐‘˜) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘˜))))
73, 4, 5, 6stirlinglem9 44409 . 2 (๐‘ โˆˆ โ„• โ†’ seq1( + , ๐พ) โ‡ ((๐ตโ€˜๐‘) โˆ’ (๐ตโ€˜(๐‘ + 1))))
8 2cnd 12236 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚)
9 nncn 12166 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚)
108, 9mulcld 11180 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
11 1cnd 11155 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
1210, 11addcld 11179 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ ((2 ยท ๐‘) + 1) โˆˆ โ„‚)
1312sqcld 14055 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (((2 ยท ๐‘) + 1)โ†‘2) โˆˆ โ„‚)
14 0red 11163 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 โˆˆ โ„)
15 1red 11161 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„)
16 2re 12232 . . . . . . . . . . 11 2 โˆˆ โ„
1716a1i 11 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„)
18 nnre 12165 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„)
1917, 18remulcld 11190 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ (2 ยท ๐‘) โˆˆ โ„)
2019, 15readdcld 11189 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ((2 ยท ๐‘) + 1) โˆˆ โ„)
21 0lt1 11682 . . . . . . . . 9 0 < 1
2221a1i 11 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 < 1)
23 2rp 12925 . . . . . . . . . . 11 2 โˆˆ โ„+
2423a1i 11 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„+)
25 nnrp 12931 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„+)
2624, 25rpmulcld 12978 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ (2 ยท ๐‘) โˆˆ โ„+)
2715, 26ltaddrp2d 12996 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 1 < ((2 ยท ๐‘) + 1))
2814, 15, 20, 22, 27lttrd 11321 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 0 < ((2 ยท ๐‘) + 1))
2928gt0ne0d 11724 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ ((2 ยท ๐‘) + 1) โ‰  0)
30 2z 12540 . . . . . . 7 2 โˆˆ โ„ค
3130a1i 11 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„ค)
3212, 29, 31expne0d 14063 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (((2 ยท ๐‘) + 1)โ†‘2) โ‰  0)
3313, 32reccld 11929 . . . 4 (๐‘ โˆˆ โ„• โ†’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)) โˆˆ โ„‚)
3415renegcld 11587 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ -1 โˆˆ โ„)
3520resqcld 14036 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ (((2 ยท ๐‘) + 1)โ†‘2) โˆˆ โ„)
3635, 32rereccld 11987 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)) โˆˆ โ„)
37 1re 11160 . . . . . . . 8 1 โˆˆ โ„
38 lt0neg2 11667 . . . . . . . 8 (1 โˆˆ โ„ โ†’ (0 < 1 โ†” -1 < 0))
3937, 38ax-mp 5 . . . . . . 7 (0 < 1 โ†” -1 < 0)
4022, 39sylib 217 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ -1 < 0)
4120, 29sqgt0d 14159 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 0 < (((2 ยท ๐‘) + 1)โ†‘2))
4235, 41recgt0d 12094 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 0 < (1 / (((2 ยท ๐‘) + 1)โ†‘2)))
4334, 14, 36, 40, 42lttrd 11321 . . . . 5 (๐‘ โˆˆ โ„• โ†’ -1 < (1 / (((2 ยท ๐‘) + 1)โ†‘2)))
44 2nn 12231 . . . . . . . 8 2 โˆˆ โ„•
4544a1i 11 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
46 expgt1 14012 . . . . . . 7 ((((2 ยท ๐‘) + 1) โˆˆ โ„ โˆง 2 โˆˆ โ„• โˆง 1 < ((2 ยท ๐‘) + 1)) โ†’ 1 < (((2 ยท ๐‘) + 1)โ†‘2))
4720, 45, 27, 46syl3anc 1372 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 1 < (((2 ยท ๐‘) + 1)โ†‘2))
4835, 41elrpd 12959 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ (((2 ยท ๐‘) + 1)โ†‘2) โˆˆ โ„+)
4948recgt1d 12976 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (1 < (((2 ยท ๐‘) + 1)โ†‘2) โ†” (1 / (((2 ยท ๐‘) + 1)โ†‘2)) < 1))
5047, 49mpbid 231 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)) < 1)
5136, 15absltd 15320 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((absโ€˜(1 / (((2 ยท ๐‘) + 1)โ†‘2))) < 1 โ†” (-1 < (1 / (((2 ยท ๐‘) + 1)โ†‘2)) โˆง (1 / (((2 ยท ๐‘) + 1)โ†‘2)) < 1)))
5243, 50, 51mpbir2and 712 . . . 4 (๐‘ โˆˆ โ„• โ†’ (absโ€˜(1 / (((2 ยท ๐‘) + 1)โ†‘2))) < 1)
53 1nn0 12434 . . . . 5 1 โˆˆ โ„•0
5453a1i 11 . . . 4 (๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„•0)
55 stirlinglem10.5 . . . . . 6 ๐ฟ = (๐‘˜ โˆˆ โ„• โ†ฆ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘˜))
5655a1i 11 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ๐ฟ = (๐‘˜ โˆˆ โ„• โ†ฆ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘˜)))
57 simpr 486 . . . . . 6 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ = ๐‘—) โ†’ ๐‘˜ = ๐‘—)
5857oveq2d 7374 . . . . 5 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘˜ = ๐‘—) โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘˜) = ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘—))
59 elnnuz 12812 . . . . . . 7 (๐‘— โˆˆ โ„• โ†” ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1))
6059biimpri 227 . . . . . 6 (๐‘— โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ ๐‘— โˆˆ โ„•)
6160adantl 483 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ๐‘— โˆˆ โ„•)
6233adantr 482 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)) โˆˆ โ„‚)
6361nnnn0d 12478 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ๐‘— โˆˆ โ„•0)
6462, 63expcld 14057 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘—) โˆˆ โ„‚)
6556, 58, 61, 64fvmptd 6956 . . . 4 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ (๐ฟโ€˜๐‘—) = ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘—))
6633, 52, 54, 65geolim2 15761 . . 3 (๐‘ โˆˆ โ„• โ†’ seq1( + , ๐ฟ) โ‡ (((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘1) / (1 โˆ’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)))))
6733exp1d 14052 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘1) = (1 / (((2 ยท ๐‘) + 1)โ†‘2)))
6813, 32dividd 11934 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ((((2 ยท ๐‘) + 1)โ†‘2) / (((2 ยท ๐‘) + 1)โ†‘2)) = 1)
6968eqcomd 2739 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 1 = ((((2 ยท ๐‘) + 1)โ†‘2) / (((2 ยท ๐‘) + 1)โ†‘2)))
7069oveq1d 7373 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (1 โˆ’ (1 / (((2 ยท ๐‘) + 1)โ†‘2))) = (((((2 ยท ๐‘) + 1)โ†‘2) / (((2 ยท ๐‘) + 1)โ†‘2)) โˆ’ (1 / (((2 ยท ๐‘) + 1)โ†‘2))))
7148rpcnne0d 12971 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ((((2 ยท ๐‘) + 1)โ†‘2) โˆˆ โ„‚ โˆง (((2 ยท ๐‘) + 1)โ†‘2) โ‰  0))
72 divsubdir 11854 . . . . . . 7 (((((2 ยท ๐‘) + 1)โ†‘2) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง ((((2 ยท ๐‘) + 1)โ†‘2) โˆˆ โ„‚ โˆง (((2 ยท ๐‘) + 1)โ†‘2) โ‰  0)) โ†’ (((((2 ยท ๐‘) + 1)โ†‘2) โˆ’ 1) / (((2 ยท ๐‘) + 1)โ†‘2)) = (((((2 ยท ๐‘) + 1)โ†‘2) / (((2 ยท ๐‘) + 1)โ†‘2)) โˆ’ (1 / (((2 ยท ๐‘) + 1)โ†‘2))))
7313, 11, 71, 72syl3anc 1372 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (((((2 ยท ๐‘) + 1)โ†‘2) โˆ’ 1) / (((2 ยท ๐‘) + 1)โ†‘2)) = (((((2 ยท ๐‘) + 1)โ†‘2) / (((2 ยท ๐‘) + 1)โ†‘2)) โˆ’ (1 / (((2 ยท ๐‘) + 1)โ†‘2))))
74 ax-1cn 11114 . . . . . . . . . 10 1 โˆˆ โ„‚
75 binom2 14127 . . . . . . . . . 10 (((2 ยท ๐‘) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (((2 ยท ๐‘) + 1)โ†‘2) = ((((2 ยท ๐‘)โ†‘2) + (2 ยท ((2 ยท ๐‘) ยท 1))) + (1โ†‘2)))
7610, 74, 75sylancl 587 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ (((2 ยท ๐‘) + 1)โ†‘2) = ((((2 ยท ๐‘)โ†‘2) + (2 ยท ((2 ยท ๐‘) ยท 1))) + (1โ†‘2)))
7776oveq1d 7373 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ((((2 ยท ๐‘) + 1)โ†‘2) โˆ’ 1) = (((((2 ยท ๐‘)โ†‘2) + (2 ยท ((2 ยท ๐‘) ยท 1))) + (1โ†‘2)) โˆ’ 1))
788, 9sqmuld 14069 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„• โ†’ ((2 ยท ๐‘)โ†‘2) = ((2โ†‘2) ยท (๐‘โ†‘2)))
79 sq2 14107 . . . . . . . . . . . . . . 15 (2โ†‘2) = 4
8079a1i 11 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ (2โ†‘2) = 4)
8180oveq1d 7373 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„• โ†’ ((2โ†‘2) ยท (๐‘โ†‘2)) = (4 ยท (๐‘โ†‘2)))
8278, 81eqtrd 2773 . . . . . . . . . . . 12 (๐‘ โˆˆ โ„• โ†’ ((2 ยท ๐‘)โ†‘2) = (4 ยท (๐‘โ†‘2)))
8310mulid1d 11177 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ ((2 ยท ๐‘) ยท 1) = (2 ยท ๐‘))
8483oveq2d 7374 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„• โ†’ (2 ยท ((2 ยท ๐‘) ยท 1)) = (2 ยท (2 ยท ๐‘)))
858, 8, 9mulassd 11183 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„• โ†’ ((2 ยท 2) ยท ๐‘) = (2 ยท (2 ยท ๐‘)))
86 2t2e4 12322 . . . . . . . . . . . . . . 15 (2 ยท 2) = 4
8786a1i 11 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ (2 ยท 2) = 4)
8887oveq1d 7373 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„• โ†’ ((2 ยท 2) ยท ๐‘) = (4 ยท ๐‘))
8984, 85, 883eqtr2d 2779 . . . . . . . . . . . 12 (๐‘ โˆˆ โ„• โ†’ (2 ยท ((2 ยท ๐‘) ยท 1)) = (4 ยท ๐‘))
9082, 89oveq12d 7376 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ (((2 ยท ๐‘)โ†‘2) + (2 ยท ((2 ยท ๐‘) ยท 1))) = ((4 ยท (๐‘โ†‘2)) + (4 ยท ๐‘)))
91 4cn 12243 . . . . . . . . . . . . 13 4 โˆˆ โ„‚
9291a1i 11 . . . . . . . . . . . 12 (๐‘ โˆˆ โ„• โ†’ 4 โˆˆ โ„‚)
939sqcld 14055 . . . . . . . . . . . 12 (๐‘ โˆˆ โ„• โ†’ (๐‘โ†‘2) โˆˆ โ„‚)
9492, 93, 9adddid 11184 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ (4 ยท ((๐‘โ†‘2) + ๐‘)) = ((4 ยท (๐‘โ†‘2)) + (4 ยท ๐‘)))
959sqvald 14054 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ (๐‘โ†‘2) = (๐‘ ยท ๐‘))
969mulid1d 11177 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ โ„• โ†’ (๐‘ ยท 1) = ๐‘)
9796eqcomd 2739 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ ๐‘ = (๐‘ ยท 1))
9895, 97oveq12d 7376 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„• โ†’ ((๐‘โ†‘2) + ๐‘) = ((๐‘ ยท ๐‘) + (๐‘ ยท 1)))
999, 9, 11adddid 11184 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„• โ†’ (๐‘ ยท (๐‘ + 1)) = ((๐‘ ยท ๐‘) + (๐‘ ยท 1)))
10098, 99eqtr4d 2776 . . . . . . . . . . . 12 (๐‘ โˆˆ โ„• โ†’ ((๐‘โ†‘2) + ๐‘) = (๐‘ ยท (๐‘ + 1)))
101100oveq2d 7374 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ (4 ยท ((๐‘โ†‘2) + ๐‘)) = (4 ยท (๐‘ ยท (๐‘ + 1))))
10290, 94, 1013eqtr2d 2779 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ (((2 ยท ๐‘)โ†‘2) + (2 ยท ((2 ยท ๐‘) ยท 1))) = (4 ยท (๐‘ ยท (๐‘ + 1))))
103 sq1 14105 . . . . . . . . . . 11 (1โ†‘2) = 1
104103a1i 11 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ (1โ†‘2) = 1)
105102, 104oveq12d 7376 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ((((2 ยท ๐‘)โ†‘2) + (2 ยท ((2 ยท ๐‘) ยท 1))) + (1โ†‘2)) = ((4 ยท (๐‘ ยท (๐‘ + 1))) + 1))
106105oveq1d 7373 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (((((2 ยท ๐‘)โ†‘2) + (2 ยท ((2 ยท ๐‘) ยท 1))) + (1โ†‘2)) โˆ’ 1) = (((4 ยท (๐‘ ยท (๐‘ + 1))) + 1) โˆ’ 1))
1079, 11addcld 11179 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ (๐‘ + 1) โˆˆ โ„‚)
1089, 107mulcld 11180 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ (๐‘ ยท (๐‘ + 1)) โˆˆ โ„‚)
10992, 108mulcld 11180 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ (4 ยท (๐‘ ยท (๐‘ + 1))) โˆˆ โ„‚)
110109, 11pncand 11518 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (((4 ยท (๐‘ ยท (๐‘ + 1))) + 1) โˆ’ 1) = (4 ยท (๐‘ ยท (๐‘ + 1))))
11177, 106, 1103eqtrd 2777 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ((((2 ยท ๐‘) + 1)โ†‘2) โˆ’ 1) = (4 ยท (๐‘ ยท (๐‘ + 1))))
112111oveq1d 7373 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (((((2 ยท ๐‘) + 1)โ†‘2) โˆ’ 1) / (((2 ยท ๐‘) + 1)โ†‘2)) = ((4 ยท (๐‘ ยท (๐‘ + 1))) / (((2 ยท ๐‘) + 1)โ†‘2)))
11370, 73, 1123eqtr2d 2779 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (1 โˆ’ (1 / (((2 ยท ๐‘) + 1)โ†‘2))) = ((4 ยท (๐‘ ยท (๐‘ + 1))) / (((2 ยท ๐‘) + 1)โ†‘2)))
11467, 113oveq12d 7376 . . . 4 (๐‘ โˆˆ โ„• โ†’ (((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘1) / (1 โˆ’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)))) = ((1 / (((2 ยท ๐‘) + 1)โ†‘2)) / ((4 ยท (๐‘ ยท (๐‘ + 1))) / (((2 ยท ๐‘) + 1)โ†‘2))))
115 4pos 12265 . . . . . . . . 9 0 < 4
116115a1i 11 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 < 4)
117116gt0ne0d 11724 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 4 โ‰  0)
118 nnne0 12192 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0)
11918, 15readdcld 11189 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ (๐‘ + 1) โˆˆ โ„)
120 nngt0 12189 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ 0 < ๐‘)
12118ltp1d 12090 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ ๐‘ < (๐‘ + 1))
12214, 18, 119, 120, 121lttrd 11321 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ 0 < (๐‘ + 1))
123122gt0ne0d 11724 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (๐‘ + 1) โ‰  0)
1249, 107, 118, 123mulne0d 11812 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ (๐‘ ยท (๐‘ + 1)) โ‰  0)
12592, 108, 117, 124mulne0d 11812 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (4 ยท (๐‘ ยท (๐‘ + 1))) โ‰  0)
12611, 13, 109, 13, 32, 32, 125divdivdivd 11983 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2)) / ((4 ยท (๐‘ ยท (๐‘ + 1))) / (((2 ยท ๐‘) + 1)โ†‘2))) = ((1 ยท (((2 ยท ๐‘) + 1)โ†‘2)) / ((((2 ยท ๐‘) + 1)โ†‘2) ยท (4 ยท (๐‘ ยท (๐‘ + 1))))))
12711, 13mulcomd 11181 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (1 ยท (((2 ยท ๐‘) + 1)โ†‘2)) = ((((2 ยท ๐‘) + 1)โ†‘2) ยท 1))
128127oveq1d 7373 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 ยท (((2 ยท ๐‘) + 1)โ†‘2)) / ((((2 ยท ๐‘) + 1)โ†‘2) ยท (4 ยท (๐‘ ยท (๐‘ + 1))))) = (((((2 ยท ๐‘) + 1)โ†‘2) ยท 1) / ((((2 ยท ๐‘) + 1)โ†‘2) ยท (4 ยท (๐‘ ยท (๐‘ + 1))))))
12911mulid1d 11177 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ (1 ยท 1) = 1)
130129eqcomd 2739 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ 1 = (1 ยท 1))
131130oveq1d 7373 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (1 / (4 ยท (๐‘ ยท (๐‘ + 1)))) = ((1 ยท 1) / (4 ยท (๐‘ ยท (๐‘ + 1)))))
13211, 92, 11, 108, 117, 124divmuldivd 11977 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))) = ((1 ยท 1) / (4 ยท (๐‘ ยท (๐‘ + 1)))))
133131, 132eqtr4d 2776 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ (1 / (4 ยท (๐‘ ยท (๐‘ + 1)))) = ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))))
13468, 133oveq12d 7376 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (((((2 ยท ๐‘) + 1)โ†‘2) / (((2 ยท ๐‘) + 1)โ†‘2)) ยท (1 / (4 ยท (๐‘ ยท (๐‘ + 1))))) = (1 ยท ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1))))))
13513, 13, 11, 109, 32, 125divmuldivd 11977 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (((((2 ยท ๐‘) + 1)โ†‘2) / (((2 ยท ๐‘) + 1)โ†‘2)) ยท (1 / (4 ยท (๐‘ ยท (๐‘ + 1))))) = (((((2 ยท ๐‘) + 1)โ†‘2) ยท 1) / ((((2 ยท ๐‘) + 1)โ†‘2) ยท (4 ยท (๐‘ ยท (๐‘ + 1))))))
13692, 117reccld 11929 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (1 / 4) โˆˆ โ„‚)
137108, 124reccld 11929 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (1 / (๐‘ ยท (๐‘ + 1))) โˆˆ โ„‚)
138136, 137mulcld 11180 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))) โˆˆ โ„‚)
139138mulid2d 11178 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (1 ยท ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1))))) = ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))))
140134, 135, 1393eqtr3d 2781 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (((((2 ยท ๐‘) + 1)โ†‘2) ยท 1) / ((((2 ยท ๐‘) + 1)โ†‘2) ยท (4 ยท (๐‘ ยท (๐‘ + 1))))) = ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))))
141126, 128, 1403eqtrd 2777 . . . 4 (๐‘ โˆˆ โ„• โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2)) / ((4 ยท (๐‘ ยท (๐‘ + 1))) / (((2 ยท ๐‘) + 1)โ†‘2))) = ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))))
142114, 141eqtrd 2773 . . 3 (๐‘ โˆˆ โ„• โ†’ (((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘1) / (1 โˆ’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)))) = ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))))
14366, 142breqtrd 5132 . 2 (๐‘ โˆˆ โ„• โ†’ seq1( + , ๐ฟ) โ‡ ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))))
14459biimpi 215 . . . 4 (๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1))
145144adantl 483 . . 3 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜1))
146 oveq2 7366 . . . . . . . . 9 (๐‘˜ = ๐‘› โ†’ (2 ยท ๐‘˜) = (2 ยท ๐‘›))
147146oveq1d 7373 . . . . . . . 8 (๐‘˜ = ๐‘› โ†’ ((2 ยท ๐‘˜) + 1) = ((2 ยท ๐‘›) + 1))
148147oveq2d 7374 . . . . . . 7 (๐‘˜ = ๐‘› โ†’ (1 / ((2 ยท ๐‘˜) + 1)) = (1 / ((2 ยท ๐‘›) + 1)))
149146oveq2d 7374 . . . . . . 7 (๐‘˜ = ๐‘› โ†’ ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘˜)) = ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›)))
150148, 149oveq12d 7376 . . . . . 6 (๐‘˜ = ๐‘› โ†’ ((1 / ((2 ยท ๐‘˜) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘˜))) = ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›))))
151 elfznn 13476 . . . . . . 7 (๐‘› โˆˆ (1...๐‘—) โ†’ ๐‘› โˆˆ โ„•)
152151adantl 483 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ๐‘› โˆˆ โ„•)
153 2cnd 12236 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 2 โˆˆ โ„‚)
154152nncnd 12174 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ๐‘› โˆˆ โ„‚)
155153, 154mulcld 11180 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (2 ยท ๐‘›) โˆˆ โ„‚)
156 1cnd 11155 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 1 โˆˆ โ„‚)
157155, 156addcld 11179 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„‚)
158 0red 11163 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 0 โˆˆ โ„)
159 1red 11161 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„)
16016a1i 11 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„)
161 nnre 12165 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„)
162160, 161remulcld 11190 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„)
163162, 159readdcld 11189 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„)
16421a1i 11 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 0 < 1)
16523a1i 11 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„+)
166 nnrp 12931 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„+)
167165, 166rpmulcld 12978 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„+)
168159, 167ltaddrp2d 12996 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 1 < ((2 ยท ๐‘›) + 1))
169158, 159, 163, 164, 168lttrd 11321 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ 0 < ((2 ยท ๐‘›) + 1))
170151, 169syl 17 . . . . . . . . . 10 (๐‘› โˆˆ (1...๐‘—) โ†’ 0 < ((2 ยท ๐‘›) + 1))
171170gt0ne0d 11724 . . . . . . . . 9 (๐‘› โˆˆ (1...๐‘—) โ†’ ((2 ยท ๐‘›) + 1) โ‰  0)
172171adantl 483 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((2 ยท ๐‘›) + 1) โ‰  0)
173157, 172reccld 11929 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / ((2 ยท ๐‘›) + 1)) โˆˆ โ„‚)
1749adantr 482 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ๐‘ โˆˆ โ„‚)
175153, 174mulcld 11180 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
176175, 156addcld 11179 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((2 ยท ๐‘) + 1) โˆˆ โ„‚)
17729adantr 482 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((2 ยท ๐‘) + 1) โ‰  0)
178176, 177reccld 11929 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / ((2 ยท ๐‘) + 1)) โˆˆ โ„‚)
179 2nn0 12435 . . . . . . . . . 10 2 โˆˆ โ„•0
180179a1i 11 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 2 โˆˆ โ„•0)
181152nnnn0d 12478 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ๐‘› โˆˆ โ„•0)
182180, 181nn0mulcld 12483 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (2 ยท ๐‘›) โˆˆ โ„•0)
183178, 182expcld 14057 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›)) โˆˆ โ„‚)
184173, 183mulcld 11180 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›))) โˆˆ โ„‚)
1856, 150, 152, 184fvmptd3 6972 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (๐พโ€˜๐‘›) = ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›))))
186185adantlr 714 . . . 4 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (๐พโ€˜๐‘›) = ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›))))
187169gt0ne0d 11724 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โ‰  0)
188163, 187rereccld 11987 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (1 / ((2 ยท ๐‘›) + 1)) โˆˆ โ„)
189151, 188syl 17 . . . . . 6 (๐‘› โˆˆ (1...๐‘—) โ†’ (1 / ((2 ยท ๐‘›) + 1)) โˆˆ โ„)
190189adantl 483 . . . . 5 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / ((2 ยท ๐‘›) + 1)) โˆˆ โ„)
19120, 29rereccld 11987 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (1 / ((2 ยท ๐‘) + 1)) โˆˆ โ„)
192191adantr 482 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / ((2 ยท ๐‘) + 1)) โˆˆ โ„)
193192, 182reexpcld 14074 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›)) โˆˆ โ„)
194193adantlr 714 . . . . 5 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›)) โˆˆ โ„)
195190, 194remulcld 11190 . . . 4 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›))) โˆˆ โ„)
196186, 195eqeltrd 2834 . . 3 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (๐พโ€˜๐‘›) โˆˆ โ„)
197 readdcl 11139 . . . 4 ((๐‘› โˆˆ โ„ โˆง ๐‘– โˆˆ โ„) โ†’ (๐‘› + ๐‘–) โˆˆ โ„)
198197adantl 483 . . 3 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„ โˆง ๐‘– โˆˆ โ„)) โ†’ (๐‘› + ๐‘–) โˆˆ โ„)
199145, 196, 198seqcl 13934 . 2 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (seq1( + , ๐พ)โ€˜๐‘—) โˆˆ โ„)
200 oveq2 7366 . . . . . 6 (๐‘˜ = ๐‘› โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘˜) = ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›))
20133adantr 482 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)) โˆˆ โ„‚)
202201, 181expcld 14057 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›) โˆˆ โ„‚)
20355, 200, 152, 202fvmptd3 6972 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (๐ฟโ€˜๐‘›) = ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›))
20436adantr 482 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)) โˆˆ โ„)
205204, 181reexpcld 14074 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›) โˆˆ โ„)
206203, 205eqeltrd 2834 . . . 4 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (๐ฟโ€˜๐‘›) โˆˆ โ„)
207206adantlr 714 . . 3 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (๐ฟโ€˜๐‘›) โˆˆ โ„)
208145, 207, 198seqcl 13934 . 2 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (seq1( + , ๐ฟ)โ€˜๐‘—) โˆˆ โ„)
20930a1i 11 . . . . . . . . . . . . 13 (๐‘› โˆˆ (1...๐‘—) โ†’ 2 โˆˆ โ„ค)
210 elfzelz 13447 . . . . . . . . . . . . 13 (๐‘› โˆˆ (1...๐‘—) โ†’ ๐‘› โˆˆ โ„ค)
211209, 210zmulcld 12618 . . . . . . . . . . . 12 (๐‘› โˆˆ (1...๐‘—) โ†’ (2 ยท ๐‘›) โˆˆ โ„ค)
212 1exp 14003 . . . . . . . . . . . 12 ((2 ยท ๐‘›) โˆˆ โ„ค โ†’ (1โ†‘(2 ยท ๐‘›)) = 1)
213211, 212syl 17 . . . . . . . . . . 11 (๐‘› โˆˆ (1...๐‘—) โ†’ (1โ†‘(2 ยท ๐‘›)) = 1)
214 1exp 14003 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„ค โ†’ (1โ†‘๐‘›) = 1)
215210, 214syl 17 . . . . . . . . . . 11 (๐‘› โˆˆ (1...๐‘—) โ†’ (1โ†‘๐‘›) = 1)
216213, 215eqtr4d 2776 . . . . . . . . . 10 (๐‘› โˆˆ (1...๐‘—) โ†’ (1โ†‘(2 ยท ๐‘›)) = (1โ†‘๐‘›))
217216adantl 483 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1โ†‘(2 ยท ๐‘›)) = (1โ†‘๐‘›))
218176, 181, 180expmuld 14060 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (((2 ยท ๐‘) + 1)โ†‘(2 ยท ๐‘›)) = ((((2 ยท ๐‘) + 1)โ†‘2)โ†‘๐‘›))
219217, 218oveq12d 7376 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1โ†‘(2 ยท ๐‘›)) / (((2 ยท ๐‘) + 1)โ†‘(2 ยท ๐‘›))) = ((1โ†‘๐‘›) / ((((2 ยท ๐‘) + 1)โ†‘2)โ†‘๐‘›)))
220156, 176, 177, 182expdivd 14071 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›)) = ((1โ†‘(2 ยท ๐‘›)) / (((2 ยท ๐‘) + 1)โ†‘(2 ยท ๐‘›))))
221176sqcld 14055 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (((2 ยท ๐‘) + 1)โ†‘2) โˆˆ โ„‚)
22230a1i 11 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 2 โˆˆ โ„ค)
223176, 177, 222expne0d 14063 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (((2 ยท ๐‘) + 1)โ†‘2) โ‰  0)
224156, 221, 223, 181expdivd 14071 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›) = ((1โ†‘๐‘›) / ((((2 ยท ๐‘) + 1)โ†‘2)โ†‘๐‘›)))
225219, 220, 2243eqtr4d 2783 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›)) = ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›))
226225oveq2d 7374 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›))) = ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›)))
227 1rp 12924 . . . . . . . . . . 11 1 โˆˆ โ„+
228227a1i 11 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 1 โˆˆ โ„+)
22916a1i 11 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 2 โˆˆ โ„)
230152nnred 12173 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ๐‘› โˆˆ โ„)
231229, 230remulcld 11190 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (2 ยท ๐‘›) โˆˆ โ„)
232180nn0ge0d 12481 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 0 โ‰ค 2)
233181nn0ge0d 12481 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 0 โ‰ค ๐‘›)
234229, 230, 232, 233mulge0d 11737 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 0 โ‰ค (2 ยท ๐‘›))
235231, 234ge0p1rpd 12992 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„+)
236 1red 11161 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 1 โˆˆ โ„)
237228rpge0d 12966 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 0 โ‰ค 1)
238159, 163, 168ltled 11308 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 1 โ‰ค ((2 ยท ๐‘›) + 1))
239151, 238syl 17 . . . . . . . . . . 11 (๐‘› โˆˆ (1...๐‘—) โ†’ 1 โ‰ค ((2 ยท ๐‘›) + 1))
240239adantl 483 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 1 โ‰ค ((2 ยท ๐‘›) + 1))
241228, 235, 236, 237, 240lediv2ad 12984 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / ((2 ยท ๐‘›) + 1)) โ‰ค (1 / 1))
242156div1d 11928 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / 1) = 1)
243241, 242breqtrd 5132 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / ((2 ยท ๐‘›) + 1)) โ‰ค 1)
244152, 188syl 17 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / ((2 ยท ๐‘›) + 1)) โˆˆ โ„)
24518adantr 482 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ๐‘ โˆˆ โ„)
246229, 245remulcld 11190 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (2 ยท ๐‘) โˆˆ โ„)
24714, 18, 120ltled 11308 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ๐‘)
248247adantr 482 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 0 โ‰ค ๐‘)
249229, 245, 232, 248mulge0d 11737 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ 0 โ‰ค (2 ยท ๐‘))
250246, 249ge0p1rpd 12992 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((2 ยท ๐‘) + 1) โˆˆ โ„+)
251250, 222rpexpcld 14156 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (((2 ยท ๐‘) + 1)โ†‘2) โˆˆ โ„+)
252251rpreccld 12972 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 / (((2 ยท ๐‘) + 1)โ†‘2)) โˆˆ โ„+)
253210adantl 483 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ๐‘› โˆˆ โ„ค)
254252, 253rpexpcld 14156 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›) โˆˆ โ„+)
255244, 236, 254lemul1d 13005 . . . . . . . 8 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘›) + 1)) โ‰ค 1 โ†” ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›)) โ‰ค (1 ยท ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›))))
256243, 255mpbid 231 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›)) โ‰ค (1 ยท ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›)))
257202mulid2d 11178 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (1 ยท ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›)) = ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›))
258256, 257breqtrd 5132 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›)) โ‰ค ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›))
259226, 258eqbrtrd 5128 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ ((1 / ((2 ยท ๐‘›) + 1)) ยท ((1 / ((2 ยท ๐‘) + 1))โ†‘(2 ยท ๐‘›))) โ‰ค ((1 / (((2 ยท ๐‘) + 1)โ†‘2))โ†‘๐‘›))
260259, 185, 2033brtr4d 5138 . . . 4 ((๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (๐พโ€˜๐‘›) โ‰ค (๐ฟโ€˜๐‘›))
261260adantlr 714 . . 3 (((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘—)) โ†’ (๐พโ€˜๐‘›) โ‰ค (๐ฟโ€˜๐‘›))
262145, 196, 207, 261serle 13969 . 2 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (seq1( + , ๐พ)โ€˜๐‘—) โ‰ค (seq1( + , ๐ฟ)โ€˜๐‘—))
2631, 2, 7, 143, 199, 208, 262climle 15528 1 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜๐‘) โˆ’ (๐ตโ€˜(๐‘ + 1))) โ‰ค ((1 / 4) ยท (1 / (๐‘ ยท (๐‘ + 1)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940   class class class wbr 5106   โ†ฆ cmpt 5189  โ€˜cfv 6497  (class class class)co 7358  โ„‚cc 11054  โ„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   ยท cmul 11061   < clt 11194   โ‰ค cle 11195   โˆ’ cmin 11390  -cneg 11391   / cdiv 11817  โ„•cn 12158  2c2 12213  4c4 12215  โ„•0cn0 12418  โ„คcz 12504  โ„คโ‰ฅcuz 12768  โ„+crp 12920  ...cfz 13430  seqcseq 13912  โ†‘cexp 13973  !cfa 14179  โˆšcsqrt 15124  abscabs 15125   โ‡ cli 15372  eceu 15950  logclog 25926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-xnn0 12491  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577  df-ef 15955  df-e 15956  df-sin 15957  df-cos 15958  df-tan 15959  df-pi 15960  df-dvds 16142  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-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
This theorem is referenced by:  stirlinglem12  44412
  Copyright terms: Public domain W3C validator