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

Theorem stirlinglem12 44412
Description: The sequence ๐ต is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem12.1 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
stirlinglem12.2 ๐ต = (๐‘› โˆˆ โ„• โ†ฆ (logโ€˜(๐ดโ€˜๐‘›)))
stirlinglem12.3 ๐น = (๐‘› โˆˆ โ„• โ†ฆ (1 / (๐‘› ยท (๐‘› + 1))))
Assertion
Ref Expression
stirlinglem12 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜1) โˆ’ (1 / 4)) โ‰ค (๐ตโ€˜๐‘))
Distinct variable group:   ๐‘›,๐‘
Allowed substitution hints:   ๐ด(๐‘›)   ๐ต(๐‘›)   ๐น(๐‘›)

Proof of Theorem stirlinglem12
Dummy variables ๐‘– ๐‘— ๐‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1nn 12169 . . . . 5 1 โˆˆ โ„•
2 stirlinglem12.1 . . . . . . 7 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
32stirlinglem2 44402 . . . . . 6 (1 โˆˆ โ„• โ†’ (๐ดโ€˜1) โˆˆ โ„+)
4 relogcl 25947 . . . . . 6 ((๐ดโ€˜1) โˆˆ โ„+ โ†’ (logโ€˜(๐ดโ€˜1)) โˆˆ โ„)
51, 3, 4mp2b 10 . . . . 5 (logโ€˜(๐ดโ€˜1)) โˆˆ โ„
6 nfcv 2904 . . . . . 6 โ„ฒ๐‘›1
7 nfcv 2904 . . . . . . 7 โ„ฒ๐‘›log
8 nfmpt1 5214 . . . . . . . . 9 โ„ฒ๐‘›(๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
92, 8nfcxfr 2902 . . . . . . . 8 โ„ฒ๐‘›๐ด
109, 6nffv 6853 . . . . . . 7 โ„ฒ๐‘›(๐ดโ€˜1)
117, 10nffv 6853 . . . . . 6 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜1))
12 2fveq3 6848 . . . . . 6 (๐‘› = 1 โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜1)))
13 stirlinglem12.2 . . . . . 6 ๐ต = (๐‘› โˆˆ โ„• โ†ฆ (logโ€˜(๐ดโ€˜๐‘›)))
146, 11, 12, 13fvmptf 6970 . . . . 5 ((1 โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜1)) โˆˆ โ„) โ†’ (๐ตโ€˜1) = (logโ€˜(๐ดโ€˜1)))
151, 5, 14mp2an 691 . . . 4 (๐ตโ€˜1) = (logโ€˜(๐ดโ€˜1))
1615, 5eqeltri 2830 . . 3 (๐ตโ€˜1) โˆˆ โ„
1716a1i 11 . 2 (๐‘ โˆˆ โ„• โ†’ (๐ตโ€˜1) โˆˆ โ„)
182stirlinglem2 44402 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (๐ดโ€˜๐‘) โˆˆ โ„+)
1918relogcld 25994 . . . 4 (๐‘ โˆˆ โ„• โ†’ (logโ€˜(๐ดโ€˜๐‘)) โˆˆ โ„)
20 nfcv 2904 . . . . 5 โ„ฒ๐‘›๐‘
219, 20nffv 6853 . . . . . 6 โ„ฒ๐‘›(๐ดโ€˜๐‘)
227, 21nffv 6853 . . . . 5 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜๐‘))
23 2fveq3 6848 . . . . 5 (๐‘› = ๐‘ โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜๐‘)))
2420, 22, 23, 13fvmptf 6970 . . . 4 ((๐‘ โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜๐‘)) โˆˆ โ„) โ†’ (๐ตโ€˜๐‘) = (logโ€˜(๐ดโ€˜๐‘)))
2519, 24mpdan 686 . . 3 (๐‘ โˆˆ โ„• โ†’ (๐ตโ€˜๐‘) = (logโ€˜(๐ดโ€˜๐‘)))
2625, 19eqeltrd 2834 . 2 (๐‘ โˆˆ โ„• โ†’ (๐ตโ€˜๐‘) โˆˆ โ„)
27 4re 12242 . . . 4 4 โˆˆ โ„
28 4ne0 12266 . . . 4 4 โ‰  0
2927, 28rereccli 11925 . . 3 (1 / 4) โˆˆ โ„
3029a1i 11 . 2 (๐‘ โˆˆ โ„• โ†’ (1 / 4) โˆˆ โ„)
31 fveq2 6843 . . . . 5 (๐‘˜ = ๐‘— โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜๐‘—))
32 fveq2 6843 . . . . 5 (๐‘˜ = (๐‘— + 1) โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜(๐‘— + 1)))
33 fveq2 6843 . . . . 5 (๐‘˜ = 1 โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜1))
34 fveq2 6843 . . . . 5 (๐‘˜ = ๐‘ โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜๐‘))
35 elnnuz 12812 . . . . . 6 (๐‘ โˆˆ โ„• โ†” ๐‘ โˆˆ (โ„คโ‰ฅโ€˜1))
3635biimpi 215 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜1))
37 elfznn 13476 . . . . . . . 8 (๐‘˜ โˆˆ (1...๐‘) โ†’ ๐‘˜ โˆˆ โ„•)
382stirlinglem2 44402 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (๐ดโ€˜๐‘˜) โˆˆ โ„+)
3937, 38syl 17 . . . . . . . . 9 (๐‘˜ โˆˆ (1...๐‘) โ†’ (๐ดโ€˜๐‘˜) โˆˆ โ„+)
4039relogcld 25994 . . . . . . . 8 (๐‘˜ โˆˆ (1...๐‘) โ†’ (logโ€˜(๐ดโ€˜๐‘˜)) โˆˆ โ„)
41 nfcv 2904 . . . . . . . . 9 โ„ฒ๐‘›๐‘˜
429, 41nffv 6853 . . . . . . . . . 10 โ„ฒ๐‘›(๐ดโ€˜๐‘˜)
437, 42nffv 6853 . . . . . . . . 9 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜๐‘˜))
44 2fveq3 6848 . . . . . . . . 9 (๐‘› = ๐‘˜ โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜๐‘˜)))
4541, 43, 44, 13fvmptf 6970 . . . . . . . 8 ((๐‘˜ โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜๐‘˜)) โˆˆ โ„) โ†’ (๐ตโ€˜๐‘˜) = (logโ€˜(๐ดโ€˜๐‘˜)))
4637, 40, 45syl2anc 585 . . . . . . 7 (๐‘˜ โˆˆ (1...๐‘) โ†’ (๐ตโ€˜๐‘˜) = (logโ€˜(๐ดโ€˜๐‘˜)))
4746adantl 483 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘˜) = (logโ€˜(๐ดโ€˜๐‘˜)))
4839rpcnd 12964 . . . . . . . 8 (๐‘˜ โˆˆ (1...๐‘) โ†’ (๐ดโ€˜๐‘˜) โˆˆ โ„‚)
4948adantl 483 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘˜) โˆˆ โ„‚)
5038rpne0d 12967 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (๐ดโ€˜๐‘˜) โ‰  0)
5137, 50syl 17 . . . . . . . 8 (๐‘˜ โˆˆ (1...๐‘) โ†’ (๐ดโ€˜๐‘˜) โ‰  0)
5251adantl 483 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘˜) โ‰  0)
5349, 52logcld 25942 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (logโ€˜(๐ดโ€˜๐‘˜)) โˆˆ โ„‚)
5447, 53eqeltrd 2834 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘˜) โˆˆ โ„‚)
5531, 32, 33, 34, 36, 54telfsumo 15692 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1..^๐‘)((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) = ((๐ตโ€˜1) โˆ’ (๐ตโ€˜๐‘)))
56 nnz 12525 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ค)
57 fzoval 13579 . . . . . 6 (๐‘ โˆˆ โ„ค โ†’ (1..^๐‘) = (1...(๐‘ โˆ’ 1)))
5856, 57syl 17 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (1..^๐‘) = (1...(๐‘ โˆ’ 1)))
5958sumeq1d 15591 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1..^๐‘)((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) = ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))))
6055, 59eqtr3d 2775 . . 3 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜1) โˆ’ (๐ตโ€˜๐‘)) = ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))))
61 fzfid 13884 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (1...(๐‘ โˆ’ 1)) โˆˆ Fin)
62 elfznn 13476 . . . . . . . 8 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ ๐‘— โˆˆ โ„•)
6362adantl 483 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ ๐‘— โˆˆ โ„•)
642stirlinglem2 44402 . . . . . . . . . 10 (๐‘— โˆˆ โ„• โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„+)
6564relogcld 25994 . . . . . . . . 9 (๐‘— โˆˆ โ„• โ†’ (logโ€˜(๐ดโ€˜๐‘—)) โˆˆ โ„)
66 nfcv 2904 . . . . . . . . . 10 โ„ฒ๐‘›๐‘—
679, 66nffv 6853 . . . . . . . . . . 11 โ„ฒ๐‘›(๐ดโ€˜๐‘—)
687, 67nffv 6853 . . . . . . . . . 10 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜๐‘—))
69 2fveq3 6848 . . . . . . . . . 10 (๐‘› = ๐‘— โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜๐‘—)))
7066, 68, 69, 13fvmptf 6970 . . . . . . . . 9 ((๐‘— โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜๐‘—)) โˆˆ โ„) โ†’ (๐ตโ€˜๐‘—) = (logโ€˜(๐ดโ€˜๐‘—)))
7165, 70mpdan 686 . . . . . . . 8 (๐‘— โˆˆ โ„• โ†’ (๐ตโ€˜๐‘—) = (logโ€˜(๐ดโ€˜๐‘—)))
7271, 65eqeltrd 2834 . . . . . . 7 (๐‘— โˆˆ โ„• โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„)
7363, 72syl 17 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„)
74 peano2nn 12170 . . . . . . . . . 10 (๐‘— โˆˆ โ„• โ†’ (๐‘— + 1) โˆˆ โ„•)
752stirlinglem2 44402 . . . . . . . . . . . 12 ((๐‘— + 1) โˆˆ โ„• โ†’ (๐ดโ€˜(๐‘— + 1)) โˆˆ โ„+)
7674, 75syl 17 . . . . . . . . . . 11 (๐‘— โˆˆ โ„• โ†’ (๐ดโ€˜(๐‘— + 1)) โˆˆ โ„+)
7776relogcld 25994 . . . . . . . . . 10 (๐‘— โˆˆ โ„• โ†’ (logโ€˜(๐ดโ€˜(๐‘— + 1))) โˆˆ โ„)
78 nfcv 2904 . . . . . . . . . . 11 โ„ฒ๐‘›(๐‘— + 1)
799, 78nffv 6853 . . . . . . . . . . . 12 โ„ฒ๐‘›(๐ดโ€˜(๐‘— + 1))
807, 79nffv 6853 . . . . . . . . . . 11 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜(๐‘— + 1)))
81 2fveq3 6848 . . . . . . . . . . 11 (๐‘› = (๐‘— + 1) โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜(๐‘— + 1))))
8278, 80, 81, 13fvmptf 6970 . . . . . . . . . 10 (((๐‘— + 1) โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜(๐‘— + 1))) โˆˆ โ„) โ†’ (๐ตโ€˜(๐‘— + 1)) = (logโ€˜(๐ดโ€˜(๐‘— + 1))))
8374, 77, 82syl2anc 585 . . . . . . . . 9 (๐‘— โˆˆ โ„• โ†’ (๐ตโ€˜(๐‘— + 1)) = (logโ€˜(๐ดโ€˜(๐‘— + 1))))
8483, 77eqeltrd 2834 . . . . . . . 8 (๐‘— โˆˆ โ„• โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
8562, 84syl 17 . . . . . . 7 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
8685adantl 483 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
8773, 86resubcld 11588 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ ((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โˆˆ โ„)
8861, 87fsumrecl 15624 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โˆˆ โ„)
8929a1i 11 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (1 / 4) โˆˆ โ„)
9062nnred 12173 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ ๐‘— โˆˆ โ„)
91 1red 11161 . . . . . . . . . 10 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ 1 โˆˆ โ„)
9290, 91readdcld 11189 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— + 1) โˆˆ โ„)
9390, 92remulcld 11190 . . . . . . . 8 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„)
9490recnd 11188 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ ๐‘— โˆˆ โ„‚)
95 1cnd 11155 . . . . . . . . . 10 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ 1 โˆˆ โ„‚)
9694, 95addcld 11179 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— + 1) โˆˆ โ„‚)
9762nnne0d 12208 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ ๐‘— โ‰  0)
9874nnne0d 12208 . . . . . . . . . 10 (๐‘— โˆˆ โ„• โ†’ (๐‘— + 1) โ‰  0)
9962, 98syl 17 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— + 1) โ‰  0)
10094, 96, 97, 99mulne0d 11812 . . . . . . . 8 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— ยท (๐‘— + 1)) โ‰  0)
10193, 100rereccld 11987 . . . . . . 7 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
102101adantl 483 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
10389, 102remulcld 11190 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ ((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))) โˆˆ โ„)
10461, 103fsumrecl 15624 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))) โˆˆ โ„)
105 eqid 2733 . . . . . . 7 (๐‘– โˆˆ โ„• โ†ฆ ((1 / ((2 ยท ๐‘–) + 1)) ยท ((1 / ((2 ยท ๐‘—) + 1))โ†‘(2 ยท ๐‘–)))) = (๐‘– โˆˆ โ„• โ†ฆ ((1 / ((2 ยท ๐‘–) + 1)) ยท ((1 / ((2 ยท ๐‘—) + 1))โ†‘(2 ยท ๐‘–))))
106 eqid 2733 . . . . . . 7 (๐‘– โˆˆ โ„• โ†ฆ ((1 / (((2 ยท ๐‘—) + 1)โ†‘2))โ†‘๐‘–)) = (๐‘– โˆˆ โ„• โ†ฆ ((1 / (((2 ยท ๐‘—) + 1)โ†‘2))โ†‘๐‘–))
1072, 13, 105, 106stirlinglem10 44410 . . . . . 6 (๐‘— โˆˆ โ„• โ†’ ((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โ‰ค ((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))))
10863, 107syl 17 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ ((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โ‰ค ((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))))
10961, 87, 103, 108fsumle 15689 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โ‰ค ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))))
11061, 102fsumrecl 15624 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
111 1red 11161 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„)
112 4pos 12265 . . . . . . . . 9 0 < 4
11327, 112elrpii 12923 . . . . . . . 8 4 โˆˆ โ„+
114113a1i 11 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 4 โˆˆ โ„+)
115 0red 11163 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 โˆˆ โ„)
116 0lt1 11682 . . . . . . . . 9 0 < 1
117116a1i 11 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 < 1)
118115, 111, 117ltled 11308 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค 1)
119111, 114, 118divge0d 13002 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค (1 / 4))
120 eqid 2733 . . . . . . . . . 10 (โ„คโ‰ฅโ€˜๐‘) = (โ„คโ‰ฅโ€˜๐‘)
121 eluznn 12848 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โˆˆ โ„•)
122 stirlinglem12.3 . . . . . . . . . . . . 13 ๐น = (๐‘› โˆˆ โ„• โ†ฆ (1 / (๐‘› ยท (๐‘› + 1))))
123122a1i 11 . . . . . . . . . . . 12 (๐‘— โˆˆ โ„• โ†’ ๐น = (๐‘› โˆˆ โ„• โ†ฆ (1 / (๐‘› ยท (๐‘› + 1)))))
124 simpr 486 . . . . . . . . . . . . . 14 ((๐‘— โˆˆ โ„• โˆง ๐‘› = ๐‘—) โ†’ ๐‘› = ๐‘—)
125124oveq1d 7373 . . . . . . . . . . . . . 14 ((๐‘— โˆˆ โ„• โˆง ๐‘› = ๐‘—) โ†’ (๐‘› + 1) = (๐‘— + 1))
126124, 125oveq12d 7376 . . . . . . . . . . . . 13 ((๐‘— โˆˆ โ„• โˆง ๐‘› = ๐‘—) โ†’ (๐‘› ยท (๐‘› + 1)) = (๐‘— ยท (๐‘— + 1)))
127126oveq2d 7374 . . . . . . . . . . . 12 ((๐‘— โˆˆ โ„• โˆง ๐‘› = ๐‘—) โ†’ (1 / (๐‘› ยท (๐‘› + 1))) = (1 / (๐‘— ยท (๐‘— + 1))))
128 id 22 . . . . . . . . . . . 12 (๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„•)
129 nnre 12165 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„)
130 1red 11161 . . . . . . . . . . . . . . 15 (๐‘— โˆˆ โ„• โ†’ 1 โˆˆ โ„)
131129, 130readdcld 11189 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ (๐‘— + 1) โˆˆ โ„)
132129, 131remulcld 11190 . . . . . . . . . . . . 13 (๐‘— โˆˆ โ„• โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„)
133 nncn 12166 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„‚)
134 1cnd 11155 . . . . . . . . . . . . . . 15 (๐‘— โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
135133, 134addcld 11179 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ (๐‘— + 1) โˆˆ โ„‚)
136 nnne0 12192 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ ๐‘— โ‰  0)
137133, 135, 136, 98mulne0d 11812 . . . . . . . . . . . . 13 (๐‘— โˆˆ โ„• โ†’ (๐‘— ยท (๐‘— + 1)) โ‰  0)
138132, 137rereccld 11987 . . . . . . . . . . . 12 (๐‘— โˆˆ โ„• โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
139123, 127, 128, 138fvmptd 6956 . . . . . . . . . . 11 (๐‘— โˆˆ โ„• โ†’ (๐นโ€˜๐‘—) = (1 / (๐‘— ยท (๐‘— + 1))))
140121, 139syl 17 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐นโ€˜๐‘—) = (1 / (๐‘— ยท (๐‘— + 1))))
141121nnred 12173 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โˆˆ โ„)
142 1red 11161 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 1 โˆˆ โ„)
143141, 142readdcld 11189 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— + 1) โˆˆ โ„)
144141, 143remulcld 11190 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„)
145141recnd 11188 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โˆˆ โ„‚)
146 1cnd 11155 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 1 โˆˆ โ„‚)
147145, 146addcld 11179 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— + 1) โˆˆ โ„‚)
148121nnne0d 12208 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โ‰  0)
149121, 98syl 17 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— + 1) โ‰  0)
150145, 147, 148, 149mulne0d 11812 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— ยท (๐‘— + 1)) โ‰  0)
151144, 150rereccld 11987 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
152 seqeq1 13915 . . . . . . . . . . . . 13 (๐‘ = 1 โ†’ seq๐‘( + , ๐น) = seq1( + , ๐น))
153122trireciplem 15752 . . . . . . . . . . . . . 14 seq1( + , ๐น) โ‡ 1
154 climrel 15380 . . . . . . . . . . . . . . 15 Rel โ‡
155154releldmi 5904 . . . . . . . . . . . . . 14 (seq1( + , ๐น) โ‡ 1 โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
156153, 155mp1i 13 . . . . . . . . . . . . 13 (๐‘ = 1 โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
157152, 156eqeltrd 2834 . . . . . . . . . . . 12 (๐‘ = 1 โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
158157adantl 483 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘ = 1) โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
159 simpl 484 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ ๐‘ โˆˆ โ„•)
160 simpr 486 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ ยฌ ๐‘ = 1)
161 elnn1uz2 12855 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ โ„• โ†” (๐‘ = 1 โˆจ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2)))
162159, 161sylib 217 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ (๐‘ = 1 โˆจ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2)))
163162ord 863 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ (ยฌ ๐‘ = 1 โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2)))
164160, 163mpd 15 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2))
165 uz2m1nn 12853 . . . . . . . . . . . . 13 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
166164, 165syl 17 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
167 nncn 12166 . . . . . . . . . . . . . . . . . 18 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚)
168167adantr 482 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„‚)
169 1cnd 11155 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ 1 โˆˆ โ„‚)
170168, 169npcand 11521 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ ((๐‘ โˆ’ 1) + 1) = ๐‘)
171170eqcomd 2739 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ ๐‘ = ((๐‘ โˆ’ 1) + 1))
172171seqeq1d 13918 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ seq๐‘( + , ๐น) = seq((๐‘ โˆ’ 1) + 1)( + , ๐น))
173 nnuz 12811 . . . . . . . . . . . . . . . 16 โ„• = (โ„คโ‰ฅโ€˜1)
174 id 22 . . . . . . . . . . . . . . . 16 ((๐‘ โˆ’ 1) โˆˆ โ„• โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
175138recnd 11188 . . . . . . . . . . . . . . . . . 18 (๐‘— โˆˆ โ„• โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
176139, 175eqeltrd 2834 . . . . . . . . . . . . . . . . 17 (๐‘— โˆˆ โ„• โ†’ (๐นโ€˜๐‘—) โˆˆ โ„‚)
177176adantl 483 . . . . . . . . . . . . . . . 16 (((๐‘ โˆ’ 1) โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐นโ€˜๐‘—) โˆˆ โ„‚)
178153a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘ โˆ’ 1) โˆˆ โ„• โ†’ seq1( + , ๐น) โ‡ 1)
179173, 174, 177, 178clim2ser 15545 . . . . . . . . . . . . . . 15 ((๐‘ โˆ’ 1) โˆˆ โ„• โ†’ seq((๐‘ โˆ’ 1) + 1)( + , ๐น) โ‡ (1 โˆ’ (seq1( + , ๐น)โ€˜(๐‘ โˆ’ 1))))
180179adantl 483 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ seq((๐‘ โˆ’ 1) + 1)( + , ๐น) โ‡ (1 โˆ’ (seq1( + , ๐น)โ€˜(๐‘ โˆ’ 1))))
181172, 180eqbrtrd 5128 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ seq๐‘( + , ๐น) โ‡ (1 โˆ’ (seq1( + , ๐น)โ€˜(๐‘ โˆ’ 1))))
182154releldmi 5904 . . . . . . . . . . . . 13 (seq๐‘( + , ๐น) โ‡ (1 โˆ’ (seq1( + , ๐น)โ€˜(๐‘ โˆ’ 1))) โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
183181, 182syl 17 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
184159, 166, 183syl2anc 585 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
185158, 184pm2.61dan 812 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
186120, 56, 140, 151, 185isumrecl 15655 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)(1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
187121nnrpd 12960 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โˆˆ โ„+)
188187rpge0d 12966 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 0 โ‰ค ๐‘—)
189141, 188ge0p1rpd 12992 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— + 1) โˆˆ โ„+)
190187, 189rpmulcld 12978 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„+)
191118adantr 482 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 0 โ‰ค 1)
192142, 190, 191divge0d 13002 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 0 โ‰ค (1 / (๐‘— ยท (๐‘— + 1))))
193120, 56, 140, 151, 185, 192isumge0 15656 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ฮฃ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)(1 / (๐‘— ยท (๐‘— + 1))))
194115, 186, 110, 193leadd2dd 11775 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + 0) โ‰ค (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + ฮฃ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)(1 / (๐‘— ยท (๐‘— + 1)))))
195110recnd 11188 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
196195addid1d 11360 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + 0) = ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))))
197196eqcomd 2739 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) = (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + 0))
198 id 22 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•)
199139adantl 483 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐นโ€˜๐‘—) = (1 / (๐‘— ยท (๐‘— + 1))))
200133adantl 483 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ ๐‘— โˆˆ โ„‚)
201 1cnd 11155 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ 1 โˆˆ โ„‚)
202200, 201addcld 11179 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐‘— + 1) โˆˆ โ„‚)
203200, 202mulcld 11180 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„‚)
204136adantl 483 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ ๐‘— โ‰  0)
20598adantl 483 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐‘— + 1) โ‰  0)
206200, 202, 204, 205mulne0d 11812 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐‘— ยท (๐‘— + 1)) โ‰  0)
207203, 206reccld 11929 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
208153, 155mp1i 13 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
209173, 120, 198, 199, 207, 208isumsplit 15730 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ โ„• (1 / (๐‘— ยท (๐‘— + 1))) = (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + ฮฃ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)(1 / (๐‘— ยท (๐‘— + 1)))))
210194, 197, 2093brtr4d 5138 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) โ‰ค ฮฃ๐‘— โˆˆ โ„• (1 / (๐‘— ยท (๐‘— + 1))))
211 1zzd 12539 . . . . . . . . 9 (โŠค โ†’ 1 โˆˆ โ„ค)
212139adantl 483 . . . . . . . . 9 ((โŠค โˆง ๐‘— โˆˆ โ„•) โ†’ (๐นโ€˜๐‘—) = (1 / (๐‘— ยท (๐‘— + 1))))
213175adantl 483 . . . . . . . . 9 ((โŠค โˆง ๐‘— โˆˆ โ„•) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
214153a1i 11 . . . . . . . . 9 (โŠค โ†’ seq1( + , ๐น) โ‡ 1)
215173, 211, 212, 213, 214isumclim 15647 . . . . . . . 8 (โŠค โ†’ ฮฃ๐‘— โˆˆ โ„• (1 / (๐‘— ยท (๐‘— + 1))) = 1)
216215mptru 1549 . . . . . . 7 ฮฃ๐‘— โˆˆ โ„• (1 / (๐‘— ยท (๐‘— + 1))) = 1
217210, 216breqtrdi 5147 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) โ‰ค 1)
218110, 111, 30, 119, 217lemul2ad 12100 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 / 4) ยท ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1)))) โ‰ค ((1 / 4) ยท 1))
219 4cn 12243 . . . . . . . 8 4 โˆˆ โ„‚
220219a1i 11 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 4 โˆˆ โ„‚)
221112a1i 11 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 < 4)
222221gt0ne0d 11724 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 4 โ‰  0)
223220, 222reccld 11929 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (1 / 4) โˆˆ โ„‚)
224102recnd 11188 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
22561, 223, 224fsummulc2 15674 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 / 4) ยท ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1)))) = ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))))
226223mulid1d 11177 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 / 4) ยท 1) = (1 / 4))
227218, 225, 2263brtr3d 5137 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))) โ‰ค (1 / 4))
22888, 104, 30, 109, 227letrd 11317 . . 3 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โ‰ค (1 / 4))
22960, 228eqbrtrd 5128 . 2 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜1) โˆ’ (๐ตโ€˜๐‘)) โ‰ค (1 / 4))
23017, 26, 30, 229subled 11763 1 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜1) โˆ’ (1 / 4)) โ‰ค (๐ตโ€˜๐‘))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 397   โˆจ wo 846   = wceq 1542  โŠคwtru 1543   โˆˆ wcel 2107   โ‰  wne 2940   class class class wbr 5106   โ†ฆ cmpt 5189  dom cdm 5634  โ€˜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   / cdiv 11817  โ„•cn 12158  2c2 12213  4c4 12215  โ„คcz 12504  โ„คโ‰ฅcuz 12768  โ„+crp 12920  ...cfz 13430  ..^cfzo 13573  seqcseq 13912  โ†‘cexp 13973  !cfa 14179  โˆšcsqrt 15124   โ‡ cli 15372  ฮฃcsu 15576  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:  stirlinglem13  44413
  Copyright terms: Public domain W3C validator