Step | Hyp | Ref
| Expression |
1 | | nnuz 12864 |
. . 3
โข โ =
(โคโฅโ1) |
2 | | 1zzd 12592 |
. . 3
โข (โค
โ 1 โ โค) |
3 | | ax-1cn 11167 |
. . . 4
โข 1 โ
โ |
4 | | divcnv 15798 |
. . . 4
โข (1 โ
โ โ (๐ โ
โ โฆ (1 / ๐))
โ 0) |
5 | 3, 4 | mp1i 13 |
. . 3
โข (โค
โ (๐ โ โ
โฆ (1 / ๐)) โ
0) |
6 | | basel.g |
. . . . 5
โข ๐บ = (๐ โ โ โฆ (1 / ((2 ยท
๐) + 1))) |
7 | | nnex 12217 |
. . . . . 6
โข โ
โ V |
8 | 7 | mptex 7224 |
. . . . 5
โข (๐ โ โ โฆ (1 / ((2
ยท ๐) + 1))) โ
V |
9 | 6, 8 | eqeltri 2829 |
. . . 4
โข ๐บ โ V |
10 | 9 | a1i 11 |
. . 3
โข (โค
โ ๐บ โ
V) |
11 | | oveq2 7416 |
. . . . . 6
โข (๐ = ๐ โ (1 / ๐) = (1 / ๐)) |
12 | | eqid 2732 |
. . . . . 6
โข (๐ โ โ โฆ (1 /
๐)) = (๐ โ โ โฆ (1 / ๐)) |
13 | | ovex 7441 |
. . . . . 6
โข (1 /
๐) โ
V |
14 | 11, 12, 13 | fvmpt 6998 |
. . . . 5
โข (๐ โ โ โ ((๐ โ โ โฆ (1 /
๐))โ๐) = (1 / ๐)) |
15 | 14 | adantl 482 |
. . . 4
โข
((โค โง ๐
โ โ) โ ((๐
โ โ โฆ (1 / ๐))โ๐) = (1 / ๐)) |
16 | | nnrecre 12253 |
. . . . 5
โข (๐ โ โ โ (1 /
๐) โ
โ) |
17 | 16 | adantl 482 |
. . . 4
โข
((โค โง ๐
โ โ) โ (1 / ๐) โ โ) |
18 | 15, 17 | eqeltrd 2833 |
. . 3
โข
((โค โง ๐
โ โ) โ ((๐
โ โ โฆ (1 / ๐))โ๐) โ โ) |
19 | | oveq2 7416 |
. . . . . . . 8
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
20 | 19 | oveq1d 7423 |
. . . . . . 7
โข (๐ = ๐ โ ((2 ยท ๐) + 1) = ((2 ยท ๐) + 1)) |
21 | 20 | oveq2d 7424 |
. . . . . 6
โข (๐ = ๐ โ (1 / ((2 ยท ๐) + 1)) = (1 / ((2 ยท ๐) + 1))) |
22 | | ovex 7441 |
. . . . . 6
โข (1 / ((2
ยท ๐) + 1)) โ
V |
23 | 21, 6, 22 | fvmpt 6998 |
. . . . 5
โข (๐ โ โ โ (๐บโ๐) = (1 / ((2 ยท ๐) + 1))) |
24 | 23 | adantl 482 |
. . . 4
โข
((โค โง ๐
โ โ) โ (๐บโ๐) = (1 / ((2 ยท ๐) + 1))) |
25 | | 2nn 12284 |
. . . . . . . 8
โข 2 โ
โ |
26 | 25 | a1i 11 |
. . . . . . 7
โข (โค
โ 2 โ โ) |
27 | | nnmulcl 12235 |
. . . . . . 7
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
28 | 26, 27 | sylan 580 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
29 | 28 | peano2nnd 12228 |
. . . . 5
โข
((โค โง ๐
โ โ) โ ((2 ยท ๐) + 1) โ โ) |
30 | 29 | nnrecred 12262 |
. . . 4
โข
((โค โง ๐
โ โ) โ (1 / ((2 ยท ๐) + 1)) โ โ) |
31 | 24, 30 | eqeltrd 2833 |
. . 3
โข
((โค โง ๐
โ โ) โ (๐บโ๐) โ โ) |
32 | | nnre 12218 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
33 | 32 | adantl 482 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ ๐
โ โ) |
34 | 28 | nnred 12226 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
35 | 29 | nnred 12226 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ ((2 ยท ๐) + 1) โ โ) |
36 | | nnnn0 12478 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
37 | 36 | adantl 482 |
. . . . . . . 8
โข
((โค โง ๐
โ โ) โ ๐
โ โ0) |
38 | | nn0addge1 12517 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โค (๐ + ๐)) |
39 | 33, 37, 38 | syl2anc 584 |
. . . . . . 7
โข
((โค โง ๐
โ โ) โ ๐
โค (๐ + ๐)) |
40 | 33 | recnd 11241 |
. . . . . . . 8
โข
((โค โง ๐
โ โ) โ ๐
โ โ) |
41 | 40 | 2timesd 12454 |
. . . . . . 7
โข
((โค โง ๐
โ โ) โ (2 ยท ๐) = (๐ + ๐)) |
42 | 39, 41 | breqtrrd 5176 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ ๐
โค (2 ยท ๐)) |
43 | 34 | lep1d 12144 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (2 ยท ๐) โค ((2 ยท ๐) + 1)) |
44 | 33, 34, 35, 42, 43 | letrd 11370 |
. . . . 5
โข
((โค โง ๐
โ โ) โ ๐
โค ((2 ยท ๐) +
1)) |
45 | | nngt0 12242 |
. . . . . . 7
โข (๐ โ โ โ 0 <
๐) |
46 | 45 | adantl 482 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ 0 < ๐) |
47 | 29 | nngt0d 12260 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ 0 < ((2 ยท ๐) + 1)) |
48 | | lerec 12096 |
. . . . . 6
โข (((๐ โ โ โง 0 <
๐) โง (((2 ยท
๐) + 1) โ โ
โง 0 < ((2 ยท ๐) + 1))) โ (๐ โค ((2 ยท ๐) + 1) โ (1 / ((2 ยท ๐) + 1)) โค (1 / ๐))) |
49 | 33, 46, 35, 47, 48 | syl22anc 837 |
. . . . 5
โข
((โค โง ๐
โ โ) โ (๐
โค ((2 ยท ๐) + 1)
โ (1 / ((2 ยท ๐)
+ 1)) โค (1 / ๐))) |
50 | 44, 49 | mpbid 231 |
. . . 4
โข
((โค โง ๐
โ โ) โ (1 / ((2 ยท ๐) + 1)) โค (1 / ๐)) |
51 | 50, 24, 15 | 3brtr4d 5180 |
. . 3
โข
((โค โง ๐
โ โ) โ (๐บโ๐) โค ((๐ โ โ โฆ (1 / ๐))โ๐)) |
52 | 29 | nnrpd 13013 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ ((2 ยท ๐) + 1) โ
โ+) |
53 | 52 | rpreccld 13025 |
. . . . 5
โข
((โค โง ๐
โ โ) โ (1 / ((2 ยท ๐) + 1)) โ
โ+) |
54 | 53 | rpge0d 13019 |
. . . 4
โข
((โค โง ๐
โ โ) โ 0 โค (1 / ((2 ยท ๐) + 1))) |
55 | 54, 24 | breqtrrd 5176 |
. . 3
โข
((โค โง ๐
โ โ) โ 0 โค (๐บโ๐)) |
56 | 1, 2, 5, 10, 18, 31, 51, 55 | climsqz2 15585 |
. 2
โข (โค
โ ๐บ โ
0) |
57 | 56 | mptru 1548 |
1
โข ๐บ โ 0 |