Step | Hyp | Ref
| Expression |
1 | | phtpcrel 24372 |
. 2
โข Rel (
โphโ๐ฝ) |
2 | | isphtpc 24373 |
. . . 4
โข (๐ฅ(
โphโ๐ฝ)๐ฆ โ (๐ฅ โ (II Cn ๐ฝ) โง ๐ฆ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โ โ
)) |
3 | 2 | simp2bi 1147 |
. . 3
โข (๐ฅ(
โphโ๐ฝ)๐ฆ โ ๐ฆ โ (II Cn ๐ฝ)) |
4 | 2 | simp1bi 1146 |
. . 3
โข (๐ฅ(
โphโ๐ฝ)๐ฆ โ ๐ฅ โ (II Cn ๐ฝ)) |
5 | 2 | simp3bi 1148 |
. . . . 5
โข (๐ฅ(
โphโ๐ฝ)๐ฆ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โ โ
) |
6 | | n0 4311 |
. . . . 5
โข ((๐ฅ(PHtpyโ๐ฝ)๐ฆ) โ โ
โ โ๐ ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) |
7 | 5, 6 | sylib 217 |
. . . 4
โข (๐ฅ(
โphโ๐ฝ)๐ฆ โ โ๐ ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) |
8 | 4 | adantr 482 |
. . . . . 6
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) โ ๐ฅ โ (II Cn ๐ฝ)) |
9 | 3 | adantr 482 |
. . . . . 6
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) โ ๐ฆ โ (II Cn ๐ฝ)) |
10 | | eqid 2737 |
. . . . . 6
โข (๐ข โ (0[,]1), ๐ฃ โ (0[,]1) โฆ (๐ข๐(1 โ ๐ฃ))) = (๐ข โ (0[,]1), ๐ฃ โ (0[,]1) โฆ (๐ข๐(1 โ ๐ฃ))) |
11 | | simpr 486 |
. . . . . 6
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) โ ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) |
12 | 8, 9, 10, 11 | phtpycom 24367 |
. . . . 5
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) โ (๐ข โ (0[,]1), ๐ฃ โ (0[,]1) โฆ (๐ข๐(1 โ ๐ฃ))) โ (๐ฆ(PHtpyโ๐ฝ)๐ฅ)) |
13 | 12 | ne0d 4300 |
. . . 4
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) โ (๐ฆ(PHtpyโ๐ฝ)๐ฅ) โ โ
) |
14 | 7, 13 | exlimddv 1939 |
. . 3
โข (๐ฅ(
โphโ๐ฝ)๐ฆ โ (๐ฆ(PHtpyโ๐ฝ)๐ฅ) โ โ
) |
15 | | isphtpc 24373 |
. . 3
โข (๐ฆ(
โphโ๐ฝ)๐ฅ โ (๐ฆ โ (II Cn ๐ฝ) โง ๐ฅ โ (II Cn ๐ฝ) โง (๐ฆ(PHtpyโ๐ฝ)๐ฅ) โ โ
)) |
16 | 3, 4, 14, 15 | syl3anbrc 1344 |
. 2
โข (๐ฅ(
โphโ๐ฝ)๐ฆ โ ๐ฆ( โphโ๐ฝ)๐ฅ) |
17 | 4 | adantr 482 |
. . 3
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ ๐ฅ โ (II Cn ๐ฝ)) |
18 | | simpr 486 |
. . . . 5
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ ๐ฆ( โphโ๐ฝ)๐ง) |
19 | | isphtpc 24373 |
. . . . 5
โข (๐ฆ(
โphโ๐ฝ)๐ง โ (๐ฆ โ (II Cn ๐ฝ) โง ๐ง โ (II Cn ๐ฝ) โง (๐ฆ(PHtpyโ๐ฝ)๐ง) โ โ
)) |
20 | 18, 19 | sylib 217 |
. . . 4
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ (๐ฆ โ (II Cn ๐ฝ) โง ๐ง โ (II Cn ๐ฝ) โง (๐ฆ(PHtpyโ๐ฝ)๐ง) โ โ
)) |
21 | 20 | simp2d 1144 |
. . 3
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ ๐ง โ (II Cn ๐ฝ)) |
22 | 5 | adantr 482 |
. . . . . 6
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โ โ
) |
23 | 22, 6 | sylib 217 |
. . . . 5
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ โ๐ ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) |
24 | 20 | simp3d 1145 |
. . . . . 6
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ (๐ฆ(PHtpyโ๐ฝ)๐ง) โ โ
) |
25 | | n0 4311 |
. . . . . 6
โข ((๐ฆ(PHtpyโ๐ฝ)๐ง) โ โ
โ โ๐ ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง)) |
26 | 24, 25 | sylib 217 |
. . . . 5
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ โ๐ ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง)) |
27 | | exdistrv 1960 |
. . . . 5
โข
(โ๐โ๐(๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง)) โ (โ๐ ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง โ๐ ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) |
28 | 23, 26, 27 | sylanbrc 584 |
. . . 4
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ โ๐โ๐(๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) |
29 | | eqid 2737 |
. . . . . . . 8
โข (๐ข โ (0[,]1), ๐ฃ โ (0[,]1) โฆ if(๐ฃ โค (1 / 2), (๐ข๐(2 ยท ๐ฃ)), (๐ข๐((2 ยท ๐ฃ) โ 1)))) = (๐ข โ (0[,]1), ๐ฃ โ (0[,]1) โฆ if(๐ฃ โค (1 / 2), (๐ข๐(2 ยท ๐ฃ)), (๐ข๐((2 ยท ๐ฃ) โ 1)))) |
30 | 17 | adantr 482 |
. . . . . . . 8
โข (((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โง (๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) โ ๐ฅ โ (II Cn ๐ฝ)) |
31 | 20 | simp1d 1143 |
. . . . . . . . 9
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ ๐ฆ โ (II Cn ๐ฝ)) |
32 | 31 | adantr 482 |
. . . . . . . 8
โข (((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โง (๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) โ ๐ฆ โ (II Cn ๐ฝ)) |
33 | 21 | adantr 482 |
. . . . . . . 8
โข (((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โง (๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) โ ๐ง โ (II Cn ๐ฝ)) |
34 | | simprl 770 |
. . . . . . . 8
โข (((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โง (๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) โ ๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ)) |
35 | | simprr 772 |
. . . . . . . 8
โข (((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โง (๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) โ ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง)) |
36 | 29, 30, 32, 33, 34, 35 | phtpycc 24370 |
. . . . . . 7
โข (((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โง (๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) โ (๐ข โ (0[,]1), ๐ฃ โ (0[,]1) โฆ if(๐ฃ โค (1 / 2), (๐ข๐(2 ยท ๐ฃ)), (๐ข๐((2 ยท ๐ฃ) โ 1)))) โ (๐ฅ(PHtpyโ๐ฝ)๐ง)) |
37 | 36 | ne0d 4300 |
. . . . . 6
โข (((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โง (๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง))) โ (๐ฅ(PHtpyโ๐ฝ)๐ง) โ โ
) |
38 | 37 | ex 414 |
. . . . 5
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ ((๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง)) โ (๐ฅ(PHtpyโ๐ฝ)๐ง) โ โ
)) |
39 | 38 | exlimdvv 1938 |
. . . 4
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ (โ๐โ๐(๐ โ (๐ฅ(PHtpyโ๐ฝ)๐ฆ) โง ๐ โ (๐ฆ(PHtpyโ๐ฝ)๐ง)) โ (๐ฅ(PHtpyโ๐ฝ)๐ง) โ โ
)) |
40 | 28, 39 | mpd 15 |
. . 3
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ (๐ฅ(PHtpyโ๐ฝ)๐ง) โ โ
) |
41 | | isphtpc 24373 |
. . 3
โข (๐ฅ(
โphโ๐ฝ)๐ง โ (๐ฅ โ (II Cn ๐ฝ) โง ๐ง โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ง) โ โ
)) |
42 | 17, 21, 40, 41 | syl3anbrc 1344 |
. 2
โข ((๐ฅ(
โphโ๐ฝ)๐ฆ โง ๐ฆ( โphโ๐ฝ)๐ง) โ ๐ฅ( โphโ๐ฝ)๐ง) |
43 | | eqid 2737 |
. . . . . . . 8
โข (๐ฆ โ (0[,]1), ๐ง โ (0[,]1) โฆ (๐ฅโ๐ฆ)) = (๐ฆ โ (0[,]1), ๐ง โ (0[,]1) โฆ (๐ฅโ๐ฆ)) |
44 | | id 22 |
. . . . . . . 8
โข (๐ฅ โ (II Cn ๐ฝ) โ ๐ฅ โ (II Cn ๐ฝ)) |
45 | 43, 44 | phtpyid 24368 |
. . . . . . 7
โข (๐ฅ โ (II Cn ๐ฝ) โ (๐ฆ โ (0[,]1), ๐ง โ (0[,]1) โฆ (๐ฅโ๐ฆ)) โ (๐ฅ(PHtpyโ๐ฝ)๐ฅ)) |
46 | 45 | ne0d 4300 |
. . . . . 6
โข (๐ฅ โ (II Cn ๐ฝ) โ (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
) |
47 | 46 | ancli 550 |
. . . . 5
โข (๐ฅ โ (II Cn ๐ฝ) โ (๐ฅ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
)) |
48 | 47 | pm4.71ri 562 |
. . . 4
โข (๐ฅ โ (II Cn ๐ฝ) โ ((๐ฅ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
) โง ๐ฅ โ (II Cn ๐ฝ))) |
49 | | df-3an 1090 |
. . . 4
โข ((๐ฅ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
โง ๐ฅ โ (II Cn ๐ฝ)) โ ((๐ฅ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
) โง ๐ฅ โ (II Cn ๐ฝ))) |
50 | | 3ancomb 1100 |
. . . 4
โข ((๐ฅ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
โง ๐ฅ โ (II Cn ๐ฝ)) โ (๐ฅ โ (II Cn ๐ฝ) โง ๐ฅ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
)) |
51 | 48, 49, 50 | 3bitr2i 299 |
. . 3
โข (๐ฅ โ (II Cn ๐ฝ) โ (๐ฅ โ (II Cn ๐ฝ) โง ๐ฅ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
)) |
52 | | isphtpc 24373 |
. . 3
โข (๐ฅ(
โphโ๐ฝ)๐ฅ โ (๐ฅ โ (II Cn ๐ฝ) โง ๐ฅ โ (II Cn ๐ฝ) โง (๐ฅ(PHtpyโ๐ฝ)๐ฅ) โ โ
)) |
53 | 51, 52 | bitr4i 278 |
. 2
โข (๐ฅ โ (II Cn ๐ฝ) โ ๐ฅ( โphโ๐ฝ)๐ฅ) |
54 | 1, 16, 42, 53 | iseri 8682 |
1
โข (
โphโ๐ฝ) Er (II Cn ๐ฝ) |