Metamath Proof Explorer


Theorem stirlinglem11

Description: B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem11.1 โŠข ๐ด = ( ๐‘› โˆˆ โ„• โ†ฆ ( ( ! โ€˜ ๐‘› ) / ( ( โˆš โ€˜ ( 2 ยท ๐‘› ) ) ยท ( ( ๐‘› / e ) โ†‘ ๐‘› ) ) ) )
stirlinglem11.2 โŠข ๐ต = ( ๐‘› โˆˆ โ„• โ†ฆ ( log โ€˜ ( ๐ด โ€˜ ๐‘› ) ) )
stirlinglem11.3 โŠข ๐พ = ( ๐‘˜ โˆˆ โ„• โ†ฆ ( ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) ) )
Assertion stirlinglem11 ( ๐‘ โˆˆ โ„• โ†’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) < ( ๐ต โ€˜ ๐‘ ) )

Proof

Step Hyp Ref Expression
1 stirlinglem11.1 โŠข ๐ด = ( ๐‘› โˆˆ โ„• โ†ฆ ( ( ! โ€˜ ๐‘› ) / ( ( โˆš โ€˜ ( 2 ยท ๐‘› ) ) ยท ( ( ๐‘› / e ) โ†‘ ๐‘› ) ) ) )
2 stirlinglem11.2 โŠข ๐ต = ( ๐‘› โˆˆ โ„• โ†ฆ ( log โ€˜ ( ๐ด โ€˜ ๐‘› ) ) )
3 stirlinglem11.3 โŠข ๐พ = ( ๐‘˜ โˆˆ โ„• โ†ฆ ( ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) ) )
4 0red โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โˆˆ โ„ )
5 3 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐พ = ( ๐‘˜ โˆˆ โ„• โ†ฆ ( ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) ) ) )
6 simpr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘˜ = 1 ) โ†’ ๐‘˜ = 1 )
7 6 oveq2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘˜ = 1 ) โ†’ ( 2 ยท ๐‘˜ ) = ( 2 ยท 1 ) )
8 7 oveq1d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘˜ = 1 ) โ†’ ( ( 2 ยท ๐‘˜ ) + 1 ) = ( ( 2 ยท 1 ) + 1 ) )
9 8 oveq2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘˜ = 1 ) โ†’ ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) = ( 1 / ( ( 2 ยท 1 ) + 1 ) ) )
10 7 oveq2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘˜ = 1 ) โ†’ ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) = ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) )
11 9 10 oveq12d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘˜ = 1 ) โ†’ ( ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) ) = ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) ) )
12 1nn โŠข 1 โˆˆ โ„•
13 12 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„• )
14 2cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚ )
15 1cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„‚ )
16 14 15 mulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท 1 ) โˆˆ โ„‚ )
17 16 15 addcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท 1 ) + 1 ) โˆˆ โ„‚ )
18 2t1e2 โŠข ( 2 ยท 1 ) = 2
19 18 oveq1i โŠข ( ( 2 ยท 1 ) + 1 ) = ( 2 + 1 )
20 2p1e3 โŠข ( 2 + 1 ) = 3
21 19 20 eqtri โŠข ( ( 2 ยท 1 ) + 1 ) = 3
22 3ne0 โŠข 3 โ‰  0
23 21 22 eqnetri โŠข ( ( 2 ยท 1 ) + 1 ) โ‰  0
24 23 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท 1 ) + 1 ) โ‰  0 )
25 17 24 reccld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 1 / ( ( 2 ยท 1 ) + 1 ) ) โˆˆ โ„‚ )
26 nncn โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚ )
27 14 26 mulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„‚ )
28 27 15 addcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โˆˆ โ„‚ )
29 1red โŠข ( ๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„ )
30 2re โŠข 2 โˆˆ โ„
31 30 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„ )
32 nnre โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ )
33 31 32 remulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ )
34 33 29 readdcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โˆˆ โ„ )
35 0lt1 โŠข 0 < 1
36 35 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 < 1 )
37 2rp โŠข 2 โˆˆ โ„+
38 37 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„+ )
39 nnrp โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„+ )
40 38 39 rpmulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„+ )
41 29 40 ltaddrp2d โŠข ( ๐‘ โˆˆ โ„• โ†’ 1 < ( ( 2 ยท ๐‘ ) + 1 ) )
42 4 29 34 36 41 lttrd โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 < ( ( 2 ยท ๐‘ ) + 1 ) )
43 42 gt0ne0d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โ‰  0 )
44 28 43 reccld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โˆˆ โ„‚ )
45 2nn0 โŠข 2 โˆˆ โ„•0
46 45 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„•0 )
47 1nn0 โŠข 1 โˆˆ โ„•0
48 47 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„•0 )
49 46 48 nn0mulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท 1 ) โˆˆ โ„•0 )
50 44 49 expcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) โˆˆ โ„‚ )
51 25 50 mulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) ) โˆˆ โ„‚ )
52 5 11 13 51 fvmptd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐พ โ€˜ 1 ) = ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) ) )
53 1re โŠข 1 โˆˆ โ„
54 30 53 remulcli โŠข ( 2 ยท 1 ) โˆˆ โ„
55 54 53 readdcli โŠข ( ( 2 ยท 1 ) + 1 ) โˆˆ โ„
56 55 23 rereccli โŠข ( 1 / ( ( 2 ยท 1 ) + 1 ) ) โˆˆ โ„
57 56 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 1 / ( ( 2 ยท 1 ) + 1 ) ) โˆˆ โ„ )
58 34 43 rereccld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โˆˆ โ„ )
59 58 49 reexpcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) โˆˆ โ„ )
60 57 59 remulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) ) โˆˆ โ„ )
61 52 60 eqeltrd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐พ โ€˜ 1 ) โˆˆ โ„ )
62 1 stirlinglem2 โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ด โ€˜ ๐‘ ) โˆˆ โ„+ )
63 62 relogcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( log โ€˜ ( ๐ด โ€˜ ๐‘ ) ) โˆˆ โ„ )
64 nfcv โŠข โ„ฒ ๐‘› ๐‘
65 nfcv โŠข โ„ฒ ๐‘› log
66 nfmpt1 โŠข โ„ฒ ๐‘› ( ๐‘› โˆˆ โ„• โ†ฆ ( ( ! โ€˜ ๐‘› ) / ( ( โˆš โ€˜ ( 2 ยท ๐‘› ) ) ยท ( ( ๐‘› / e ) โ†‘ ๐‘› ) ) ) )
67 1 66 nfcxfr โŠข โ„ฒ ๐‘› ๐ด
68 67 64 nffv โŠข โ„ฒ ๐‘› ( ๐ด โ€˜ ๐‘ )
69 65 68 nffv โŠข โ„ฒ ๐‘› ( log โ€˜ ( ๐ด โ€˜ ๐‘ ) )
70 2fveq3 โŠข ( ๐‘› = ๐‘ โ†’ ( log โ€˜ ( ๐ด โ€˜ ๐‘› ) ) = ( log โ€˜ ( ๐ด โ€˜ ๐‘ ) ) )
71 64 69 70 2 fvmptf โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( log โ€˜ ( ๐ด โ€˜ ๐‘ ) ) โˆˆ โ„ ) โ†’ ( ๐ต โ€˜ ๐‘ ) = ( log โ€˜ ( ๐ด โ€˜ ๐‘ ) ) )
72 63 71 mpdan โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ต โ€˜ ๐‘ ) = ( log โ€˜ ( ๐ด โ€˜ ๐‘ ) ) )
73 72 63 eqeltrd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ต โ€˜ ๐‘ ) โˆˆ โ„ )
74 peano2nn โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ + 1 ) โˆˆ โ„• )
75 1 stirlinglem2 โŠข ( ( ๐‘ + 1 ) โˆˆ โ„• โ†’ ( ๐ด โ€˜ ( ๐‘ + 1 ) ) โˆˆ โ„+ )
76 74 75 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ด โ€˜ ( ๐‘ + 1 ) ) โˆˆ โ„+ )
77 76 relogcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( log โ€˜ ( ๐ด โ€˜ ( ๐‘ + 1 ) ) ) โˆˆ โ„ )
78 nfcv โŠข โ„ฒ ๐‘› ( ๐‘ + 1 )
79 67 78 nffv โŠข โ„ฒ ๐‘› ( ๐ด โ€˜ ( ๐‘ + 1 ) )
80 65 79 nffv โŠข โ„ฒ ๐‘› ( log โ€˜ ( ๐ด โ€˜ ( ๐‘ + 1 ) ) )
81 2fveq3 โŠข ( ๐‘› = ( ๐‘ + 1 ) โ†’ ( log โ€˜ ( ๐ด โ€˜ ๐‘› ) ) = ( log โ€˜ ( ๐ด โ€˜ ( ๐‘ + 1 ) ) ) )
82 78 80 81 2 fvmptf โŠข ( ( ( ๐‘ + 1 ) โˆˆ โ„• โˆง ( log โ€˜ ( ๐ด โ€˜ ( ๐‘ + 1 ) ) ) โˆˆ โ„ ) โ†’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) = ( log โ€˜ ( ๐ด โ€˜ ( ๐‘ + 1 ) ) ) )
83 74 77 82 syl2anc โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) = ( log โ€˜ ( ๐ด โ€˜ ( ๐‘ + 1 ) ) ) )
84 83 77 eqeltrd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) โˆˆ โ„ )
85 73 84 resubcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆˆ โ„ )
86 31 29 remulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท 1 ) โˆˆ โ„ )
87 0le2 โŠข 0 โ‰ค 2
88 87 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โ‰ค 2 )
89 0le1 โŠข 0 โ‰ค 1
90 89 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โ‰ค 1 )
91 31 29 88 90 mulge0d โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ( 2 ยท 1 ) )
92 86 91 ge0p1rpd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท 1 ) + 1 ) โˆˆ โ„+ )
93 92 rpreccld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 1 / ( ( 2 ยท 1 ) + 1 ) ) โˆˆ โ„+ )
94 39 rpge0d โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ๐‘ )
95 31 32 88 94 mulge0d โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ( 2 ยท ๐‘ ) )
96 33 95 ge0p1rpd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โˆˆ โ„+ )
97 96 rpreccld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โˆˆ โ„+ )
98 2z โŠข 2 โˆˆ โ„ค
99 98 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„ค )
100 1z โŠข 1 โˆˆ โ„ค
101 100 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„ค )
102 99 101 zmulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท 1 ) โˆˆ โ„ค )
103 97 102 rpexpcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) โˆˆ โ„+ )
104 93 103 rpmulcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท 1 ) ) ) โˆˆ โ„+ )
105 52 104 eqeltrd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐พ โ€˜ 1 ) โˆˆ โ„+ )
106 105 rpgt0d โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 < ( ๐พ โ€˜ 1 ) )
107 85 61 resubcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆ’ ( ๐พ โ€˜ 1 ) ) โˆˆ โ„ )
108 eqid โŠข ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) = ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) )
109 101 peano2zd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 1 + 1 ) โˆˆ โ„ค )
110 nnuz โŠข โ„• = ( โ„คโ‰ฅ โ€˜ 1 )
111 3 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ๐พ = ( ๐‘˜ โˆˆ โ„• โ†ฆ ( ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) ) ) )
112 oveq2 โŠข ( ๐‘˜ = ๐‘— โ†’ ( 2 ยท ๐‘˜ ) = ( 2 ยท ๐‘— ) )
113 112 oveq1d โŠข ( ๐‘˜ = ๐‘— โ†’ ( ( 2 ยท ๐‘˜ ) + 1 ) = ( ( 2 ยท ๐‘— ) + 1 ) )
114 113 oveq2d โŠข ( ๐‘˜ = ๐‘— โ†’ ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) = ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) )
115 112 oveq2d โŠข ( ๐‘˜ = ๐‘— โ†’ ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) = ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) )
116 114 115 oveq12d โŠข ( ๐‘˜ = ๐‘— โ†’ ( ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) ) = ( ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) ) )
117 116 adantl โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โˆง ๐‘˜ = ๐‘— ) โ†’ ( ( 1 / ( ( 2 ยท ๐‘˜ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘˜ ) ) ) = ( ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) ) )
118 simpr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ๐‘— โˆˆ โ„• )
119 2cnd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 2 โˆˆ โ„‚ )
120 nncn โŠข ( ๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„‚ )
121 120 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ๐‘— โˆˆ โ„‚ )
122 119 121 mulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„‚ )
123 1cnd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 1 โˆˆ โ„‚ )
124 122 123 addcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โˆˆ โ„‚ )
125 0red โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 0 โˆˆ โ„ )
126 1red โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 1 โˆˆ โ„ )
127 30 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 2 โˆˆ โ„ )
128 nnre โŠข ( ๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„ )
129 128 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ๐‘— โˆˆ โ„ )
130 127 129 remulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„ )
131 130 126 readdcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โˆˆ โ„ )
132 35 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 0 < 1 )
133 37 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 2 โˆˆ โ„+ )
134 nnrp โŠข ( ๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„+ )
135 134 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ๐‘— โˆˆ โ„+ )
136 133 135 rpmulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„+ )
137 126 136 ltaddrp2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 1 < ( ( 2 ยท ๐‘— ) + 1 ) )
138 125 126 131 132 137 lttrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 0 < ( ( 2 ยท ๐‘— ) + 1 ) )
139 138 gt0ne0d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โ‰  0 )
140 124 139 reccld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) โˆˆ โ„‚ )
141 26 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„‚ )
142 119 141 mulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„‚ )
143 142 123 addcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โˆˆ โ„‚ )
144 43 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โ‰  0 )
145 143 144 reccld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โˆˆ โ„‚ )
146 45 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ 2 โˆˆ โ„•0 )
147 nnnn0 โŠข ( ๐‘— โˆˆ โ„• โ†’ ๐‘— โˆˆ โ„•0 )
148 147 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ๐‘— โˆˆ โ„•0 )
149 146 148 nn0mulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„•0 )
150 145 149 expcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) โˆˆ โ„‚ )
151 140 150 mulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) ) โˆˆ โ„‚ )
152 111 117 118 151 fvmptd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ๐พ โ€˜ ๐‘— ) = ( ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) ) )
153 0red โŠข ( ๐‘— โˆˆ โ„• โ†’ 0 โˆˆ โ„ )
154 1red โŠข ( ๐‘— โˆˆ โ„• โ†’ 1 โˆˆ โ„ )
155 30 a1i โŠข ( ๐‘— โˆˆ โ„• โ†’ 2 โˆˆ โ„ )
156 155 128 remulcld โŠข ( ๐‘— โˆˆ โ„• โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„ )
157 156 154 readdcld โŠข ( ๐‘— โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โˆˆ โ„ )
158 35 a1i โŠข ( ๐‘— โˆˆ โ„• โ†’ 0 < 1 )
159 37 a1i โŠข ( ๐‘— โˆˆ โ„• โ†’ 2 โˆˆ โ„+ )
160 159 134 rpmulcld โŠข ( ๐‘— โˆˆ โ„• โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„+ )
161 154 160 ltaddrp2d โŠข ( ๐‘— โˆˆ โ„• โ†’ 1 < ( ( 2 ยท ๐‘— ) + 1 ) )
162 153 154 157 158 161 lttrd โŠข ( ๐‘— โˆˆ โ„• โ†’ 0 < ( ( 2 ยท ๐‘— ) + 1 ) )
163 162 gt0ne0d โŠข ( ๐‘— โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โ‰  0 )
164 163 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โ‰  0 )
165 124 164 reccld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) โˆˆ โ„‚ )
166 165 150 mulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) ) โˆˆ โ„‚ )
167 152 166 eqeltrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) โ†’ ( ๐พ โ€˜ ๐‘— ) โˆˆ โ„‚ )
168 eqid โŠข ( ๐‘› โˆˆ โ„• โ†ฆ ( ( ( ( 1 + ( 2 ยท ๐‘› ) ) / 2 ) ยท ( log โ€˜ ( ( ๐‘› + 1 ) / ๐‘› ) ) ) โˆ’ 1 ) ) = ( ๐‘› โˆˆ โ„• โ†ฆ ( ( ( ( 1 + ( 2 ยท ๐‘› ) ) / 2 ) ยท ( log โ€˜ ( ( ๐‘› + 1 ) / ๐‘› ) ) ) โˆ’ 1 ) )
169 1 2 168 3 stirlinglem9 โŠข ( ๐‘ โˆˆ โ„• โ†’ seq 1 ( + , ๐พ ) โ‡ ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) )
170 110 13 167 169 clim2ser โŠข ( ๐‘ โˆˆ โ„• โ†’ seq ( 1 + 1 ) ( + , ๐พ ) โ‡ ( ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆ’ ( seq 1 ( + , ๐พ ) โ€˜ 1 ) ) )
171 peano2nn โŠข ( 1 โˆˆ โ„• โ†’ ( 1 + 1 ) โˆˆ โ„• )
172 uznnssnn โŠข ( ( 1 + 1 ) โˆˆ โ„• โ†’ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โІ โ„• )
173 12 171 172 mp2b โŠข ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โІ โ„•
174 173 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โІ โ„• )
175 174 sseld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ ๐‘— โˆˆ โ„• ) )
176 175 imdistani โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ โ„• ) )
177 176 152 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ๐พ โ€˜ ๐‘— ) = ( ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) ) )
178 30 a1i โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ 2 โˆˆ โ„ )
179 eluzelre โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ ๐‘— โˆˆ โ„ )
180 178 179 remulcld โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„ )
181 1red โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ 1 โˆˆ โ„ )
182 180 181 readdcld โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โˆˆ โ„ )
183 173 sseli โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ ๐‘— โˆˆ โ„• )
184 183 163 syl โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โ‰  0 )
185 182 184 rereccld โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) โˆˆ โ„ )
186 185 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) โˆˆ โ„ )
187 34 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โˆˆ โ„ )
188 43 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โ‰  0 )
189 187 188 rereccld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โˆˆ โ„ )
190 176 149 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„•0 )
191 189 190 reexpcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) โˆˆ โ„ )
192 186 191 remulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) ) โˆˆ โ„ )
193 177 192 eqeltrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ๐พ โ€˜ ๐‘— ) โˆˆ โ„ )
194 1red โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 1 โˆˆ โ„ )
195 30 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 2 โˆˆ โ„ )
196 176 129 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ๐‘— โˆˆ โ„ )
197 195 196 remulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„ )
198 87 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค 2 )
199 0red โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ 0 โˆˆ โ„ )
200 87 a1i โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ 0 โ‰ค 2 )
201 1p1e2 โŠข ( 1 + 1 ) = 2
202 eluzle โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ ( 1 + 1 ) โ‰ค ๐‘— )
203 201 202 eqbrtrrid โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ 2 โ‰ค ๐‘— )
204 199 178 179 200 203 letrd โŠข ( ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) โ†’ 0 โ‰ค ๐‘— )
205 204 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ๐‘— )
206 195 196 198 205 mulge0d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ( 2 ยท ๐‘— ) )
207 197 206 ge0p1rpd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ( 2 ยท ๐‘— ) + 1 ) โˆˆ โ„+ )
208 89 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค 1 )
209 194 207 208 divge0d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) )
210 32 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ๐‘ โˆˆ โ„ )
211 195 210 remulcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ )
212 94 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ๐‘ )
213 195 210 198 212 mulge0d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ( 2 ยท ๐‘ ) )
214 211 213 ge0p1rpd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ ( ( 2 ยท ๐‘ ) + 1 ) โˆˆ โ„+ )
215 194 214 208 divge0d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) )
216 189 190 215 expge0d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) )
217 186 191 209 216 mulge0d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ( ( 1 / ( ( 2 ยท ๐‘— ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐‘ ) + 1 ) ) โ†‘ ( 2 ยท ๐‘— ) ) ) )
218 217 177 breqtrrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘— โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 + 1 ) ) ) โ†’ 0 โ‰ค ( ๐พ โ€˜ ๐‘— ) )
219 108 109 170 193 218 iserge0 โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ( ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆ’ ( seq 1 ( + , ๐พ ) โ€˜ 1 ) ) )
220 seq1 โŠข ( 1 โˆˆ โ„ค โ†’ ( seq 1 ( + , ๐พ ) โ€˜ 1 ) = ( ๐พ โ€˜ 1 ) )
221 100 220 mp1i โŠข ( ๐‘ โˆˆ โ„• โ†’ ( seq 1 ( + , ๐พ ) โ€˜ 1 ) = ( ๐พ โ€˜ 1 ) )
222 221 oveq2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆ’ ( seq 1 ( + , ๐พ ) โ€˜ 1 ) ) = ( ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆ’ ( ๐พ โ€˜ 1 ) ) )
223 219 222 breqtrd โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ( ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆ’ ( ๐พ โ€˜ 1 ) ) )
224 4 107 61 223 leadd1dd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 0 + ( ๐พ โ€˜ 1 ) ) โ‰ค ( ( ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆ’ ( ๐พ โ€˜ 1 ) ) + ( ๐พ โ€˜ 1 ) ) )
225 52 51 eqeltrd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐พ โ€˜ 1 ) โˆˆ โ„‚ )
226 225 addlidd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 0 + ( ๐พ โ€˜ 1 ) ) = ( ๐พ โ€˜ 1 ) )
227 73 recnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ต โ€˜ ๐‘ ) โˆˆ โ„‚ )
228 84 recnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) โˆˆ โ„‚ )
229 227 228 subcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆˆ โ„‚ )
230 229 225 npcand โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) โˆ’ ( ๐พ โ€˜ 1 ) ) + ( ๐พ โ€˜ 1 ) ) = ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) )
231 224 226 230 3brtr3d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐พ โ€˜ 1 ) โ‰ค ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) )
232 4 61 85 106 231 ltletrd โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 < ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) )
233 84 73 posdifd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐ต โ€˜ ( ๐‘ + 1 ) ) < ( ๐ต โ€˜ ๐‘ ) โ†” 0 < ( ( ๐ต โ€˜ ๐‘ ) โˆ’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) ) ) )
234 232 233 mpbird โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐ต โ€˜ ( ๐‘ + 1 ) ) < ( ๐ต โ€˜ ๐‘ ) )