Step | Hyp | Ref
| Expression |
1 | | elfznn 13529 |
. . . . . 6
โข (๐พ โ (1...๐) โ ๐พ โ โ) |
2 | 1 | nnrpd 13013 |
. . . . 5
โข (๐พ โ (1...๐) โ ๐พ โ
โ+) |
3 | | pirp 25970 |
. . . . 5
โข ฯ
โ โ+ |
4 | | rpmulcl 12996 |
. . . . 5
โข ((๐พ โ โ+
โง ฯ โ โ+) โ (๐พ ยท ฯ) โ
โ+) |
5 | 2, 3, 4 | sylancl 586 |
. . . 4
โข (๐พ โ (1...๐) โ (๐พ ยท ฯ) โ
โ+) |
6 | | basel.n |
. . . . . 6
โข ๐ = ((2 ยท ๐) + 1) |
7 | | 2nn 12284 |
. . . . . . . 8
โข 2 โ
โ |
8 | | nnmulcl 12235 |
. . . . . . . 8
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
9 | 7, 8 | mpan 688 |
. . . . . . 7
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
10 | 9 | peano2nnd 12228 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
11 | 6, 10 | eqeltrid 2837 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
12 | 11 | nnrpd 13013 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ+) |
13 | | rpdivcl 12998 |
. . . 4
โข (((๐พ ยท ฯ) โ
โ+ โง ๐
โ โ+) โ ((๐พ ยท ฯ) / ๐) โ
โ+) |
14 | 5, 12, 13 | syl2anr 597 |
. . 3
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ((๐พ ยท ฯ) / ๐) โ
โ+) |
15 | 14 | rpred 13015 |
. 2
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ((๐พ ยท ฯ) / ๐) โ โ) |
16 | 14 | rpgt0d 13018 |
. 2
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ 0 < ((๐พ ยท ฯ) / ๐)) |
17 | 1 | adantl 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ๐พ โ โ) |
18 | | nnmulcl 12235 |
. . . . . . . 8
โข ((๐พ โ โ โง 2 โ
โ) โ (๐พ ยท
2) โ โ) |
19 | 17, 7, 18 | sylancl 586 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ ยท 2) โ
โ) |
20 | 19 | nnred 12226 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ ยท 2) โ
โ) |
21 | 9 | adantr 481 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (2 ยท ๐) โ โ) |
22 | 21 | nnred 12226 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (2 ยท ๐) โ โ) |
23 | 11 | adantr 481 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ๐ โ โ) |
24 | 23 | nnred 12226 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ๐ โ โ) |
25 | 6, 24 | eqeltrrid 2838 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ((2 ยท ๐) + 1) โ โ) |
26 | 17 | nncnd 12227 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ๐พ โ โ) |
27 | | 2cn 12286 |
. . . . . . . 8
โข 2 โ
โ |
28 | | mulcom 11195 |
. . . . . . . 8
โข ((๐พ โ โ โง 2 โ
โ) โ (๐พ ยท
2) = (2 ยท ๐พ)) |
29 | 26, 27, 28 | sylancl 586 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ ยท 2) = (2 ยท ๐พ)) |
30 | | elfzle2 13504 |
. . . . . . . . 9
โข (๐พ โ (1...๐) โ ๐พ โค ๐) |
31 | 30 | adantl 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ๐พ โค ๐) |
32 | 17 | nnred 12226 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ๐พ โ โ) |
33 | | nnre 12218 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
34 | 33 | adantr 481 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ๐ โ โ) |
35 | | 2re 12285 |
. . . . . . . . . . 11
โข 2 โ
โ |
36 | | 2pos 12314 |
. . . . . . . . . . 11
โข 0 <
2 |
37 | 35, 36 | pm3.2i 471 |
. . . . . . . . . 10
โข (2 โ
โ โง 0 < 2) |
38 | 37 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (2 โ โ โง 0 <
2)) |
39 | | lemul2 12066 |
. . . . . . . . 9
โข ((๐พ โ โ โง ๐ โ โ โง (2 โ
โ โง 0 < 2)) โ (๐พ โค ๐ โ (2 ยท ๐พ) โค (2 ยท ๐))) |
40 | 32, 34, 38, 39 | syl3anc 1371 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ โค ๐ โ (2 ยท ๐พ) โค (2 ยท ๐))) |
41 | 31, 40 | mpbid 231 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (2 ยท ๐พ) โค (2 ยท ๐)) |
42 | 29, 41 | eqbrtrd 5170 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ ยท 2) โค (2 ยท ๐)) |
43 | 22 | ltp1d 12143 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (2 ยท ๐) < ((2 ยท ๐) + 1)) |
44 | 20, 22, 25, 42, 43 | lelttrd 11371 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ ยท 2) < ((2 ยท ๐) + 1)) |
45 | 44, 6 | breqtrrdi 5190 |
. . . 4
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ ยท 2) < ๐) |
46 | 19 | nngt0d 12260 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ 0 < (๐พ ยท 2)) |
47 | 23 | nngt0d 12260 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ 0 < ๐) |
48 | | pire 25967 |
. . . . . 6
โข ฯ
โ โ |
49 | | remulcl 11194 |
. . . . . 6
โข ((๐พ โ โ โง ฯ
โ โ) โ (๐พ
ยท ฯ) โ โ) |
50 | 32, 48, 49 | sylancl 586 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ ยท ฯ) โ
โ) |
51 | 5 | adantl 482 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (๐พ ยท ฯ) โ
โ+) |
52 | 51 | rpgt0d 13018 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ 0 < (๐พ ยท ฯ)) |
53 | | ltdiv2 12099 |
. . . . 5
โข ((((๐พ ยท 2) โ โ
โง 0 < (๐พ ยท
2)) โง (๐ โ โ
โง 0 < ๐) โง
((๐พ ยท ฯ) โ
โ โง 0 < (๐พ
ยท ฯ))) โ ((๐พ
ยท 2) < ๐ โ
((๐พ ยท ฯ) / ๐) < ((๐พ ยท ฯ) / (๐พ ยท 2)))) |
54 | 20, 46, 24, 47, 50, 52, 53 | syl222anc 1386 |
. . . 4
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ((๐พ ยท 2) < ๐ โ ((๐พ ยท ฯ) / ๐) < ((๐พ ยท ฯ) / (๐พ ยท 2)))) |
55 | 45, 54 | mpbid 231 |
. . 3
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ((๐พ ยท ฯ) / ๐) < ((๐พ ยท ฯ) / (๐พ ยท 2))) |
56 | | picn 25968 |
. . . . 5
โข ฯ
โ โ |
57 | 56 | a1i 11 |
. . . 4
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ฯ โ
โ) |
58 | | 2cnne0 12421 |
. . . . 5
โข (2 โ
โ โง 2 โ 0) |
59 | 58 | a1i 11 |
. . . 4
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ (2 โ โ โง 2 โ
0)) |
60 | 17 | nnne0d 12261 |
. . . 4
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ๐พ โ 0) |
61 | | divcan5 11915 |
. . . 4
โข ((ฯ
โ โ โง (2 โ โ โง 2 โ 0) โง (๐พ โ โ โง ๐พ โ 0)) โ ((๐พ ยท ฯ) / (๐พ ยท 2)) = (ฯ / 2)) |
62 | 57, 59, 26, 60, 61 | syl112anc 1374 |
. . 3
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ((๐พ ยท ฯ) / (๐พ ยท 2)) = (ฯ / 2)) |
63 | 55, 62 | breqtrd 5174 |
. 2
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ((๐พ ยท ฯ) / ๐) < (ฯ / 2)) |
64 | | 0xr 11260 |
. . 3
โข 0 โ
โ* |
65 | | rehalfcl 12437 |
. . . 4
โข (ฯ
โ โ โ (ฯ / 2) โ โ) |
66 | | rexr 11259 |
. . . 4
โข ((ฯ /
2) โ โ โ (ฯ / 2) โ
โ*) |
67 | 48, 65, 66 | mp2b 10 |
. . 3
โข (ฯ /
2) โ โ* |
68 | | elioo2 13364 |
. . 3
โข ((0
โ โ* โง (ฯ / 2) โ โ*) โ
(((๐พ ยท ฯ) / ๐) โ (0(,)(ฯ / 2)) โ
(((๐พ ยท ฯ) / ๐) โ โ โง 0 <
((๐พ ยท ฯ) / ๐) โง ((๐พ ยท ฯ) / ๐) < (ฯ / 2)))) |
69 | 64, 67, 68 | mp2an 690 |
. 2
โข (((๐พ ยท ฯ) / ๐) โ (0(,)(ฯ / 2)) โ
(((๐พ ยท ฯ) / ๐) โ โ โง 0 <
((๐พ ยท ฯ) / ๐) โง ((๐พ ยท ฯ) / ๐) < (ฯ / 2))) |
70 | 15, 16, 63, 69 | syl3anbrc 1343 |
1
โข ((๐ โ โ โง ๐พ โ (1...๐)) โ ((๐พ ยท ฯ) / ๐) โ (0(,)(ฯ / 2))) |