Step | Hyp | Ref
| Expression |
1 | | trilpolemclim.g |
. . . 4
โข ๐บ = (๐ โ โ โฆ ((1 / (2โ๐)) ยท (๐นโ๐))) |
2 | | oveq2 5883 |
. . . . . 6
โข (๐ = ๐ โ (2โ๐) = (2โ๐)) |
3 | 2 | oveq2d 5891 |
. . . . 5
โข (๐ = ๐ โ (1 / (2โ๐)) = (1 / (2โ๐))) |
4 | | fveq2 5516 |
. . . . 5
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
5 | 3, 4 | oveq12d 5893 |
. . . 4
โข (๐ = ๐ โ ((1 / (2โ๐)) ยท (๐นโ๐)) = ((1 / (2โ๐)) ยท (๐นโ๐))) |
6 | | simpr 110 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
7 | | 2rp 9658 |
. . . . . . . . 9
โข 2 โ
โ+ |
8 | 7 | a1i 9 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ 2 โ
โ+) |
9 | 6 | nnzd 9374 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ๐ โ โค) |
10 | 8, 9 | rpexpcld 10678 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (2โ๐) โ
โ+) |
11 | 10 | rpreccld 9707 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (1 / (2โ๐)) โ
โ+) |
12 | 11 | rpred 9696 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (1 / (2โ๐)) โ
โ) |
13 | | simpr 110 |
. . . . . . 7
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ (๐นโ๐) = 0) |
14 | | 0re 7957 |
. . . . . . 7
โข 0 โ
โ |
15 | 13, 14 | eqeltrdi 2268 |
. . . . . 6
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ (๐นโ๐) โ โ) |
16 | | simpr 110 |
. . . . . . 7
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ (๐นโ๐) = 1) |
17 | | 1re 7956 |
. . . . . . 7
โข 1 โ
โ |
18 | 16, 17 | eqeltrdi 2268 |
. . . . . 6
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ (๐นโ๐) โ โ) |
19 | | trilpolemgt1.f |
. . . . . . . 8
โข (๐ โ ๐น:โโถ{0, 1}) |
20 | 19 | ffvelcdmda 5652 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ {0, 1}) |
21 | | elpri 3616 |
. . . . . . 7
โข ((๐นโ๐) โ {0, 1} โ ((๐นโ๐) = 0 โจ (๐นโ๐) = 1)) |
22 | 20, 21 | syl 14 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐นโ๐) = 0 โจ (๐นโ๐) = 1)) |
23 | 15, 18, 22 | mpjaodan 798 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
24 | 12, 23 | remulcld 7988 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ((1 / (2โ๐)) ยท (๐นโ๐)) โ โ) |
25 | 1, 5, 6, 24 | fvmptd3 5610 |
. . 3
โข ((๐ โง ๐ โ โ) โ (๐บโ๐) = ((1 / (2โ๐)) ยท (๐นโ๐))) |
26 | 25, 24 | eqeltrd 2254 |
. 2
โข ((๐ โง ๐ โ โ) โ (๐บโ๐) โ โ) |
27 | 11 | rpge0d 9700 |
. . . 4
โข ((๐ โง ๐ โ โ) โ 0 โค (1 /
(2โ๐))) |
28 | | 0le0 9008 |
. . . . . 6
โข 0 โค
0 |
29 | 28, 13 | breqtrrid 4042 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ 0 โค (๐นโ๐)) |
30 | | 0le1 8438 |
. . . . . 6
โข 0 โค
1 |
31 | 30, 16 | breqtrrid 4042 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ 0 โค (๐นโ๐)) |
32 | 29, 31, 22 | mpjaodan 798 |
. . . 4
โข ((๐ โง ๐ โ โ) โ 0 โค (๐นโ๐)) |
33 | 12, 23, 27, 32 | mulge0d 8578 |
. . 3
โข ((๐ โง ๐ โ โ) โ 0 โค ((1 /
(2โ๐)) ยท (๐นโ๐))) |
34 | 33, 25 | breqtrrd 4032 |
. 2
โข ((๐ โง ๐ โ โ) โ 0 โค (๐บโ๐)) |
35 | 25 | adantr 276 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ (๐บโ๐) = ((1 / (2โ๐)) ยท (๐นโ๐))) |
36 | 13 | oveq2d 5891 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ ((1 / (2โ๐)) ยท (๐นโ๐)) = ((1 / (2โ๐)) ยท 0)) |
37 | 11 | rpcnd 9698 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (1 / (2โ๐)) โ
โ) |
38 | 37 | adantr 276 |
. . . . . 6
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ (1 / (2โ๐)) โ โ) |
39 | 38 | mul01d 8350 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ ((1 / (2โ๐)) ยท 0) =
0) |
40 | 35, 36, 39 | 3eqtrd 2214 |
. . . 4
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ (๐บโ๐) = 0) |
41 | 27 | adantr 276 |
. . . 4
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ 0 โค (1 / (2โ๐))) |
42 | 40, 41 | eqbrtrd 4026 |
. . 3
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 0) โ (๐บโ๐) โค (1 / (2โ๐))) |
43 | 25 | adantr 276 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ (๐บโ๐) = ((1 / (2โ๐)) ยท (๐นโ๐))) |
44 | 16 | oveq2d 5891 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ ((1 / (2โ๐)) ยท (๐นโ๐)) = ((1 / (2โ๐)) ยท 1)) |
45 | 37 | adantr 276 |
. . . . . 6
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ (1 / (2โ๐)) โ โ) |
46 | 45 | mulridd 7974 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ ((1 / (2โ๐)) ยท 1) = (1 /
(2โ๐))) |
47 | 43, 44, 46 | 3eqtrd 2214 |
. . . 4
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ (๐บโ๐) = (1 / (2โ๐))) |
48 | 12 | adantr 276 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ (1 / (2โ๐)) โ โ) |
49 | 48 | leidd 8471 |
. . . 4
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ (1 / (2โ๐)) โค (1 / (2โ๐))) |
50 | 47, 49 | eqbrtrd 4026 |
. . 3
โข (((๐ โง ๐ โ โ) โง (๐นโ๐) = 1) โ (๐บโ๐) โค (1 / (2โ๐))) |
51 | 42, 50, 22 | mpjaodan 798 |
. 2
โข ((๐ โง ๐ โ โ) โ (๐บโ๐) โค (1 / (2โ๐))) |
52 | 26, 34, 51 | cvgcmp2n 14784 |
1
โข (๐ โ seq1( + , ๐บ) โ dom โ
) |