Step | Hyp | Ref
| Expression |
1 | | 1nn 12169 |
. . . . 5
โข 1 โ
โ |
2 | | stirlinglem12.1 |
. . . . . . 7
โข ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
3 | 2 | stirlinglem2 44402 |
. . . . . 6
โข (1 โ
โ โ (๐ดโ1)
โ โ+) |
4 | | relogcl 25947 |
. . . . . 6
โข ((๐ดโ1) โ
โ+ โ (logโ(๐ดโ1)) โ โ) |
5 | 1, 3, 4 | mp2b 10 |
. . . . 5
โข
(logโ(๐ดโ1)) โ โ |
6 | | nfcv 2904 |
. . . . . 6
โข
โฒ๐1 |
7 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐log |
8 | | nfmpt1 5214 |
. . . . . . . . 9
โข
โฒ๐(๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
9 | 2, 8 | nfcxfr 2902 |
. . . . . . . 8
โข
โฒ๐๐ด |
10 | 9, 6 | nffv 6853 |
. . . . . . 7
โข
โฒ๐(๐ดโ1) |
11 | 7, 10 | nffv 6853 |
. . . . . 6
โข
โฒ๐(logโ(๐ดโ1)) |
12 | | 2fveq3 6848 |
. . . . . 6
โข (๐ = 1 โ (logโ(๐ดโ๐)) = (logโ(๐ดโ1))) |
13 | | stirlinglem12.2 |
. . . . . 6
โข ๐ต = (๐ โ โ โฆ (logโ(๐ดโ๐))) |
14 | 6, 11, 12, 13 | fvmptf 6970 |
. . . . 5
โข ((1
โ โ โง (logโ(๐ดโ1)) โ โ) โ (๐ตโ1) = (logโ(๐ดโ1))) |
15 | 1, 5, 14 | mp2an 691 |
. . . 4
โข (๐ตโ1) = (logโ(๐ดโ1)) |
16 | 15, 5 | eqeltri 2830 |
. . 3
โข (๐ตโ1) โ
โ |
17 | 16 | a1i 11 |
. 2
โข (๐ โ โ โ (๐ตโ1) โ
โ) |
18 | 2 | stirlinglem2 44402 |
. . . . 5
โข (๐ โ โ โ (๐ดโ๐) โ
โ+) |
19 | 18 | relogcld 25994 |
. . . 4
โข (๐ โ โ โ
(logโ(๐ดโ๐)) โ
โ) |
20 | | nfcv 2904 |
. . . . 5
โข
โฒ๐๐ |
21 | 9, 20 | nffv 6853 |
. . . . . 6
โข
โฒ๐(๐ดโ๐) |
22 | 7, 21 | nffv 6853 |
. . . . 5
โข
โฒ๐(logโ(๐ดโ๐)) |
23 | | 2fveq3 6848 |
. . . . 5
โข (๐ = ๐ โ (logโ(๐ดโ๐)) = (logโ(๐ดโ๐))) |
24 | 20, 22, 23, 13 | fvmptf 6970 |
. . . 4
โข ((๐ โ โ โง
(logโ(๐ดโ๐)) โ โ) โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
25 | 19, 24 | mpdan 686 |
. . 3
โข (๐ โ โ โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
26 | 25, 19 | eqeltrd 2834 |
. 2
โข (๐ โ โ โ (๐ตโ๐) โ โ) |
27 | | 4re 12242 |
. . . 4
โข 4 โ
โ |
28 | | 4ne0 12266 |
. . . 4
โข 4 โ
0 |
29 | 27, 28 | rereccli 11925 |
. . 3
โข (1 / 4)
โ โ |
30 | 29 | a1i 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)) |
36 | 35 | biimpi 215 |
. . . . 5
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
37 | | elfznn 13476 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ๐ โ โ) |
38 | 2 | stirlinglem2 44402 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ดโ๐) โ
โ+) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ (๐ดโ๐) โ
โ+) |
40 | 39 | relogcld 25994 |
. . . . . . . 8
โข (๐ โ (1...๐) โ (logโ(๐ดโ๐)) โ โ) |
41 | | nfcv 2904 |
. . . . . . . . 9
โข
โฒ๐๐ |
42 | 9, 41 | nffv 6853 |
. . . . . . . . . 10
โข
โฒ๐(๐ดโ๐) |
43 | 7, 42 | nffv 6853 |
. . . . . . . . 9
โข
โฒ๐(logโ(๐ดโ๐)) |
44 | | 2fveq3 6848 |
. . . . . . . . 9
โข (๐ = ๐ โ (logโ(๐ดโ๐)) = (logโ(๐ดโ๐))) |
45 | 41, 43, 44, 13 | fvmptf 6970 |
. . . . . . . 8
โข ((๐ โ โ โง
(logโ(๐ดโ๐)) โ โ) โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
46 | 37, 40, 45 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (1...๐) โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
47 | 46 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
48 | 39 | rpcnd 12964 |
. . . . . . . 8
โข (๐ โ (1...๐) โ (๐ดโ๐) โ โ) |
49 | 48 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
50 | 38 | rpne0d 12967 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ดโ๐) โ 0) |
51 | 37, 50 | syl 17 |
. . . . . . . 8
โข (๐ โ (1...๐) โ (๐ดโ๐) โ 0) |
52 | 51 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐ดโ๐) โ 0) |
53 | 49, 52 | logcld 25942 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (logโ(๐ดโ๐)) โ โ) |
54 | 47, 53 | eqeltrd 2834 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
55 | 31, 32, 33, 34, 36, 54 | telfsumo 15692 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (1..^๐)((๐ตโ๐) โ (๐ตโ(๐ + 1))) = ((๐ตโ1) โ (๐ตโ๐))) |
56 | | nnz 12525 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
57 | | fzoval 13579 |
. . . . . 6
โข (๐ โ โค โ
(1..^๐) = (1...(๐ โ 1))) |
58 | 56, 57 | syl 17 |
. . . . 5
โข (๐ โ โ โ
(1..^๐) = (1...(๐ โ 1))) |
59 | 58 | sumeq1d 15591 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (1..^๐)((๐ตโ๐) โ (๐ตโ(๐ + 1))) = ฮฃ๐ โ (1...(๐ โ 1))((๐ตโ๐) โ (๐ตโ(๐ + 1)))) |
60 | 55, 59 | eqtr3d 2775 |
. . 3
โข (๐ โ โ โ ((๐ตโ1) โ (๐ตโ๐)) = ฮฃ๐ โ (1...(๐ โ 1))((๐ตโ๐) โ (๐ตโ(๐ + 1)))) |
61 | | fzfid 13884 |
. . . . 5
โข (๐ โ โ โ
(1...(๐ โ 1)) โ
Fin) |
62 | | elfznn 13476 |
. . . . . . . 8
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
63 | 62 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
64 | 2 | stirlinglem2 44402 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ดโ๐) โ
โ+) |
65 | 64 | relogcld 25994 |
. . . . . . . . 9
โข (๐ โ โ โ
(logโ(๐ดโ๐)) โ
โ) |
66 | | nfcv 2904 |
. . . . . . . . . 10
โข
โฒ๐๐ |
67 | 9, 66 | nffv 6853 |
. . . . . . . . . . 11
โข
โฒ๐(๐ดโ๐) |
68 | 7, 67 | nffv 6853 |
. . . . . . . . . 10
โข
โฒ๐(logโ(๐ดโ๐)) |
69 | | 2fveq3 6848 |
. . . . . . . . . 10
โข (๐ = ๐ โ (logโ(๐ดโ๐)) = (logโ(๐ดโ๐))) |
70 | 66, 68, 69, 13 | fvmptf 6970 |
. . . . . . . . 9
โข ((๐ โ โ โง
(logโ(๐ดโ๐)) โ โ) โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
71 | 65, 70 | mpdan 686 |
. . . . . . . 8
โข (๐ โ โ โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
72 | 71, 65 | eqeltrd 2834 |
. . . . . . 7
โข (๐ โ โ โ (๐ตโ๐) โ โ) |
73 | 63, 72 | syl 17 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ตโ๐) โ โ) |
74 | | peano2nn 12170 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ
โ) |
75 | 2 | stirlinglem2 44402 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ โ โ
(๐ดโ(๐ + 1)) โ
โ+) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ดโ(๐ + 1)) โ
โ+) |
77 | 76 | relogcld 25994 |
. . . . . . . . . 10
โข (๐ โ โ โ
(logโ(๐ดโ(๐ + 1))) โ
โ) |
78 | | nfcv 2904 |
. . . . . . . . . . 11
โข
โฒ๐(๐ + 1) |
79 | 9, 78 | nffv 6853 |
. . . . . . . . . . . 12
โข
โฒ๐(๐ดโ(๐ + 1)) |
80 | 7, 79 | nffv 6853 |
. . . . . . . . . . 11
โข
โฒ๐(logโ(๐ดโ(๐ + 1))) |
81 | | 2fveq3 6848 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (logโ(๐ดโ๐)) = (logโ(๐ดโ(๐ + 1)))) |
82 | 78, 80, 81, 13 | fvmptf 6970 |
. . . . . . . . . 10
โข (((๐ + 1) โ โ โง
(logโ(๐ดโ(๐ + 1))) โ โ) โ
(๐ตโ(๐ + 1)) = (logโ(๐ดโ(๐ + 1)))) |
83 | 74, 77, 82 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ตโ(๐ + 1)) = (logโ(๐ดโ(๐ + 1)))) |
84 | 83, 77 | eqeltrd 2834 |
. . . . . . . 8
โข (๐ โ โ โ (๐ตโ(๐ + 1)) โ โ) |
85 | 62, 84 | syl 17 |
. . . . . . 7
โข (๐ โ (1...(๐ โ 1)) โ (๐ตโ(๐ + 1)) โ โ) |
86 | 85 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ตโ(๐ + 1)) โ โ) |
87 | 73, 86 | resubcld 11588 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ตโ๐) โ (๐ตโ(๐ + 1))) โ โ) |
88 | 61, 87 | fsumrecl 15624 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))((๐ตโ๐) โ (๐ตโ(๐ + 1))) โ โ) |
89 | 29 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (1 / 4) โ
โ) |
90 | 62 | nnred 12173 |
. . . . . . . . 9
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
91 | | 1red 11161 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ โ 1)) โ 1 โ
โ) |
92 | 90, 91 | readdcld 11189 |
. . . . . . . . 9
โข (๐ โ (1...(๐ โ 1)) โ (๐ + 1) โ โ) |
93 | 90, 92 | remulcld 11190 |
. . . . . . . 8
โข (๐ โ (1...(๐ โ 1)) โ (๐ ยท (๐ + 1)) โ โ) |
94 | 90 | recnd 11188 |
. . . . . . . . 9
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
95 | | 1cnd 11155 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ โ 1)) โ 1 โ
โ) |
96 | 94, 95 | addcld 11179 |
. . . . . . . . 9
โข (๐ โ (1...(๐ โ 1)) โ (๐ + 1) โ โ) |
97 | 62 | nnne0d 12208 |
. . . . . . . . 9
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ 0) |
98 | 74 | nnne0d 12208 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ 0) |
99 | 62, 98 | syl 17 |
. . . . . . . . 9
โข (๐ โ (1...(๐ โ 1)) โ (๐ + 1) โ 0) |
100 | 94, 96, 97, 99 | mulne0d 11812 |
. . . . . . . 8
โข (๐ โ (1...(๐ โ 1)) โ (๐ ยท (๐ + 1)) โ 0) |
101 | 93, 100 | rereccld 11987 |
. . . . . . 7
โข (๐ โ (1...(๐ โ 1)) โ (1 / (๐ ยท (๐ + 1))) โ โ) |
102 | 101 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (1 / (๐ ยท (๐ + 1))) โ โ) |
103 | 89, 102 | remulcld 11190 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((1 / 4) ยท (1 /
(๐ ยท (๐ + 1)))) โ
โ) |
104 | 61, 103 | fsumrecl 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))โ๐)) |
107 | 2, 13, 105, 106 | stirlinglem10 44410 |
. . . . . 6
โข (๐ โ โ โ ((๐ตโ๐) โ (๐ตโ(๐ + 1))) โค ((1 / 4) ยท (1 / (๐ ยท (๐ + 1))))) |
108 | 63, 107 | syl 17 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ตโ๐) โ (๐ตโ(๐ + 1))) โค ((1 / 4) ยท (1 / (๐ ยท (๐ + 1))))) |
109 | 61, 87, 103, 108 | fsumle 15689 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))((๐ตโ๐) โ (๐ตโ(๐ + 1))) โค ฮฃ๐ โ (1...(๐ โ 1))((1 / 4) ยท (1 / (๐ ยท (๐ + 1))))) |
110 | 61, 102 | fsumrecl 15624 |
. . . . . 6
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1))) โ โ) |
111 | | 1red 11161 |
. . . . . 6
โข (๐ โ โ โ 1 โ
โ) |
112 | | 4pos 12265 |
. . . . . . . . 9
โข 0 <
4 |
113 | 27, 112 | elrpii 12923 |
. . . . . . . 8
โข 4 โ
โ+ |
114 | 113 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
โ+) |
115 | | 0red 11163 |
. . . . . . . 8
โข (๐ โ โ โ 0 โ
โ) |
116 | | 0lt1 11682 |
. . . . . . . . 9
โข 0 <
1 |
117 | 116 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 0 <
1) |
118 | 115, 111,
117 | ltled 11308 |
. . . . . . 7
โข (๐ โ โ โ 0 โค
1) |
119 | 111, 114,
118 | divge0d 13002 |
. . . . . 6
โข (๐ โ โ โ 0 โค (1
/ 4)) |
120 | | eqid 2733 |
. . . . . . . . . 10
โข
(โคโฅโ๐) = (โคโฅโ๐) |
121 | | eluznn 12848 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
122 | | stirlinglem12.3 |
. . . . . . . . . . . . 13
โข ๐น = (๐ โ โ โฆ (1 / (๐ ยท (๐ + 1)))) |
123 | 122 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐น = (๐ โ โ โฆ (1 / (๐ ยท (๐ + 1))))) |
124 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ = ๐) โ ๐ = ๐) |
125 | 124 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ = ๐) โ (๐ + 1) = (๐ + 1)) |
126 | 124, 125 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ = ๐) โ (๐ ยท (๐ + 1)) = (๐ ยท (๐ + 1))) |
127 | 126 | oveq2d 7374 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ = ๐) โ (1 / (๐ ยท (๐ + 1))) = (1 / (๐ ยท (๐ + 1)))) |
128 | | id 22 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
129 | | nnre 12165 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
130 | | 1red 11161 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 1 โ
โ) |
131 | 129, 130 | readdcld 11189 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ + 1) โ
โ) |
132 | 129, 131 | remulcld 11190 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ ยท (๐ + 1)) โ โ) |
133 | | nncn 12166 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
134 | | 1cnd 11155 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 1 โ
โ) |
135 | 133, 134 | addcld 11179 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ + 1) โ
โ) |
136 | | nnne0 12192 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ 0) |
137 | 133, 135,
136, 98 | mulne0d 11812 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ ยท (๐ + 1)) โ 0) |
138 | 132, 137 | rereccld 11987 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1 /
(๐ ยท (๐ + 1))) โ
โ) |
139 | 123, 127,
128, 138 | fvmptd 6956 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐นโ๐) = (1 / (๐ ยท (๐ + 1)))) |
140 | 121, 139 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (๐นโ๐) = (1 / (๐ ยท (๐ + 1)))) |
141 | 121 | nnred 12173 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
142 | | 1red 11161 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ 1 โ โ) |
143 | 141, 142 | readdcld 11189 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (๐ + 1) โ โ) |
144 | 141, 143 | remulcld 11190 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (๐ ยท (๐ + 1)) โ โ) |
145 | 141 | recnd 11188 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
146 | | 1cnd 11155 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ 1 โ โ) |
147 | 145, 146 | addcld 11179 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (๐ + 1) โ โ) |
148 | 121 | nnne0d 12208 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ 0) |
149 | 121, 98 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (๐ + 1) โ 0) |
150 | 145, 147,
148, 149 | mulne0d 11812 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (๐ ยท (๐ + 1)) โ 0) |
151 | 144, 150 | rereccld 11987 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (1 / (๐ ยท (๐ + 1))) โ โ) |
152 | | seqeq1 13915 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ seq๐( + , ๐น) = seq1( + , ๐น)) |
153 | 122 | trireciplem 15752 |
. . . . . . . . . . . . . 14
โข seq1( + ,
๐น) โ
1 |
154 | | climrel 15380 |
. . . . . . . . . . . . . . 15
โข Rel
โ |
155 | 154 | releldmi 5904 |
. . . . . . . . . . . . . 14
โข (seq1( +
, ๐น) โ 1 โ seq1(
+ , ๐น) โ dom โ
) |
156 | 153, 155 | mp1i 13 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ seq1( + , ๐น) โ dom โ
) |
157 | 152, 156 | eqeltrd 2834 |
. . . . . . . . . . . 12
โข (๐ = 1 โ seq๐( + , ๐น) โ dom โ ) |
158 | 157 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ = 1) โ seq๐( + , ๐น) โ dom โ ) |
159 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ยฌ
๐ = 1) โ ๐ โ
โ) |
160 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ยฌ
๐ = 1) โ ยฌ ๐ = 1) |
161 | | elnn1uz2 12855 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (๐ = 1 โจ ๐ โ
(โคโฅโ2))) |
162 | 159, 161 | sylib 217 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ยฌ
๐ = 1) โ (๐ = 1 โจ ๐ โ
(โคโฅโ2))) |
163 | 162 | ord 863 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ยฌ
๐ = 1) โ (ยฌ ๐ = 1 โ ๐ โ
(โคโฅโ2))) |
164 | 160, 163 | mpd 15 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ยฌ
๐ = 1) โ ๐ โ
(โคโฅโ2)) |
165 | | uz2m1nn 12853 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ยฌ
๐ = 1) โ (๐ โ 1) โ
โ) |
167 | | nncn 12166 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โ) |
168 | 167 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ ๐ โ
โ) |
169 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ 1 โ โ) |
170 | 168, 169 | npcand 11521 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ ((๐ โ 1) + 1)
= ๐) |
171 | 170 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ ๐ = ((๐ โ 1) +
1)) |
172 | 171 | seqeq1d 13918 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ seq๐( + , ๐น) = seq((๐ โ 1) + 1)( + , ๐น)) |
173 | | nnuz 12811 |
. . . . . . . . . . . . . . . 16
โข โ =
(โคโฅโ1) |
174 | | id 22 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ 1) โ โ
โ (๐ โ 1) โ
โ) |
175 | 138 | recnd 11188 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (1 /
(๐ ยท (๐ + 1))) โ
โ) |
176 | 139, 175 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐นโ๐) โ โ) |
177 | 176 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ 1) โ โ โง
๐ โ โ) โ
(๐นโ๐) โ โ) |
178 | 153 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ 1) โ โ
โ seq1( + , ๐น) โ
1) |
179 | 173, 174,
177, 178 | clim2ser 15545 |
. . . . . . . . . . . . . . 15
โข ((๐ โ 1) โ โ
โ seq((๐ โ 1) +
1)( + , ๐น) โ (1
โ (seq1( + , ๐น)โ(๐ โ 1)))) |
180 | 179 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ seq((๐ โ 1) +
1)( + , ๐น) โ (1
โ (seq1( + , ๐น)โ(๐ โ 1)))) |
181 | 172, 180 | eqbrtrd 5128 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ seq๐( + , ๐น) โ (1 โ (seq1( + ,
๐น)โ(๐ โ 1)))) |
182 | 154 | releldmi 5904 |
. . . . . . . . . . . . 13
โข (seq๐( + , ๐น) โ (1 โ (seq1( + , ๐น)โ(๐ โ 1))) โ seq๐( + , ๐น) โ dom โ ) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ seq๐( + , ๐น) โ dom โ
) |
184 | 159, 166,
183 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ยฌ
๐ = 1) โ seq๐( + , ๐น) โ dom โ ) |
185 | 158, 184 | pm2.61dan 812 |
. . . . . . . . . 10
โข (๐ โ โ โ seq๐( + , ๐น) โ dom โ ) |
186 | 120, 56, 140, 151, 185 | isumrecl 15655 |
. . . . . . . . 9
โข (๐ โ โ โ
ฮฃ๐ โ
(โคโฅโ๐)(1 / (๐ ยท (๐ + 1))) โ โ) |
187 | 121 | nnrpd 12960 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ+) |
188 | 187 | rpge0d 12966 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ 0 โค ๐) |
189 | 141, 188 | ge0p1rpd 12992 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (๐ + 1) โ
โ+) |
190 | 187, 189 | rpmulcld 12978 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ (๐ ยท (๐ + 1)) โ
โ+) |
191 | 118 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ 0 โค 1) |
192 | 142, 190,
191 | divge0d 13002 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ 0 โค (1 / (๐ ยท (๐ + 1)))) |
193 | 120, 56, 140, 151, 185, 192 | isumge0 15656 |
. . . . . . . . 9
โข (๐ โ โ โ 0 โค
ฮฃ๐ โ
(โคโฅโ๐)(1 / (๐ ยท (๐ + 1)))) |
194 | 115, 186,
110, 193 | leadd2dd 11775 |
. . . . . . . 8
โข (๐ โ โ โ
(ฮฃ๐ โ
(1...(๐ โ 1))(1 /
(๐ ยท (๐ + 1))) + 0) โค (ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1))) + ฮฃ๐ โ (โคโฅโ๐)(1 / (๐ ยท (๐ + 1))))) |
195 | 110 | recnd 11188 |
. . . . . . . . . 10
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1))) โ โ) |
196 | 195 | addid1d 11360 |
. . . . . . . . 9
โข (๐ โ โ โ
(ฮฃ๐ โ
(1...(๐ โ 1))(1 /
(๐ ยท (๐ + 1))) + 0) = ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1)))) |
197 | 196 | eqcomd 2739 |
. . . . . . . 8
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1))) = (ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1))) + 0)) |
198 | | id 22 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
199 | 139 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐นโ๐) = (1 / (๐ ยท (๐ + 1)))) |
200 | 133 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
201 | | 1cnd 11155 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ 1 โ
โ) |
202 | 200, 201 | addcld 11179 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + 1) โ
โ) |
203 | 200, 202 | mulcld 11180 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) โ โ) |
204 | 136 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ 0) |
205 | 98 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + 1) โ 0) |
206 | 200, 202,
204, 205 | mulne0d 11812 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) โ 0) |
207 | 203, 206 | reccld 11929 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (1 /
(๐ ยท (๐ + 1))) โ
โ) |
208 | 153, 155 | mp1i 13 |
. . . . . . . . 9
โข (๐ โ โ โ seq1( + ,
๐น) โ dom โ
) |
209 | 173, 120,
198, 199, 207, 208 | isumsplit 15730 |
. . . . . . . 8
โข (๐ โ โ โ
ฮฃ๐ โ โ (1
/ (๐ ยท (๐ + 1))) = (ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1))) + ฮฃ๐ โ (โคโฅโ๐)(1 / (๐ ยท (๐ + 1))))) |
210 | 194, 197,
209 | 3brtr4d 5138 |
. . . . . . 7
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1))) โค ฮฃ๐ โ โ (1 / (๐ ยท (๐ + 1)))) |
211 | | 1zzd 12539 |
. . . . . . . . 9
โข (โค
โ 1 โ โค) |
212 | 139 | adantl 483 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ) โ (๐นโ๐) = (1 / (๐ ยท (๐ + 1)))) |
213 | 175 | adantl 483 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ) โ (1 / (๐ ยท (๐ + 1))) โ โ) |
214 | 153 | a1i 11 |
. . . . . . . . 9
โข (โค
โ seq1( + , ๐น) โ
1) |
215 | 173, 211,
212, 213, 214 | isumclim 15647 |
. . . . . . . 8
โข (โค
โ ฮฃ๐ โ
โ (1 / (๐ ยท
(๐ + 1))) =
1) |
216 | 215 | mptru 1549 |
. . . . . . 7
โข
ฮฃ๐ โ
โ (1 / (๐ ยท
(๐ + 1))) =
1 |
217 | 210, 216 | breqtrdi 5147 |
. . . . . 6
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))(1 / (๐ ยท (๐ + 1))) โค 1) |
218 | 110, 111,
30, 119, 217 | lemul2ad 12100 |
. . . . 5
โข (๐ โ โ โ ((1 / 4)
ยท ฮฃ๐ โ
(1...(๐ โ 1))(1 /
(๐ ยท (๐ + 1)))) โค ((1 / 4) ยท
1)) |
219 | | 4cn 12243 |
. . . . . . . 8
โข 4 โ
โ |
220 | 219 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
โ) |
221 | 112 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 0 <
4) |
222 | 221 | gt0ne0d 11724 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
0) |
223 | 220, 222 | reccld 11929 |
. . . . . 6
โข (๐ โ โ โ (1 / 4)
โ โ) |
224 | 102 | recnd 11188 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (1 / (๐ ยท (๐ + 1))) โ โ) |
225 | 61, 223, 224 | fsummulc2 15674 |
. . . . 5
โข (๐ โ โ โ ((1 / 4)
ยท ฮฃ๐ โ
(1...(๐ โ 1))(1 /
(๐ ยท (๐ + 1)))) = ฮฃ๐ โ (1...(๐ โ 1))((1 / 4) ยท (1 / (๐ ยท (๐ + 1))))) |
226 | 223 | mulid1d 11177 |
. . . . 5
โข (๐ โ โ โ ((1 / 4)
ยท 1) = (1 / 4)) |
227 | 218, 225,
226 | 3brtr3d 5137 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))((1 / 4) ยท (1
/ (๐ ยท (๐ + 1)))) โค (1 /
4)) |
228 | 88, 104, 30, 109, 227 | letrd 11317 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))((๐ตโ๐) โ (๐ตโ(๐ + 1))) โค (1 / 4)) |
229 | 60, 228 | eqbrtrd 5128 |
. 2
โข (๐ โ โ โ ((๐ตโ1) โ (๐ตโ๐)) โค (1 / 4)) |
230 | 17, 26, 30, 229 | subled 11763 |
1
โข (๐ โ โ โ ((๐ตโ1) โ (1 / 4)) โค
(๐ตโ๐)) |