Step | Hyp | Ref
| Expression |
1 | | 0re 11216 |
. . . . 5
โข 0 โ
โ |
2 | | 1re 11214 |
. . . . 5
โข 1 โ
โ |
3 | | halfge0 12429 |
. . . . 5
โข 0 โค (1
/ 2) |
4 | | 1le1 11842 |
. . . . 5
โข 1 โค
1 |
5 | | iccss 13392 |
. . . . 5
โข (((0
โ โ โง 1 โ โ) โง (0 โค (1 / 2) โง 1 โค 1))
โ ((1 / 2)[,]1) โ (0[,]1)) |
6 | 1, 2, 3, 4, 5 | mp4an 692 |
. . . 4
โข ((1 /
2)[,]1) โ (0[,]1) |
7 | 6 | sseli 3979 |
. . 3
โข (๐ โ ((1 / 2)[,]1) โ
๐ โ
(0[,]1)) |
8 | | pcoval.2 |
. . . 4
โข (๐ โ ๐น โ (II Cn ๐ฝ)) |
9 | | pcoval.3 |
. . . 4
โข (๐ โ ๐บ โ (II Cn ๐ฝ)) |
10 | 8, 9 | pcovalg 24528 |
. . 3
โข ((๐ โง ๐ โ (0[,]1)) โ ((๐น(*๐โ๐ฝ)๐บ)โ๐) = if(๐ โค (1 / 2), (๐นโ(2 ยท ๐)), (๐บโ((2 ยท ๐) โ 1)))) |
11 | 7, 10 | sylan2 594 |
. 2
โข ((๐ โง ๐ โ ((1 / 2)[,]1)) โ ((๐น(*๐โ๐ฝ)๐บ)โ๐) = if(๐ โค (1 / 2), (๐นโ(2 ยท ๐)), (๐บโ((2 ยท ๐) โ 1)))) |
12 | | pcoval2.4 |
. . . . . . . 8
โข (๐ โ (๐นโ1) = (๐บโ0)) |
13 | 12 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ (๐นโ1) = (๐บโ0)) |
14 | | simprr 772 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ ๐ โค (1 / 2)) |
15 | | halfre 12426 |
. . . . . . . . . . . . . 14
โข (1 / 2)
โ โ |
16 | 15, 2 | elicc2i 13390 |
. . . . . . . . . . . . 13
โข (๐ โ ((1 / 2)[,]1) โ
(๐ โ โ โง (1
/ 2) โค ๐ โง ๐ โค 1)) |
17 | 16 | simp2bi 1147 |
. . . . . . . . . . . 12
โข (๐ โ ((1 / 2)[,]1) โ (1
/ 2) โค ๐) |
18 | 17 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ (1 / 2)
โค ๐) |
19 | 16 | simp1bi 1146 |
. . . . . . . . . . . . 13
โข (๐ โ ((1 / 2)[,]1) โ
๐ โ
โ) |
20 | 19 | ad2antrl 727 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ ๐ โ
โ) |
21 | | letri3 11299 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (1 / 2)
โ โ) โ (๐ =
(1 / 2) โ (๐ โค (1 /
2) โง (1 / 2) โค ๐))) |
22 | 20, 15, 21 | sylancl 587 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ (๐ = (1 / 2) โ (๐ โค (1 / 2) โง (1 / 2) โค
๐))) |
23 | 14, 18, 22 | mpbir2and 712 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ ๐ = (1 / 2)) |
24 | 23 | oveq2d 7425 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ (2
ยท ๐) = (2 ยท
(1 / 2))) |
25 | | 2cn 12287 |
. . . . . . . . . 10
โข 2 โ
โ |
26 | | 2ne0 12316 |
. . . . . . . . . 10
โข 2 โ
0 |
27 | 25, 26 | recidi 11945 |
. . . . . . . . 9
โข (2
ยท (1 / 2)) = 1 |
28 | 24, 27 | eqtrdi 2789 |
. . . . . . . 8
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ (2
ยท ๐) =
1) |
29 | 28 | fveq2d 6896 |
. . . . . . 7
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ (๐นโ(2 ยท ๐)) = (๐นโ1)) |
30 | 28 | oveq1d 7424 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ ((2
ยท ๐) โ 1) = (1
โ 1)) |
31 | | 1m1e0 12284 |
. . . . . . . . 9
โข (1
โ 1) = 0 |
32 | 30, 31 | eqtrdi 2789 |
. . . . . . . 8
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ ((2
ยท ๐) โ 1) =
0) |
33 | 32 | fveq2d 6896 |
. . . . . . 7
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ (๐บโ((2 ยท ๐) โ 1)) = (๐บโ0)) |
34 | 13, 29, 33 | 3eqtr4d 2783 |
. . . . . 6
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ (๐นโ(2 ยท ๐)) = (๐บโ((2 ยท ๐) โ 1))) |
35 | 34 | ifeq1d 4548 |
. . . . 5
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ if(๐ โค (1 / 2), (๐นโ(2 ยท ๐)), (๐บโ((2 ยท ๐) โ 1))) = if(๐ โค (1 / 2), (๐บโ((2 ยท ๐) โ 1)), (๐บโ((2 ยท ๐) โ 1)))) |
36 | | ifid 4569 |
. . . . 5
โข if(๐ โค (1 / 2), (๐บโ((2 ยท ๐) โ 1)), (๐บโ((2 ยท ๐) โ 1))) = (๐บโ((2 ยท ๐) โ 1)) |
37 | 35, 36 | eqtrdi 2789 |
. . . 4
โข ((๐ โง (๐ โ ((1 / 2)[,]1) โง ๐ โค (1 / 2))) โ if(๐ โค (1 / 2), (๐นโ(2 ยท ๐)), (๐บโ((2 ยท ๐) โ 1))) = (๐บโ((2 ยท ๐) โ 1))) |
38 | 37 | expr 458 |
. . 3
โข ((๐ โง ๐ โ ((1 / 2)[,]1)) โ (๐ โค (1 / 2) โ if(๐ โค (1 / 2), (๐นโ(2 ยท ๐)), (๐บโ((2 ยท ๐) โ 1))) = (๐บโ((2 ยท ๐) โ 1)))) |
39 | | iffalse 4538 |
. . 3
โข (ยฌ
๐ โค (1 / 2) โ
if(๐ โค (1 / 2), (๐นโ(2 ยท ๐)), (๐บโ((2 ยท ๐) โ 1))) = (๐บโ((2 ยท ๐) โ 1))) |
40 | 38, 39 | pm2.61d1 180 |
. 2
โข ((๐ โง ๐ โ ((1 / 2)[,]1)) โ if(๐ โค (1 / 2), (๐นโ(2 ยท ๐)), (๐บโ((2 ยท ๐) โ 1))) = (๐บโ((2 ยท ๐) โ 1))) |
41 | 11, 40 | eqtrd 2773 |
1
โข ((๐ โง ๐ โ ((1 / 2)[,]1)) โ ((๐น(*๐โ๐ฝ)๐บ)โ๐) = (๐บโ((2 ยท ๐) โ 1))) |