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 45396
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 12245 . . . . 5 1 โˆˆ โ„•
2 stirlinglem12.1 . . . . . . 7 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
32stirlinglem2 45386 . . . . . 6 (1 โˆˆ โ„• โ†’ (๐ดโ€˜1) โˆˆ โ„+)
4 relogcl 26496 . . . . . 6 ((๐ดโ€˜1) โˆˆ โ„+ โ†’ (logโ€˜(๐ดโ€˜1)) โˆˆ โ„)
51, 3, 4mp2b 10 . . . . 5 (logโ€˜(๐ดโ€˜1)) โˆˆ โ„
6 nfcv 2898 . . . . . 6 โ„ฒ๐‘›1
7 nfcv 2898 . . . . . . 7 โ„ฒ๐‘›log
8 nfmpt1 5250 . . . . . . . . 9 โ„ฒ๐‘›(๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
92, 8nfcxfr 2896 . . . . . . . 8 โ„ฒ๐‘›๐ด
109, 6nffv 6901 . . . . . . 7 โ„ฒ๐‘›(๐ดโ€˜1)
117, 10nffv 6901 . . . . . 6 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜1))
12 2fveq3 6896 . . . . . 6 (๐‘› = 1 โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜1)))
13 stirlinglem12.2 . . . . . 6 ๐ต = (๐‘› โˆˆ โ„• โ†ฆ (logโ€˜(๐ดโ€˜๐‘›)))
146, 11, 12, 13fvmptf 7020 . . . . 5 ((1 โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜1)) โˆˆ โ„) โ†’ (๐ตโ€˜1) = (logโ€˜(๐ดโ€˜1)))
151, 5, 14mp2an 691 . . . 4 (๐ตโ€˜1) = (logโ€˜(๐ดโ€˜1))
1615, 5eqeltri 2824 . . 3 (๐ตโ€˜1) โˆˆ โ„
1716a1i 11 . 2 (๐‘ โˆˆ โ„• โ†’ (๐ตโ€˜1) โˆˆ โ„)
182stirlinglem2 45386 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (๐ดโ€˜๐‘) โˆˆ โ„+)
1918relogcld 26544 . . . 4 (๐‘ โˆˆ โ„• โ†’ (logโ€˜(๐ดโ€˜๐‘)) โˆˆ โ„)
20 nfcv 2898 . . . . 5 โ„ฒ๐‘›๐‘
219, 20nffv 6901 . . . . . 6 โ„ฒ๐‘›(๐ดโ€˜๐‘)
227, 21nffv 6901 . . . . 5 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜๐‘))
23 2fveq3 6896 . . . . 5 (๐‘› = ๐‘ โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜๐‘)))
2420, 22, 23, 13fvmptf 7020 . . . 4 ((๐‘ โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜๐‘)) โˆˆ โ„) โ†’ (๐ตโ€˜๐‘) = (logโ€˜(๐ดโ€˜๐‘)))
2519, 24mpdan 686 . . 3 (๐‘ โˆˆ โ„• โ†’ (๐ตโ€˜๐‘) = (logโ€˜(๐ดโ€˜๐‘)))
2625, 19eqeltrd 2828 . 2 (๐‘ โˆˆ โ„• โ†’ (๐ตโ€˜๐‘) โˆˆ โ„)
27 4re 12318 . . . 4 4 โˆˆ โ„
28 4ne0 12342 . . . 4 4 โ‰  0
2927, 28rereccli 12001 . . 3 (1 / 4) โˆˆ โ„
3029a1i 11 . 2 (๐‘ โˆˆ โ„• โ†’ (1 / 4) โˆˆ โ„)
31 fveq2 6891 . . . . 5 (๐‘˜ = ๐‘— โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜๐‘—))
32 fveq2 6891 . . . . 5 (๐‘˜ = (๐‘— + 1) โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜(๐‘— + 1)))
33 fveq2 6891 . . . . 5 (๐‘˜ = 1 โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜1))
34 fveq2 6891 . . . . 5 (๐‘˜ = ๐‘ โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜๐‘))
35 elnnuz 12888 . . . . . 6 (๐‘ โˆˆ โ„• โ†” ๐‘ โˆˆ (โ„คโ‰ฅโ€˜1))
3635biimpi 215 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜1))
37 elfznn 13554 . . . . . . . 8 (๐‘˜ โˆˆ (1...๐‘) โ†’ ๐‘˜ โˆˆ โ„•)
382stirlinglem2 45386 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (๐ดโ€˜๐‘˜) โˆˆ โ„+)
3937, 38syl 17 . . . . . . . . 9 (๐‘˜ โˆˆ (1...๐‘) โ†’ (๐ดโ€˜๐‘˜) โˆˆ โ„+)
4039relogcld 26544 . . . . . . . 8 (๐‘˜ โˆˆ (1...๐‘) โ†’ (logโ€˜(๐ดโ€˜๐‘˜)) โˆˆ โ„)
41 nfcv 2898 . . . . . . . . 9 โ„ฒ๐‘›๐‘˜
429, 41nffv 6901 . . . . . . . . . 10 โ„ฒ๐‘›(๐ดโ€˜๐‘˜)
437, 42nffv 6901 . . . . . . . . 9 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜๐‘˜))
44 2fveq3 6896 . . . . . . . . 9 (๐‘› = ๐‘˜ โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜๐‘˜)))
4541, 43, 44, 13fvmptf 7020 . . . . . . . 8 ((๐‘˜ โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜๐‘˜)) โˆˆ โ„) โ†’ (๐ตโ€˜๐‘˜) = (logโ€˜(๐ดโ€˜๐‘˜)))
4637, 40, 45syl2anc 583 . . . . . . 7 (๐‘˜ โˆˆ (1...๐‘) โ†’ (๐ตโ€˜๐‘˜) = (logโ€˜(๐ดโ€˜๐‘˜)))
4746adantl 481 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘˜) = (logโ€˜(๐ดโ€˜๐‘˜)))
4839rpcnd 13042 . . . . . . . 8 (๐‘˜ โˆˆ (1...๐‘) โ†’ (๐ดโ€˜๐‘˜) โˆˆ โ„‚)
4948adantl 481 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘˜) โˆˆ โ„‚)
5038rpne0d 13045 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (๐ดโ€˜๐‘˜) โ‰  0)
5137, 50syl 17 . . . . . . . 8 (๐‘˜ โˆˆ (1...๐‘) โ†’ (๐ดโ€˜๐‘˜) โ‰  0)
5251adantl 481 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘˜) โ‰  0)
5349, 52logcld 26491 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (logโ€˜(๐ดโ€˜๐‘˜)) โˆˆ โ„‚)
5447, 53eqeltrd 2828 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘˜) โˆˆ โ„‚)
5531, 32, 33, 34, 36, 54telfsumo 15772 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1..^๐‘)((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) = ((๐ตโ€˜1) โˆ’ (๐ตโ€˜๐‘)))
56 nnz 12601 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ค)
57 fzoval 13657 . . . . . 6 (๐‘ โˆˆ โ„ค โ†’ (1..^๐‘) = (1...(๐‘ โˆ’ 1)))
5856, 57syl 17 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (1..^๐‘) = (1...(๐‘ โˆ’ 1)))
5958sumeq1d 15671 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1..^๐‘)((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) = ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))))
6055, 59eqtr3d 2769 . . 3 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜1) โˆ’ (๐ตโ€˜๐‘)) = ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))))
61 fzfid 13962 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (1...(๐‘ โˆ’ 1)) โˆˆ Fin)
62 elfznn 13554 . . . . . . . 8 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ ๐‘— โˆˆ โ„•)
6362adantl 481 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ ๐‘— โˆˆ โ„•)
642stirlinglem2 45386 . . . . . . . . . 10 (๐‘— โˆˆ โ„• โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„+)
6564relogcld 26544 . . . . . . . . 9 (๐‘— โˆˆ โ„• โ†’ (logโ€˜(๐ดโ€˜๐‘—)) โˆˆ โ„)
66 nfcv 2898 . . . . . . . . . 10 โ„ฒ๐‘›๐‘—
679, 66nffv 6901 . . . . . . . . . . 11 โ„ฒ๐‘›(๐ดโ€˜๐‘—)
687, 67nffv 6901 . . . . . . . . . 10 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜๐‘—))
69 2fveq3 6896 . . . . . . . . . 10 (๐‘› = ๐‘— โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜๐‘—)))
7066, 68, 69, 13fvmptf 7020 . . . . . . . . 9 ((๐‘— โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜๐‘—)) โˆˆ โ„) โ†’ (๐ตโ€˜๐‘—) = (logโ€˜(๐ดโ€˜๐‘—)))
7165, 70mpdan 686 . . . . . . . 8 (๐‘— โˆˆ โ„• โ†’ (๐ตโ€˜๐‘—) = (logโ€˜(๐ดโ€˜๐‘—)))
7271, 65eqeltrd 2828 . . . . . . 7 (๐‘— โˆˆ โ„• โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„)
7363, 72syl 17 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„)
74 peano2nn 12246 . . . . . . . . . 10 (๐‘— โˆˆ โ„• โ†’ (๐‘— + 1) โˆˆ โ„•)
752stirlinglem2 45386 . . . . . . . . . . . 12 ((๐‘— + 1) โˆˆ โ„• โ†’ (๐ดโ€˜(๐‘— + 1)) โˆˆ โ„+)
7674, 75syl 17 . . . . . . . . . . 11 (๐‘— โˆˆ โ„• โ†’ (๐ดโ€˜(๐‘— + 1)) โˆˆ โ„+)
7776relogcld 26544 . . . . . . . . . 10 (๐‘— โˆˆ โ„• โ†’ (logโ€˜(๐ดโ€˜(๐‘— + 1))) โˆˆ โ„)
78 nfcv 2898 . . . . . . . . . . 11 โ„ฒ๐‘›(๐‘— + 1)
799, 78nffv 6901 . . . . . . . . . . . 12 โ„ฒ๐‘›(๐ดโ€˜(๐‘— + 1))
807, 79nffv 6901 . . . . . . . . . . 11 โ„ฒ๐‘›(logโ€˜(๐ดโ€˜(๐‘— + 1)))
81 2fveq3 6896 . . . . . . . . . . 11 (๐‘› = (๐‘— + 1) โ†’ (logโ€˜(๐ดโ€˜๐‘›)) = (logโ€˜(๐ดโ€˜(๐‘— + 1))))
8278, 80, 81, 13fvmptf 7020 . . . . . . . . . 10 (((๐‘— + 1) โˆˆ โ„• โˆง (logโ€˜(๐ดโ€˜(๐‘— + 1))) โˆˆ โ„) โ†’ (๐ตโ€˜(๐‘— + 1)) = (logโ€˜(๐ดโ€˜(๐‘— + 1))))
8374, 77, 82syl2anc 583 . . . . . . . . 9 (๐‘— โˆˆ โ„• โ†’ (๐ตโ€˜(๐‘— + 1)) = (logโ€˜(๐ดโ€˜(๐‘— + 1))))
8483, 77eqeltrd 2828 . . . . . . . 8 (๐‘— โˆˆ โ„• โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
8562, 84syl 17 . . . . . . 7 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
8685adantl 481 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (๐ตโ€˜(๐‘— + 1)) โˆˆ โ„)
8773, 86resubcld 11664 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ ((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โˆˆ โ„)
8861, 87fsumrecl 15704 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โˆˆ โ„)
8929a1i 11 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (1 / 4) โˆˆ โ„)
9062nnred 12249 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ ๐‘— โˆˆ โ„)
91 1red 11237 . . . . . . . . . 10 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ 1 โˆˆ โ„)
9290, 91readdcld 11265 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— + 1) โˆˆ โ„)
9390, 92remulcld 11266 . . . . . . . 8 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„)
9490recnd 11264 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ ๐‘— โˆˆ โ„‚)
95 1cnd 11231 . . . . . . . . . 10 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ 1 โˆˆ โ„‚)
9694, 95addcld 11255 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— + 1) โˆˆ โ„‚)
9762nnne0d 12284 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ ๐‘— โ‰  0)
9874nnne0d 12284 . . . . . . . . . 10 (๐‘— โˆˆ โ„• โ†’ (๐‘— + 1) โ‰  0)
9962, 98syl 17 . . . . . . . . 9 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— + 1) โ‰  0)
10094, 96, 97, 99mulne0d 11888 . . . . . . . 8 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (๐‘— ยท (๐‘— + 1)) โ‰  0)
10193, 100rereccld 12063 . . . . . . 7 (๐‘— โˆˆ (1...(๐‘ โˆ’ 1)) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
102101adantl 481 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
10389, 102remulcld 11266 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ ((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))) โˆˆ โ„)
10461, 103fsumrecl 15704 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))) โˆˆ โ„)
105 eqid 2727 . . . . . . 7 (๐‘– โˆˆ โ„• โ†ฆ ((1 / ((2 ยท ๐‘–) + 1)) ยท ((1 / ((2 ยท ๐‘—) + 1))โ†‘(2 ยท ๐‘–)))) = (๐‘– โˆˆ โ„• โ†ฆ ((1 / ((2 ยท ๐‘–) + 1)) ยท ((1 / ((2 ยท ๐‘—) + 1))โ†‘(2 ยท ๐‘–))))
106 eqid 2727 . . . . . . 7 (๐‘– โˆˆ โ„• โ†ฆ ((1 / (((2 ยท ๐‘—) + 1)โ†‘2))โ†‘๐‘–)) = (๐‘– โˆˆ โ„• โ†ฆ ((1 / (((2 ยท ๐‘—) + 1)โ†‘2))โ†‘๐‘–))
1072, 13, 105, 106stirlinglem10 45394 . . . . . 6 (๐‘— โˆˆ โ„• โ†’ ((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โ‰ค ((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))))
10863, 107syl 17 . . . . 5 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ ((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โ‰ค ((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))))
10961, 87, 103, 108fsumle 15769 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โ‰ค ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))))
11061, 102fsumrecl 15704 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
111 1red 11237 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„)
112 4pos 12341 . . . . . . . . 9 0 < 4
11327, 112elrpii 13001 . . . . . . . 8 4 โˆˆ โ„+
114113a1i 11 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 4 โˆˆ โ„+)
115 0red 11239 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 โˆˆ โ„)
116 0lt1 11758 . . . . . . . . 9 0 < 1
117116a1i 11 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 < 1)
118115, 111, 117ltled 11384 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค 1)
119111, 114, 118divge0d 13080 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค (1 / 4))
120 eqid 2727 . . . . . . . . . 10 (โ„คโ‰ฅโ€˜๐‘) = (โ„คโ‰ฅโ€˜๐‘)
121 eluznn 12924 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โˆˆ โ„•)
122 stirlinglem12.3 . . . . . . . . . . . . 13 ๐น = (๐‘› โˆˆ โ„• โ†ฆ (1 / (๐‘› ยท (๐‘› + 1))))
123122a1i 11 . . . . . . . . . . . 12 (๐‘— โˆˆ โ„• โ†’ ๐น = (๐‘› โˆˆ โ„• โ†ฆ (1 / (๐‘› ยท (๐‘› + 1)))))
124 simpr 484 . . . . . . . . . . . . . 14 ((๐‘— โˆˆ โ„• โˆง ๐‘› = ๐‘—) โ†’ ๐‘› = ๐‘—)
125124oveq1d 7429 . . . . . . . . . . . . . 14 ((๐‘— โˆˆ โ„• โˆง ๐‘› = ๐‘—) โ†’ (๐‘› + 1) = (๐‘— + 1))
126124, 125oveq12d 7432 . . . . . . . . . . . . 13 ((๐‘— โˆˆ โ„• โˆง ๐‘› = ๐‘—) โ†’ (๐‘› ยท (๐‘› + 1)) = (๐‘— ยท (๐‘— + 1)))
127126oveq2d 7430 . . . . . . . . . . . 12 ((๐‘— โˆˆ โ„• โˆง ๐‘› = ๐‘—) โ†’ (1 / (๐‘› ยท (๐‘› + 1))) = (1 / (๐‘— ยท (๐‘— + 1))))
128 id 22 . . . . . . . . . . . 12 (๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„•)
129 nnre 12241 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„)
130 1red 11237 . . . . . . . . . . . . . . 15 (๐‘— โˆˆ โ„• โ†’ 1 โˆˆ โ„)
131129, 130readdcld 11265 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ (๐‘— + 1) โˆˆ โ„)
132129, 131remulcld 11266 . . . . . . . . . . . . 13 (๐‘— โˆˆ โ„• โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„)
133 nncn 12242 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„‚)
134 1cnd 11231 . . . . . . . . . . . . . . 15 (๐‘— โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
135133, 134addcld 11255 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ (๐‘— + 1) โˆˆ โ„‚)
136 nnne0 12268 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†’ ๐‘— โ‰  0)
137133, 135, 136, 98mulne0d 11888 . . . . . . . . . . . . 13 (๐‘— โˆˆ โ„• โ†’ (๐‘— ยท (๐‘— + 1)) โ‰  0)
138132, 137rereccld 12063 . . . . . . . . . . . 12 (๐‘— โˆˆ โ„• โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
139123, 127, 128, 138fvmptd 7006 . . . . . . . . . . 11 (๐‘— โˆˆ โ„• โ†’ (๐นโ€˜๐‘—) = (1 / (๐‘— ยท (๐‘— + 1))))
140121, 139syl 17 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐นโ€˜๐‘—) = (1 / (๐‘— ยท (๐‘— + 1))))
141121nnred 12249 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โˆˆ โ„)
142 1red 11237 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 1 โˆˆ โ„)
143141, 142readdcld 11265 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— + 1) โˆˆ โ„)
144141, 143remulcld 11266 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„)
145141recnd 11264 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โˆˆ โ„‚)
146 1cnd 11231 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 1 โˆˆ โ„‚)
147145, 146addcld 11255 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— + 1) โˆˆ โ„‚)
148121nnne0d 12284 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โ‰  0)
149121, 98syl 17 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— + 1) โ‰  0)
150145, 147, 148, 149mulne0d 11888 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— ยท (๐‘— + 1)) โ‰  0)
151144, 150rereccld 12063 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
152 seqeq1 13993 . . . . . . . . . . . . 13 (๐‘ = 1 โ†’ seq๐‘( + , ๐น) = seq1( + , ๐น))
153122trireciplem 15832 . . . . . . . . . . . . . 14 seq1( + , ๐น) โ‡ 1
154 climrel 15460 . . . . . . . . . . . . . . 15 Rel โ‡
155154releldmi 5944 . . . . . . . . . . . . . 14 (seq1( + , ๐น) โ‡ 1 โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
156153, 155mp1i 13 . . . . . . . . . . . . 13 (๐‘ = 1 โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
157152, 156eqeltrd 2828 . . . . . . . . . . . 12 (๐‘ = 1 โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
158157adantl 481 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘ = 1) โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
159 simpl 482 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ ๐‘ โˆˆ โ„•)
160 simpr 484 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ ยฌ ๐‘ = 1)
161 elnn1uz2 12931 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ โ„• โ†” (๐‘ = 1 โˆจ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2)))
162159, 161sylib 217 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ (๐‘ = 1 โˆจ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2)))
163162ord 863 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ (ยฌ ๐‘ = 1 โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2)))
164160, 163mpd 15 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜2))
165 uz2m1nn 12929 . . . . . . . . . . . . 13 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
166164, 165syl 17 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
167 nncn 12242 . . . . . . . . . . . . . . . . . 18 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚)
168167adantr 480 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„‚)
169 1cnd 11231 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ 1 โˆˆ โ„‚)
170168, 169npcand 11597 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ ((๐‘ โˆ’ 1) + 1) = ๐‘)
171170eqcomd 2733 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ ๐‘ = ((๐‘ โˆ’ 1) + 1))
172171seqeq1d 13996 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ seq๐‘( + , ๐น) = seq((๐‘ โˆ’ 1) + 1)( + , ๐น))
173 nnuz 12887 . . . . . . . . . . . . . . . 16 โ„• = (โ„คโ‰ฅโ€˜1)
174 id 22 . . . . . . . . . . . . . . . 16 ((๐‘ โˆ’ 1) โˆˆ โ„• โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•)
175138recnd 11264 . . . . . . . . . . . . . . . . . 18 (๐‘— โˆˆ โ„• โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
176139, 175eqeltrd 2828 . . . . . . . . . . . . . . . . 17 (๐‘— โˆˆ โ„• โ†’ (๐นโ€˜๐‘—) โˆˆ โ„‚)
177176adantl 481 . . . . . . . . . . . . . . . 16 (((๐‘ โˆ’ 1) โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐นโ€˜๐‘—) โˆˆ โ„‚)
178153a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘ โˆ’ 1) โˆˆ โ„• โ†’ seq1( + , ๐น) โ‡ 1)
179173, 174, 177, 178clim2ser 15625 . . . . . . . . . . . . . . 15 ((๐‘ โˆ’ 1) โˆˆ โ„• โ†’ seq((๐‘ โˆ’ 1) + 1)( + , ๐น) โ‡ (1 โˆ’ (seq1( + , ๐น)โ€˜(๐‘ โˆ’ 1))))
180179adantl 481 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ seq((๐‘ โˆ’ 1) + 1)( + , ๐น) โ‡ (1 โˆ’ (seq1( + , ๐น)โ€˜(๐‘ โˆ’ 1))))
181172, 180eqbrtrd 5164 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ seq๐‘( + , ๐น) โ‡ (1 โˆ’ (seq1( + , ๐น)โ€˜(๐‘ โˆ’ 1))))
182154releldmi 5944 . . . . . . . . . . . . 13 (seq๐‘( + , ๐น) โ‡ (1 โˆ’ (seq1( + , ๐น)โ€˜(๐‘ โˆ’ 1))) โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
183181, 182syl 17 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง (๐‘ โˆ’ 1) โˆˆ โ„•) โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
184159, 166, 183syl2anc 583 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ยฌ ๐‘ = 1) โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
185158, 184pm2.61dan 812 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ seq๐‘( + , ๐น) โˆˆ dom โ‡ )
186120, 56, 140, 151, 185isumrecl 15735 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)(1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„)
187121nnrpd 13038 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ ๐‘— โˆˆ โ„+)
188187rpge0d 13044 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 0 โ‰ค ๐‘—)
189141, 188ge0p1rpd 13070 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— + 1) โˆˆ โ„+)
190187, 189rpmulcld 13056 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„+)
191118adantr 480 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 0 โ‰ค 1)
192142, 190, 191divge0d 13080 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)) โ†’ 0 โ‰ค (1 / (๐‘— ยท (๐‘— + 1))))
193120, 56, 140, 151, 185, 192isumge0 15736 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ฮฃ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)(1 / (๐‘— ยท (๐‘— + 1))))
194115, 186, 110, 193leadd2dd 11851 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + 0) โ‰ค (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + ฮฃ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)(1 / (๐‘— ยท (๐‘— + 1)))))
195110recnd 11264 . . . . . . . . . 10 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
196195addridd 11436 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + 0) = ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))))
197196eqcomd 2733 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) = (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + 0))
198 id 22 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•)
199139adantl 481 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐นโ€˜๐‘—) = (1 / (๐‘— ยท (๐‘— + 1))))
200133adantl 481 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ ๐‘— โˆˆ โ„‚)
201 1cnd 11231 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ 1 โˆˆ โ„‚)
202200, 201addcld 11255 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐‘— + 1) โˆˆ โ„‚)
203200, 202mulcld 11256 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐‘— ยท (๐‘— + 1)) โˆˆ โ„‚)
204136adantl 481 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ ๐‘— โ‰  0)
20598adantl 481 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐‘— + 1) โ‰  0)
206200, 202, 204, 205mulne0d 11888 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (๐‘— ยท (๐‘— + 1)) โ‰  0)
207203, 206reccld 12005 . . . . . . . . 9 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
208153, 155mp1i 13 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
209173, 120, 198, 199, 207, 208isumsplit 15810 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ โ„• (1 / (๐‘— ยท (๐‘— + 1))) = (ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) + ฮฃ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘)(1 / (๐‘— ยท (๐‘— + 1)))))
210194, 197, 2093brtr4d 5174 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) โ‰ค ฮฃ๐‘— โˆˆ โ„• (1 / (๐‘— ยท (๐‘— + 1))))
211 1zzd 12615 . . . . . . . . 9 (โŠค โ†’ 1 โˆˆ โ„ค)
212139adantl 481 . . . . . . . . 9 ((โŠค โˆง ๐‘— โˆˆ โ„•) โ†’ (๐นโ€˜๐‘—) = (1 / (๐‘— ยท (๐‘— + 1))))
213175adantl 481 . . . . . . . . 9 ((โŠค โˆง ๐‘— โˆˆ โ„•) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
214153a1i 11 . . . . . . . . 9 (โŠค โ†’ seq1( + , ๐น) โ‡ 1)
215173, 211, 212, 213, 214isumclim 15727 . . . . . . . 8 (โŠค โ†’ ฮฃ๐‘— โˆˆ โ„• (1 / (๐‘— ยท (๐‘— + 1))) = 1)
216215mptru 1541 . . . . . . 7 ฮฃ๐‘— โˆˆ โ„• (1 / (๐‘— ยท (๐‘— + 1))) = 1
217210, 216breqtrdi 5183 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1))) โ‰ค 1)
218110, 111, 30, 119, 217lemul2ad 12176 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 / 4) ยท ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1)))) โ‰ค ((1 / 4) ยท 1))
219 4cn 12319 . . . . . . . 8 4 โˆˆ โ„‚
220219a1i 11 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 4 โˆˆ โ„‚)
221112a1i 11 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ 0 < 4)
222221gt0ne0d 11800 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 4 โ‰  0)
223220, 222reccld 12005 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ (1 / 4) โˆˆ โ„‚)
224102recnd 11264 . . . . . 6 ((๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))) โ†’ (1 / (๐‘— ยท (๐‘— + 1))) โˆˆ โ„‚)
22561, 223, 224fsummulc2 15754 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 / 4) ยท ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))(1 / (๐‘— ยท (๐‘— + 1)))) = ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))))
226223mulridd 11253 . . . . 5 (๐‘ โˆˆ โ„• โ†’ ((1 / 4) ยท 1) = (1 / 4))
227218, 225, 2263brtr3d 5173 . . . 4 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((1 / 4) ยท (1 / (๐‘— ยท (๐‘— + 1)))) โ‰ค (1 / 4))
22888, 104, 30, 109, 227letrd 11393 . . 3 (๐‘ โˆˆ โ„• โ†’ ฮฃ๐‘— โˆˆ (1...(๐‘ โˆ’ 1))((๐ตโ€˜๐‘—) โˆ’ (๐ตโ€˜(๐‘— + 1))) โ‰ค (1 / 4))
22960, 228eqbrtrd 5164 . 2 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜1) โˆ’ (๐ตโ€˜๐‘)) โ‰ค (1 / 4))
23017, 26, 30, 229subled 11839 1 (๐‘ โˆˆ โ„• โ†’ ((๐ตโ€˜1) โˆ’ (1 / 4)) โ‰ค (๐ตโ€˜๐‘))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 395   โˆจ wo 846   = wceq 1534  โŠคwtru 1535   โˆˆ wcel 2099   โ‰  wne 2935   class class class wbr 5142   โ†ฆ cmpt 5225  dom cdm 5672  โ€˜cfv 6542  (class class class)co 7414  โ„‚cc 11128  โ„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   ยท cmul 11135   < clt 11270   โ‰ค cle 11271   โˆ’ cmin 11466   / cdiv 11893  โ„•cn 12234  2c2 12289  4c4 12291  โ„คcz 12580  โ„คโ‰ฅcuz 12844  โ„+crp 12998  ...cfz 13508  ..^cfzo 13651  seqcseq 13990  โ†‘cexp 14050  !cfa 14256  โˆšcsqrt 15204   โ‡ cli 15452  ฮฃcsu 15656  eceu 16030  logclog 26475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-xnn0 12567  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ioc 13353  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-fac 14257  df-bc 14286  df-hash 14314  df-shft 15038  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-limsup 15439  df-clim 15456  df-rlim 15457  df-sum 15657  df-ef 16035  df-e 16036  df-sin 16037  df-cos 16038  df-tan 16039  df-pi 16040  df-dvds 16223  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-haus 23206  df-cmp 23278  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-limc 25782  df-dv 25783  df-ulm 26300  df-log 26477  df-cxp 26478
This theorem is referenced by:  stirlinglem13  45397
  Copyright terms: Public domain W3C validator