Step | Hyp | Ref
| Expression |
1 | | nconstwlpolemgt0.0 |
. 2
โข (๐ โ โ๐ฅ โ โ (๐บโ๐ฅ) = 1) |
2 | | 1zzd 9280 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 1 โ
โค) |
3 | | simprl 529 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ๐ฅ โ โ) |
4 | 3 | peano2nnd 8934 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (๐ฅ + 1) โ โ) |
5 | 4 | nnzd 9374 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (๐ฅ + 1) โ โค) |
6 | 5, 2 | zsubcld 9380 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ((๐ฅ + 1) โ 1) โ
โค) |
7 | 2, 6 | fzfigd 10431 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (1...((๐ฅ + 1) โ 1)) โ
Fin) |
8 | | elfznn 10054 |
. . . . . . 7
โข (๐ โ (1...((๐ฅ + 1) โ 1)) โ ๐ โ
โ) |
9 | | 2rp 9658 |
. . . . . . . . . . . 12
โข 2 โ
โ+ |
10 | 9 | a1i 9 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ 2 โ
โ+) |
11 | | simpr 110 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ ๐ โ โ) |
12 | 11 | nnzd 9374 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ ๐ โ โค) |
13 | 10, 12 | rpexpcld 10678 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ (2โ๐) โ
โ+) |
14 | 13 | rpreccld 9707 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ (1 / (2โ๐)) โ
โ+) |
15 | 14 | rpred 9696 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ (1 / (2โ๐)) โ
โ) |
16 | | 0re 7957 |
. . . . . . . . . 10
โข 0 โ
โ |
17 | | 1re 7956 |
. . . . . . . . . 10
โข 1 โ
โ |
18 | | prssi 3751 |
. . . . . . . . . 10
โข ((0
โ โ โง 1 โ โ) โ {0, 1} โ
โ) |
19 | 16, 17, 18 | mp2an 426 |
. . . . . . . . 9
โข {0, 1}
โ โ |
20 | | nconstwlpolem0.g |
. . . . . . . . . . 11
โข (๐ โ ๐บ:โโถ{0, 1}) |
21 | 20 | ad2antrr 488 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ ๐บ:โโถ{0, 1}) |
22 | 21, 11 | ffvelcdmd 5653 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ (๐บโ๐) โ {0, 1}) |
23 | 19, 22 | sselid 3154 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ (๐บโ๐) โ โ) |
24 | 15, 23 | remulcld 7988 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ ((1 / (2โ๐)) ยท (๐บโ๐)) โ โ) |
25 | 8, 24 | sylan2 286 |
. . . . . 6
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (1...((๐ฅ + 1) โ 1))) โ ((1 / (2โ๐)) ยท (๐บโ๐)) โ โ) |
26 | 7, 25 | fsumrecl 11409 |
. . . . 5
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ฮฃ๐ โ (1...((๐ฅ + 1) โ 1))((1 / (2โ๐)) ยท (๐บโ๐)) โ โ) |
27 | | eqid 2177 |
. . . . . 6
โข
(โคโฅโ(๐ฅ + 1)) = (โคโฅโ(๐ฅ + 1)) |
28 | | eqid 2177 |
. . . . . . 7
โข (๐ โ โ โฆ ((1 /
(2โ๐)) ยท (๐บโ๐))) = (๐ โ โ โฆ ((1 / (2โ๐)) ยท (๐บโ๐))) |
29 | | oveq2 5883 |
. . . . . . . . 9
โข (๐ = ๐ โ (2โ๐) = (2โ๐)) |
30 | 29 | oveq2d 5891 |
. . . . . . . 8
โข (๐ = ๐ โ (1 / (2โ๐)) = (1 / (2โ๐))) |
31 | | fveq2 5516 |
. . . . . . . 8
โข (๐ = ๐ โ (๐บโ๐) = (๐บโ๐)) |
32 | 30, 31 | oveq12d 5893 |
. . . . . . 7
โข (๐ = ๐ โ ((1 / (2โ๐)) ยท (๐บโ๐)) = ((1 / (2โ๐)) ยท (๐บโ๐))) |
33 | | eluznn 9600 |
. . . . . . . 8
โข (((๐ฅ + 1) โ โ โง ๐ โ
(โคโฅโ(๐ฅ + 1))) โ ๐ โ โ) |
34 | 4, 33 | sylan 283 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ ๐ โ
โ) |
35 | 34, 24 | syldan 282 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ ((1 /
(2โ๐)) ยท (๐บโ๐)) โ โ) |
36 | 28, 32, 34, 35 | fvmptd3 5610 |
. . . . . 6
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ ((๐ โ โ โฆ ((1 /
(2โ๐)) ยท (๐บโ๐)))โ๐) = ((1 / (2โ๐)) ยท (๐บโ๐))) |
37 | 20, 28 | trilpolemclim 14787 |
. . . . . . . 8
โข (๐ โ seq1( + , (๐ โ โ โฆ ((1 /
(2โ๐)) ยท (๐บโ๐)))) โ dom โ ) |
38 | 37 | adantr 276 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ seq1( + , (๐ โ โ โฆ ((1 / (2โ๐)) ยท (๐บโ๐)))) โ dom โ ) |
39 | | nnuz 9563 |
. . . . . . . 8
โข โ =
(โคโฅโ1) |
40 | 28, 32, 11, 24 | fvmptd3 5610 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ ((๐ โ โ โฆ ((1 / (2โ๐)) ยท (๐บโ๐)))โ๐) = ((1 / (2โ๐)) ยท (๐บโ๐))) |
41 | 24 | recnd 7986 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ ((1 / (2โ๐)) ยท (๐บโ๐)) โ โ) |
42 | 40, 41 | eqeltrd 2254 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ ((๐ โ โ โฆ ((1 / (2โ๐)) ยท (๐บโ๐)))โ๐) โ โ) |
43 | 39, 4, 42 | iserex 11347 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (seq1( + , (๐ โ โ โฆ ((1 / (2โ๐)) ยท (๐บโ๐)))) โ dom โ โ seq(๐ฅ + 1)( + , (๐ โ โ โฆ ((1 / (2โ๐)) ยท (๐บโ๐)))) โ dom โ )) |
44 | 38, 43 | mpbid 147 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ seq(๐ฅ + 1)( + , (๐ โ โ โฆ ((1 / (2โ๐)) ยท (๐บโ๐)))) โ dom โ ) |
45 | 27, 5, 36, 35, 44 | isumrecl 11437 |
. . . . 5
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ฮฃ๐ โ (โคโฅโ(๐ฅ + 1))((1 / (2โ๐)) ยท (๐บโ๐)) โ โ) |
46 | 3 | nnzd 9374 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ๐ฅ โ โค) |
47 | | fzofig 10432 |
. . . . . . . . . 10
โข ((1
โ โค โง ๐ฅ
โ โค) โ (1..^๐ฅ) โ Fin) |
48 | 2, 46, 47 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (1..^๐ฅ) โ Fin) |
49 | | elfzo1 10190 |
. . . . . . . . . . 11
โข (๐ โ (1..^๐ฅ) โ (๐ โ โ โง ๐ฅ โ โ โง ๐ < ๐ฅ)) |
50 | 49 | simp1bi 1012 |
. . . . . . . . . 10
โข (๐ โ (1..^๐ฅ) โ ๐ โ โ) |
51 | 50, 24 | sylan2 286 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (1..^๐ฅ)) โ ((1 / (2โ๐)) ยท (๐บโ๐)) โ โ) |
52 | 48, 51 | fsumrecl 11409 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ฮฃ๐ โ (1..^๐ฅ)((1 / (2โ๐)) ยท (๐บโ๐)) โ โ) |
53 | 9 | a1i 9 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 2 โ
โ+) |
54 | 53, 46 | rpexpcld 10678 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (2โ๐ฅ) โ
โ+) |
55 | 54 | rpreccld 9707 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (1 / (2โ๐ฅ)) โ
โ+) |
56 | 55 | rpred 9696 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (1 / (2โ๐ฅ)) โ
โ) |
57 | 20 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ๐บ:โโถ{0, 1}) |
58 | 57, 3 | ffvelcdmd 5653 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (๐บโ๐ฅ) โ {0, 1}) |
59 | 19, 58 | sselid 3154 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (๐บโ๐ฅ) โ โ) |
60 | 56, 59 | remulcld 7988 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ((1 / (2โ๐ฅ)) ยท (๐บโ๐ฅ)) โ โ) |
61 | 14 | rpge0d 9700 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ 0 โค (1 /
(2โ๐))) |
62 | | 0le0 9008 |
. . . . . . . . . . . . 13
โข 0 โค
0 |
63 | | simpr 110 |
. . . . . . . . . . . . 13
โข ((((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โง (๐บโ๐) = 0) โ (๐บโ๐) = 0) |
64 | 62, 63 | breqtrrid 4042 |
. . . . . . . . . . . 12
โข ((((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โง (๐บโ๐) = 0) โ 0 โค (๐บโ๐)) |
65 | | 0le1 8438 |
. . . . . . . . . . . . 13
โข 0 โค
1 |
66 | | simpr 110 |
. . . . . . . . . . . . 13
โข ((((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โง (๐บโ๐) = 1) โ (๐บโ๐) = 1) |
67 | 65, 66 | breqtrrid 4042 |
. . . . . . . . . . . 12
โข ((((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โง (๐บโ๐) = 1) โ 0 โค (๐บโ๐)) |
68 | | elpri 3616 |
. . . . . . . . . . . . 13
โข ((๐บโ๐) โ {0, 1} โ ((๐บโ๐) = 0 โจ (๐บโ๐) = 1)) |
69 | 22, 68 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ ((๐บโ๐) = 0 โจ (๐บโ๐) = 1)) |
70 | 64, 67, 69 | mpjaodan 798 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ 0 โค (๐บโ๐)) |
71 | 15, 23, 61, 70 | mulge0d 8578 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ โ) โ 0 โค ((1 /
(2โ๐)) ยท (๐บโ๐))) |
72 | 50, 71 | sylan2 286 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (1..^๐ฅ)) โ 0 โค ((1 / (2โ๐)) ยท (๐บโ๐))) |
73 | 48, 51, 72 | fsumge0 11467 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 โค ฮฃ๐ โ (1..^๐ฅ)((1 / (2โ๐)) ยท (๐บโ๐))) |
74 | 55 | rpgt0d 9699 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 < (1 / (2โ๐ฅ))) |
75 | | simprr 531 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (๐บโ๐ฅ) = 1) |
76 | 75 | oveq2d 5891 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ((1 / (2โ๐ฅ)) ยท (๐บโ๐ฅ)) = ((1 / (2โ๐ฅ)) ยท 1)) |
77 | 56 | recnd 7986 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (1 / (2โ๐ฅ)) โ
โ) |
78 | 77 | mulridd 7974 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ((1 / (2โ๐ฅ)) ยท 1) = (1 /
(2โ๐ฅ))) |
79 | 76, 78 | eqtrd 2210 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ((1 / (2โ๐ฅ)) ยท (๐บโ๐ฅ)) = (1 / (2โ๐ฅ))) |
80 | 74, 79 | breqtrrd 4032 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 < ((1 / (2โ๐ฅ)) ยท (๐บโ๐ฅ))) |
81 | 52, 60, 73, 80 | addgegt0d 8476 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 < (ฮฃ๐ โ (1..^๐ฅ)((1 / (2โ๐)) ยท (๐บโ๐)) + ((1 / (2โ๐ฅ)) ยท (๐บโ๐ฅ)))) |
82 | | nfv 1528 |
. . . . . . . 8
โข
โฒ๐(๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) |
83 | | nfcv 2319 |
. . . . . . . 8
โข
โฒ๐((1 /
(2โ๐ฅ)) ยท (๐บโ๐ฅ)) |
84 | | fzonel 10160 |
. . . . . . . . 9
โข ยฌ
๐ฅ โ (1..^๐ฅ) |
85 | 84 | a1i 9 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ยฌ ๐ฅ โ (1..^๐ฅ)) |
86 | 50, 41 | sylan2 286 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (1..^๐ฅ)) โ ((1 / (2โ๐)) ยท (๐บโ๐)) โ โ) |
87 | | oveq2 5883 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (2โ๐) = (2โ๐ฅ)) |
88 | 87 | oveq2d 5891 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (1 / (2โ๐)) = (1 / (2โ๐ฅ))) |
89 | | fveq2 5516 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (๐บโ๐) = (๐บโ๐ฅ)) |
90 | 88, 89 | oveq12d 5893 |
. . . . . . . 8
โข (๐ = ๐ฅ โ ((1 / (2โ๐)) ยท (๐บโ๐)) = ((1 / (2โ๐ฅ)) ยท (๐บโ๐ฅ))) |
91 | 60 | recnd 7986 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ((1 / (2โ๐ฅ)) ยท (๐บโ๐ฅ)) โ โ) |
92 | 82, 83, 48, 3, 85, 86, 90, 91 | fsumsplitsn 11418 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ฮฃ๐ โ ((1..^๐ฅ) โช {๐ฅ})((1 / (2โ๐)) ยท (๐บโ๐)) = (ฮฃ๐ โ (1..^๐ฅ)((1 / (2โ๐)) ยท (๐บโ๐)) + ((1 / (2โ๐ฅ)) ยท (๐บโ๐ฅ)))) |
93 | 81, 92 | breqtrrd 4032 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 < ฮฃ๐ โ ((1..^๐ฅ) โช {๐ฅ})((1 / (2โ๐)) ยท (๐บโ๐))) |
94 | 3 | nncnd 8933 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ๐ฅ โ โ) |
95 | | 1cnd 7973 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 1 โ
โ) |
96 | 94, 95 | pncand 8269 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ((๐ฅ + 1) โ 1) = ๐ฅ) |
97 | 96 | oveq2d 5891 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (1...((๐ฅ + 1) โ 1)) = (1...๐ฅ)) |
98 | 3, 39 | eleqtrdi 2270 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ๐ฅ โ
(โคโฅโ1)) |
99 | | fzisfzounsn 10236 |
. . . . . . . . 9
โข (๐ฅ โ
(โคโฅโ1) โ (1...๐ฅ) = ((1..^๐ฅ) โช {๐ฅ})) |
100 | 98, 99 | syl 14 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (1...๐ฅ) = ((1..^๐ฅ) โช {๐ฅ})) |
101 | 97, 100 | eqtrd 2210 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ (1...((๐ฅ + 1) โ 1)) = ((1..^๐ฅ) โช {๐ฅ})) |
102 | 101 | sumeq1d 11374 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ฮฃ๐ โ (1...((๐ฅ + 1) โ 1))((1 / (2โ๐)) ยท (๐บโ๐)) = ฮฃ๐ โ ((1..^๐ฅ) โช {๐ฅ})((1 / (2โ๐)) ยท (๐บโ๐))) |
103 | 93, 102 | breqtrrd 4032 |
. . . . 5
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 < ฮฃ๐ โ (1...((๐ฅ + 1) โ 1))((1 /
(2โ๐)) ยท (๐บโ๐))) |
104 | 34, 15 | syldan 282 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ (1 /
(2โ๐)) โ
โ) |
105 | 34, 23 | syldan 282 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ (๐บโ๐) โ โ) |
106 | 34, 14 | syldan 282 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ (1 /
(2โ๐)) โ
โ+) |
107 | 106 | rpge0d 9700 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ 0 โค (1 /
(2โ๐))) |
108 | 34, 70 | syldan 282 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ 0 โค (๐บโ๐)) |
109 | 104, 105,
107, 108 | mulge0d 8578 |
. . . . . 6
โข (((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โง ๐ โ (โคโฅโ(๐ฅ + 1))) โ 0 โค ((1 /
(2โ๐)) ยท (๐บโ๐))) |
110 | 27, 5, 36, 35, 44, 109 | isumge0 11438 |
. . . . 5
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 โค ฮฃ๐ โ
(โคโฅโ(๐ฅ + 1))((1 / (2โ๐)) ยท (๐บโ๐))) |
111 | 26, 45, 103, 110 | addgtge0d 8477 |
. . . 4
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 < (ฮฃ๐ โ (1...((๐ฅ + 1) โ 1))((1 /
(2โ๐)) ยท (๐บโ๐)) + ฮฃ๐ โ (โคโฅโ(๐ฅ + 1))((1 / (2โ๐)) ยท (๐บโ๐)))) |
112 | 39, 27, 4, 40, 41, 38 | isumsplit 11499 |
. . . 4
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ ฮฃ๐ โ โ ((1 / (2โ๐)) ยท (๐บโ๐)) = (ฮฃ๐ โ (1...((๐ฅ + 1) โ 1))((1 / (2โ๐)) ยท (๐บโ๐)) + ฮฃ๐ โ (โคโฅโ(๐ฅ + 1))((1 / (2โ๐)) ยท (๐บโ๐)))) |
113 | 111, 112 | breqtrrd 4032 |
. . 3
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 < ฮฃ๐ โ โ ((1 /
(2โ๐)) ยท (๐บโ๐))) |
114 | | nconstwlpolem0.a |
. . 3
โข ๐ด = ฮฃ๐ โ โ ((1 / (2โ๐)) ยท (๐บโ๐)) |
115 | 113, 114 | breqtrrdi 4046 |
. 2
โข ((๐ โง (๐ฅ โ โ โง (๐บโ๐ฅ) = 1)) โ 0 < ๐ด) |
116 | 1, 115 | rexlimddv 2599 |
1
โข (๐ โ 0 < ๐ด) |