Step | Hyp | Ref
| Expression |
1 | | pcohtpy.5 |
. . . . 5
β’ (π β πΉ( βphβπ½)π») |
2 | | isphtpc 24501 |
. . . . 5
β’ (πΉ(
βphβπ½)π» β (πΉ β (II Cn π½) β§ π» β (II Cn π½) β§ (πΉ(PHtpyβπ½)π») β β
)) |
3 | 1, 2 | sylib 217 |
. . . 4
β’ (π β (πΉ β (II Cn π½) β§ π» β (II Cn π½) β§ (πΉ(PHtpyβπ½)π») β β
)) |
4 | 3 | simp1d 1142 |
. . 3
β’ (π β πΉ β (II Cn π½)) |
5 | | pcohtpy.6 |
. . . . 5
β’ (π β πΊ( βphβπ½)πΎ) |
6 | | isphtpc 24501 |
. . . . 5
β’ (πΊ(
βphβπ½)πΎ β (πΊ β (II Cn π½) β§ πΎ β (II Cn π½) β§ (πΊ(PHtpyβπ½)πΎ) β β
)) |
7 | 5, 6 | sylib 217 |
. . . 4
β’ (π β (πΊ β (II Cn π½) β§ πΎ β (II Cn π½) β§ (πΊ(PHtpyβπ½)πΎ) β β
)) |
8 | 7 | simp1d 1142 |
. . 3
β’ (π β πΊ β (II Cn π½)) |
9 | | pcohtpy.4 |
. . 3
β’ (π β (πΉβ1) = (πΊβ0)) |
10 | 4, 8, 9 | pcocn 24524 |
. 2
β’ (π β (πΉ(*πβπ½)πΊ) β (II Cn π½)) |
11 | 3 | simp2d 1143 |
. . 3
β’ (π β π» β (II Cn π½)) |
12 | 7 | simp2d 1143 |
. . 3
β’ (π β πΎ β (II Cn π½)) |
13 | | pcohtpylem.8 |
. . . . . 6
β’ (π β π β (πΉ(PHtpyβπ½)π»)) |
14 | 4, 11, 13 | phtpy01 24492 |
. . . . 5
β’ (π β ((πΉβ0) = (π»β0) β§ (πΉβ1) = (π»β1))) |
15 | 14 | simprd 496 |
. . . 4
β’ (π β (πΉβ1) = (π»β1)) |
16 | | pcohtpylem.9 |
. . . . . 6
β’ (π β π β (πΊ(PHtpyβπ½)πΎ)) |
17 | 8, 12, 16 | phtpy01 24492 |
. . . . 5
β’ (π β ((πΊβ0) = (πΎβ0) β§ (πΊβ1) = (πΎβ1))) |
18 | 17 | simpld 495 |
. . . 4
β’ (π β (πΊβ0) = (πΎβ0)) |
19 | 9, 15, 18 | 3eqtr3d 2780 |
. . 3
β’ (π β (π»β1) = (πΎβ0)) |
20 | 11, 12, 19 | pcocn 24524 |
. 2
β’ (π β (π»(*πβπ½)πΎ) β (II Cn π½)) |
21 | | pcohtpylem.7 |
. . 3
β’ π = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦))) |
22 | | eqid 2732 |
. . . 4
β’
(topGenβran (,)) = (topGenβran (,)) |
23 | | eqid 2732 |
. . . 4
β’
((topGenβran (,)) βΎt (0[,](1 / 2))) =
((topGenβran (,)) βΎt (0[,](1 / 2))) |
24 | | eqid 2732 |
. . . 4
β’
((topGenβran (,)) βΎt ((1 / 2)[,]1)) =
((topGenβran (,)) βΎt ((1 / 2)[,]1)) |
25 | | dfii2 24389 |
. . . 4
β’ II =
((topGenβran (,)) βΎt (0[,]1)) |
26 | | 0red 11213 |
. . . 4
β’ (π β 0 β
β) |
27 | | 1red 11211 |
. . . 4
β’ (π β 1 β
β) |
28 | | halfre 12422 |
. . . . . 6
β’ (1 / 2)
β β |
29 | | halfge0 12425 |
. . . . . 6
β’ 0 β€ (1
/ 2) |
30 | | 1re 11210 |
. . . . . . 7
β’ 1 β
β |
31 | | halflt1 12426 |
. . . . . . 7
β’ (1 / 2)
< 1 |
32 | 28, 30, 31 | ltleii 11333 |
. . . . . 6
β’ (1 / 2)
β€ 1 |
33 | | elicc01 13439 |
. . . . . 6
β’ ((1 / 2)
β (0[,]1) β ((1 / 2) β β β§ 0 β€ (1 / 2) β§ (1 /
2) β€ 1)) |
34 | 28, 29, 32, 33 | mpbir3an 1341 |
. . . . 5
β’ (1 / 2)
β (0[,]1) |
35 | 34 | a1i 11 |
. . . 4
β’ (π β (1 / 2) β
(0[,]1)) |
36 | | iitopon 24386 |
. . . . 5
β’ II β
(TopOnβ(0[,]1)) |
37 | 36 | a1i 11 |
. . . 4
β’ (π β II β
(TopOnβ(0[,]1))) |
38 | 9 | adantr 481 |
. . . . . 6
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β (πΉβ1) = (πΊβ0)) |
39 | 4, 11, 13 | phtpyi 24491 |
. . . . . . . 8
β’ ((π β§ π¦ β (0[,]1)) β ((0ππ¦) = (πΉβ0) β§ (1ππ¦) = (πΉβ1))) |
40 | 39 | simprd 496 |
. . . . . . 7
β’ ((π β§ π¦ β (0[,]1)) β (1ππ¦) = (πΉβ1)) |
41 | 40 | adantrl 714 |
. . . . . 6
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β (1ππ¦) = (πΉβ1)) |
42 | 8, 12, 16 | phtpyi 24491 |
. . . . . . . 8
β’ ((π β§ π¦ β (0[,]1)) β ((0ππ¦) = (πΊβ0) β§ (1ππ¦) = (πΊβ1))) |
43 | 42 | simpld 495 |
. . . . . . 7
β’ ((π β§ π¦ β (0[,]1)) β (0ππ¦) = (πΊβ0)) |
44 | 43 | adantrl 714 |
. . . . . 6
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β (0ππ¦) = (πΊβ0)) |
45 | 38, 41, 44 | 3eqtr4d 2782 |
. . . . 5
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β (1ππ¦) = (0ππ¦)) |
46 | | simprl 769 |
. . . . . . . 8
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β π₯ = (1 / 2)) |
47 | 46 | oveq2d 7421 |
. . . . . . 7
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β (2 Β· π₯) = (2 Β· (1 /
2))) |
48 | | 2cn 12283 |
. . . . . . . 8
β’ 2 β
β |
49 | | 2ne0 12312 |
. . . . . . . 8
β’ 2 β
0 |
50 | 48, 49 | recidi 11941 |
. . . . . . 7
β’ (2
Β· (1 / 2)) = 1 |
51 | 47, 50 | eqtrdi 2788 |
. . . . . 6
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β (2 Β· π₯) = 1) |
52 | 51 | oveq1d 7420 |
. . . . 5
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β ((2 Β· π₯)ππ¦) = (1ππ¦)) |
53 | 51 | oveq1d 7420 |
. . . . . . 7
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β ((2 Β· π₯) β 1) = (1 β
1)) |
54 | | 1m1e0 12280 |
. . . . . . 7
β’ (1
β 1) = 0 |
55 | 53, 54 | eqtrdi 2788 |
. . . . . 6
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β ((2 Β· π₯) β 1) =
0) |
56 | 55 | oveq1d 7420 |
. . . . 5
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β (((2 Β· π₯) β 1)ππ¦) = (0ππ¦)) |
57 | 45, 52, 56 | 3eqtr4d 2782 |
. . . 4
β’ ((π β§ (π₯ = (1 / 2) β§ π¦ β (0[,]1))) β ((2 Β· π₯)ππ¦) = (((2 Β· π₯) β 1)ππ¦)) |
58 | | retopon 24271 |
. . . . . . 7
β’
(topGenβran (,)) β (TopOnββ) |
59 | | 0re 11212 |
. . . . . . . 8
β’ 0 β
β |
60 | | iccssre 13402 |
. . . . . . . 8
β’ ((0
β β β§ (1 / 2) β β) β (0[,](1 / 2)) β
β) |
61 | 59, 28, 60 | mp2an 690 |
. . . . . . 7
β’ (0[,](1 /
2)) β β |
62 | | resttopon 22656 |
. . . . . . 7
β’
(((topGenβran (,)) β (TopOnββ) β§ (0[,](1 /
2)) β β) β ((topGenβran (,)) βΎt (0[,](1
/ 2))) β (TopOnβ(0[,](1 / 2)))) |
63 | 58, 61, 62 | mp2an 690 |
. . . . . 6
β’
((topGenβran (,)) βΎt (0[,](1 / 2))) β
(TopOnβ(0[,](1 / 2))) |
64 | 63 | a1i 11 |
. . . . 5
β’ (π β ((topGenβran (,))
βΎt (0[,](1 / 2))) β (TopOnβ(0[,](1 /
2)))) |
65 | 64, 37 | cnmpt1st 23163 |
. . . . . 6
β’ (π β (π₯ β (0[,](1 / 2)), π¦ β (0[,]1) β¦ π₯) β ((((topGenβran (,))
βΎt (0[,](1 / 2))) Γt II) Cn
((topGenβran (,)) βΎt (0[,](1 / 2))))) |
66 | 23 | iihalf1cn 24439 |
. . . . . . 7
β’ (π§ β (0[,](1 / 2)) β¦ (2
Β· π§)) β
(((topGenβran (,)) βΎt (0[,](1 / 2))) Cn
II) |
67 | 66 | a1i 11 |
. . . . . 6
β’ (π β (π§ β (0[,](1 / 2)) β¦ (2 Β·
π§)) β
(((topGenβran (,)) βΎt (0[,](1 / 2))) Cn
II)) |
68 | | oveq2 7413 |
. . . . . 6
β’ (π§ = π₯ β (2 Β· π§) = (2 Β· π₯)) |
69 | 64, 37, 65, 64, 67, 68 | cnmpt21 23166 |
. . . . 5
β’ (π β (π₯ β (0[,](1 / 2)), π¦ β (0[,]1) β¦ (2 Β· π₯)) β ((((topGenβran
(,)) βΎt (0[,](1 / 2))) Γt II) Cn
II)) |
70 | 64, 37 | cnmpt2nd 23164 |
. . . . 5
β’ (π β (π₯ β (0[,](1 / 2)), π¦ β (0[,]1) β¦ π¦) β ((((topGenβran (,))
βΎt (0[,](1 / 2))) Γt II) Cn
II)) |
71 | 4, 11 | phtpycn 24490 |
. . . . . 6
β’ (π β (πΉ(PHtpyβπ½)π») β ((II Γt II) Cn
π½)) |
72 | 71, 13 | sseldd 3982 |
. . . . 5
β’ (π β π β ((II Γt II) Cn
π½)) |
73 | 64, 37, 69, 70, 72 | cnmpt22f 23170 |
. . . 4
β’ (π β (π₯ β (0[,](1 / 2)), π¦ β (0[,]1) β¦ ((2 Β· π₯)ππ¦)) β ((((topGenβran (,))
βΎt (0[,](1 / 2))) Γt II) Cn π½)) |
74 | | iccssre 13402 |
. . . . . . . 8
β’ (((1 / 2)
β β β§ 1 β β) β ((1 / 2)[,]1) β
β) |
75 | 28, 30, 74 | mp2an 690 |
. . . . . . 7
β’ ((1 /
2)[,]1) β β |
76 | | resttopon 22656 |
. . . . . . 7
β’
(((topGenβran (,)) β (TopOnββ) β§ ((1 /
2)[,]1) β β) β ((topGenβran (,)) βΎt ((1
/ 2)[,]1)) β (TopOnβ((1 / 2)[,]1))) |
77 | 58, 75, 76 | mp2an 690 |
. . . . . 6
β’
((topGenβran (,)) βΎt ((1 / 2)[,]1)) β
(TopOnβ((1 / 2)[,]1)) |
78 | 77 | a1i 11 |
. . . . 5
β’ (π β ((topGenβran (,))
βΎt ((1 / 2)[,]1)) β (TopOnβ((1 /
2)[,]1))) |
79 | 78, 37 | cnmpt1st 23163 |
. . . . . 6
β’ (π β (π₯ β ((1 / 2)[,]1), π¦ β (0[,]1) β¦ π₯) β ((((topGenβran (,))
βΎt ((1 / 2)[,]1)) Γt II) Cn
((topGenβran (,)) βΎt ((1 / 2)[,]1)))) |
80 | 24 | iihalf2cn 24441 |
. . . . . . 7
β’ (π§ β ((1 / 2)[,]1) β¦
((2 Β· π§) β 1))
β (((topGenβran (,)) βΎt ((1 / 2)[,]1)) Cn
II) |
81 | 80 | a1i 11 |
. . . . . 6
β’ (π β (π§ β ((1 / 2)[,]1) β¦ ((2 Β·
π§) β 1)) β
(((topGenβran (,)) βΎt ((1 / 2)[,]1)) Cn
II)) |
82 | 68 | oveq1d 7420 |
. . . . . 6
β’ (π§ = π₯ β ((2 Β· π§) β 1) = ((2 Β· π₯) β 1)) |
83 | 78, 37, 79, 78, 81, 82 | cnmpt21 23166 |
. . . . 5
β’ (π β (π₯ β ((1 / 2)[,]1), π¦ β (0[,]1) β¦ ((2 Β· π₯) β 1)) β
((((topGenβran (,)) βΎt ((1 / 2)[,]1))
Γt II) Cn II)) |
84 | 78, 37 | cnmpt2nd 23164 |
. . . . 5
β’ (π β (π₯ β ((1 / 2)[,]1), π¦ β (0[,]1) β¦ π¦) β ((((topGenβran (,))
βΎt ((1 / 2)[,]1)) Γt II) Cn
II)) |
85 | 8, 12 | phtpycn 24490 |
. . . . . 6
β’ (π β (πΊ(PHtpyβπ½)πΎ) β ((II Γt II) Cn
π½)) |
86 | 85, 16 | sseldd 3982 |
. . . . 5
β’ (π β π β ((II Γt II) Cn
π½)) |
87 | 78, 37, 83, 84, 86 | cnmpt22f 23170 |
. . . 4
β’ (π β (π₯ β ((1 / 2)[,]1), π¦ β (0[,]1) β¦ (((2 Β· π₯) β 1)ππ¦)) β ((((topGenβran (,))
βΎt ((1 / 2)[,]1)) Γt II) Cn π½)) |
88 | 22, 23, 24, 25, 26, 27, 35, 37, 57, 73, 87 | cnmpopc 24435 |
. . 3
β’ (π β (π₯ β (0[,]1), π¦ β (0[,]1) β¦ if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦))) β ((II Γt II) Cn
π½)) |
89 | 21, 88 | eqeltrid 2837 |
. 2
β’ (π β π β ((II Γt II) Cn
π½)) |
90 | | simpll 765 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β π) |
91 | | elii1 24442 |
. . . . . . . 8
β’ (π β (0[,](1 / 2)) β
(π β (0[,]1) β§
π β€ (1 /
2))) |
92 | | iihalf1 24438 |
. . . . . . . 8
β’ (π β (0[,](1 / 2)) β (2
Β· π ) β
(0[,]1)) |
93 | 91, 92 | sylbir 234 |
. . . . . . 7
β’ ((π β (0[,]1) β§ π β€ (1 / 2)) β (2
Β· π ) β
(0[,]1)) |
94 | 93 | adantll 712 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β (2 Β· π ) β
(0[,]1)) |
95 | 4, 11 | phtpyhtpy 24489 |
. . . . . . . 8
β’ (π β (πΉ(PHtpyβπ½)π») β (πΉ(II Htpy π½)π»)) |
96 | 95, 13 | sseldd 3982 |
. . . . . . 7
β’ (π β π β (πΉ(II Htpy π½)π»)) |
97 | 37, 4, 11, 96 | htpyi 24481 |
. . . . . 6
β’ ((π β§ (2 Β· π ) β (0[,]1)) β (((2
Β· π )π0) = (πΉβ(2 Β· π )) β§ ((2 Β· π )π1) = (π»β(2 Β· π )))) |
98 | 90, 94, 97 | syl2anc 584 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β (((2 Β· π )π0) = (πΉβ(2 Β· π )) β§ ((2 Β· π )π1) = (π»β(2 Β· π )))) |
99 | 98 | simpld 495 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β ((2 Β· π )π0) = (πΉβ(2 Β· π ))) |
100 | | simpll 765 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β π) |
101 | | elii2 24443 |
. . . . . . . 8
β’ ((π β (0[,]1) β§ Β¬
π β€ (1 / 2)) β
π β ((1 /
2)[,]1)) |
102 | 101 | adantll 712 |
. . . . . . 7
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β π β ((1 /
2)[,]1)) |
103 | | iihalf2 24440 |
. . . . . . 7
β’ (π β ((1 / 2)[,]1) β ((2
Β· π ) β 1)
β (0[,]1)) |
104 | 102, 103 | syl 17 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β ((2
Β· π ) β 1)
β (0[,]1)) |
105 | 8, 12 | phtpyhtpy 24489 |
. . . . . . . 8
β’ (π β (πΊ(PHtpyβπ½)πΎ) β (πΊ(II Htpy π½)πΎ)) |
106 | 105, 16 | sseldd 3982 |
. . . . . . 7
β’ (π β π β (πΊ(II Htpy π½)πΎ)) |
107 | 37, 8, 12, 106 | htpyi 24481 |
. . . . . 6
β’ ((π β§ ((2 Β· π ) β 1) β (0[,]1))
β ((((2 Β· π )
β 1)π0) = (πΊβ((2 Β· π ) β 1)) β§ (((2
Β· π ) β 1)π1) = (πΎβ((2 Β· π ) β 1)))) |
108 | 100, 104,
107 | syl2anc 584 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β ((((2
Β· π ) β 1)π0) = (πΊβ((2 Β· π ) β 1)) β§ (((2 Β· π ) β 1)π1) = (πΎβ((2 Β· π ) β 1)))) |
109 | 108 | simpld 495 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β (((2
Β· π ) β 1)π0) = (πΊβ((2 Β· π ) β 1))) |
110 | 99, 109 | ifeq12da 4560 |
. . 3
β’ ((π β§ π β (0[,]1)) β if(π β€ (1 / 2), ((2 Β· π )π0), (((2 Β· π ) β 1)π0)) = if(π β€ (1 / 2), (πΉβ(2 Β· π )), (πΊβ((2 Β· π ) β 1)))) |
111 | | simpr 485 |
. . . 4
β’ ((π β§ π β (0[,]1)) β π β (0[,]1)) |
112 | | 0elunit 13442 |
. . . 4
β’ 0 β
(0[,]1) |
113 | | simpl 483 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = 0) β π₯ = π ) |
114 | 113 | breq1d 5157 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = 0) β (π₯ β€ (1 / 2) β π β€ (1 / 2))) |
115 | 113 | oveq2d 7421 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = 0) β (2 Β· π₯) = (2 Β· π )) |
116 | | simpr 485 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = 0) β π¦ = 0) |
117 | 115, 116 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = 0) β ((2 Β· π₯)ππ¦) = ((2 Β· π )π0)) |
118 | 115 | oveq1d 7420 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = 0) β ((2 Β· π₯) β 1) = ((2 Β· π ) β 1)) |
119 | 118, 116 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = 0) β (((2 Β· π₯) β 1)ππ¦) = (((2 Β· π ) β 1)π0)) |
120 | 114, 117,
119 | ifbieq12d 4555 |
. . . . 5
β’ ((π₯ = π β§ π¦ = 0) β if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦)) = if(π β€ (1 / 2), ((2 Β· π )π0), (((2 Β· π ) β 1)π0))) |
121 | | ovex 7438 |
. . . . . 6
β’ ((2
Β· π )π0) β V |
122 | | ovex 7438 |
. . . . . 6
β’ (((2
Β· π ) β 1)π0) β V |
123 | 121, 122 | ifex 4577 |
. . . . 5
β’ if(π β€ (1 / 2), ((2 Β·
π )π0), (((2 Β· π ) β 1)π0)) β V |
124 | 120, 21, 123 | ovmpoa 7559 |
. . . 4
β’ ((π β (0[,]1) β§ 0 β
(0[,]1)) β (π π0) = if(π β€ (1 / 2), ((2 Β· π )π0), (((2 Β· π ) β 1)π0))) |
125 | 111, 112,
124 | sylancl 586 |
. . 3
β’ ((π β§ π β (0[,]1)) β (π π0) = if(π β€ (1 / 2), ((2 Β· π )π0), (((2 Β· π ) β 1)π0))) |
126 | 4, 8 | pcovalg 24519 |
. . 3
β’ ((π β§ π β (0[,]1)) β ((πΉ(*πβπ½)πΊ)βπ ) = if(π β€ (1 / 2), (πΉβ(2 Β· π )), (πΊβ((2 Β· π ) β 1)))) |
127 | 110, 125,
126 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π β (0[,]1)) β (π π0) = ((πΉ(*πβπ½)πΊ)βπ )) |
128 | 98 | simprd 496 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β ((2 Β· π )π1) = (π»β(2 Β· π ))) |
129 | 108 | simprd 496 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β (((2
Β· π ) β 1)π1) = (πΎβ((2 Β· π ) β 1))) |
130 | 128, 129 | ifeq12da 4560 |
. . 3
β’ ((π β§ π β (0[,]1)) β if(π β€ (1 / 2), ((2 Β· π )π1), (((2 Β· π ) β 1)π1)) = if(π β€ (1 / 2), (π»β(2 Β· π )), (πΎβ((2 Β· π ) β 1)))) |
131 | | 1elunit 13443 |
. . . 4
β’ 1 β
(0[,]1) |
132 | | simpl 483 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = 1) β π₯ = π ) |
133 | 132 | breq1d 5157 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = 1) β (π₯ β€ (1 / 2) β π β€ (1 / 2))) |
134 | 132 | oveq2d 7421 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = 1) β (2 Β· π₯) = (2 Β· π )) |
135 | | simpr 485 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = 1) β π¦ = 1) |
136 | 134, 135 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = 1) β ((2 Β· π₯)ππ¦) = ((2 Β· π )π1)) |
137 | 134 | oveq1d 7420 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = 1) β ((2 Β· π₯) β 1) = ((2 Β· π ) β 1)) |
138 | 137, 135 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = 1) β (((2 Β· π₯) β 1)ππ¦) = (((2 Β· π ) β 1)π1)) |
139 | 133, 136,
138 | ifbieq12d 4555 |
. . . . 5
β’ ((π₯ = π β§ π¦ = 1) β if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦)) = if(π β€ (1 / 2), ((2 Β· π )π1), (((2 Β· π ) β 1)π1))) |
140 | | ovex 7438 |
. . . . . 6
β’ ((2
Β· π )π1) β V |
141 | | ovex 7438 |
. . . . . 6
β’ (((2
Β· π ) β 1)π1) β V |
142 | 140, 141 | ifex 4577 |
. . . . 5
β’ if(π β€ (1 / 2), ((2 Β·
π )π1), (((2 Β· π ) β 1)π1)) β V |
143 | 139, 21, 142 | ovmpoa 7559 |
. . . 4
β’ ((π β (0[,]1) β§ 1 β
(0[,]1)) β (π π1) = if(π β€ (1 / 2), ((2 Β· π )π1), (((2 Β· π ) β 1)π1))) |
144 | 111, 131,
143 | sylancl 586 |
. . 3
β’ ((π β§ π β (0[,]1)) β (π π1) = if(π β€ (1 / 2), ((2 Β· π )π1), (((2 Β· π ) β 1)π1))) |
145 | 11, 12 | pcovalg 24519 |
. . 3
β’ ((π β§ π β (0[,]1)) β ((π»(*πβπ½)πΎ)βπ ) = if(π β€ (1 / 2), (π»β(2 Β· π )), (πΎβ((2 Β· π ) β 1)))) |
146 | 130, 144,
145 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π β (0[,]1)) β (π π1) = ((π»(*πβπ½)πΎ)βπ )) |
147 | 4, 11, 13 | phtpyi 24491 |
. . . 4
β’ ((π β§ π β (0[,]1)) β ((0ππ ) = (πΉβ0) β§ (1ππ ) = (πΉβ1))) |
148 | 147 | simpld 495 |
. . 3
β’ ((π β§ π β (0[,]1)) β (0ππ ) = (πΉβ0)) |
149 | | simpl 483 |
. . . . . . . 8
β’ ((π₯ = 0 β§ π¦ = π ) β π₯ = 0) |
150 | 149, 29 | eqbrtrdi 5186 |
. . . . . . 7
β’ ((π₯ = 0 β§ π¦ = π ) β π₯ β€ (1 / 2)) |
151 | 150 | iftrued 4535 |
. . . . . 6
β’ ((π₯ = 0 β§ π¦ = π ) β if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦)) = ((2 Β· π₯)ππ¦)) |
152 | 149 | oveq2d 7421 |
. . . . . . . 8
β’ ((π₯ = 0 β§ π¦ = π ) β (2 Β· π₯) = (2 Β· 0)) |
153 | | 2t0e0 12377 |
. . . . . . . 8
β’ (2
Β· 0) = 0 |
154 | 152, 153 | eqtrdi 2788 |
. . . . . . 7
β’ ((π₯ = 0 β§ π¦ = π ) β (2 Β· π₯) = 0) |
155 | | simpr 485 |
. . . . . . 7
β’ ((π₯ = 0 β§ π¦ = π ) β π¦ = π ) |
156 | 154, 155 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = 0 β§ π¦ = π ) β ((2 Β· π₯)ππ¦) = (0ππ )) |
157 | 151, 156 | eqtrd 2772 |
. . . . 5
β’ ((π₯ = 0 β§ π¦ = π ) β if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦)) = (0ππ )) |
158 | | ovex 7438 |
. . . . 5
β’ (0ππ ) β V |
159 | 157, 21, 158 | ovmpoa 7559 |
. . . 4
β’ ((0
β (0[,]1) β§ π
β (0[,]1)) β (0ππ ) = (0ππ )) |
160 | 112, 111,
159 | sylancr 587 |
. . 3
β’ ((π β§ π β (0[,]1)) β (0ππ ) = (0ππ )) |
161 | 4, 8 | pco0 24521 |
. . . 4
β’ (π β ((πΉ(*πβπ½)πΊ)β0) = (πΉβ0)) |
162 | 161 | adantr 481 |
. . 3
β’ ((π β§ π β (0[,]1)) β ((πΉ(*πβπ½)πΊ)β0) = (πΉβ0)) |
163 | 148, 160,
162 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π β (0[,]1)) β (0ππ ) = ((πΉ(*πβπ½)πΊ)β0)) |
164 | 8, 12, 16 | phtpyi 24491 |
. . . 4
β’ ((π β§ π β (0[,]1)) β ((0ππ ) = (πΊβ0) β§ (1ππ ) = (πΊβ1))) |
165 | 164 | simprd 496 |
. . 3
β’ ((π β§ π β (0[,]1)) β (1ππ ) = (πΊβ1)) |
166 | 28, 30 | ltnlei 11331 |
. . . . . . . . 9
β’ ((1 / 2)
< 1 β Β¬ 1 β€ (1 / 2)) |
167 | 31, 166 | mpbi 229 |
. . . . . . . 8
β’ Β¬ 1
β€ (1 / 2) |
168 | | simpl 483 |
. . . . . . . . 9
β’ ((π₯ = 1 β§ π¦ = π ) β π₯ = 1) |
169 | 168 | breq1d 5157 |
. . . . . . . 8
β’ ((π₯ = 1 β§ π¦ = π ) β (π₯ β€ (1 / 2) β 1 β€ (1 /
2))) |
170 | 167, 169 | mtbiri 326 |
. . . . . . 7
β’ ((π₯ = 1 β§ π¦ = π ) β Β¬ π₯ β€ (1 / 2)) |
171 | 170 | iffalsed 4538 |
. . . . . 6
β’ ((π₯ = 1 β§ π¦ = π ) β if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦)) = (((2 Β· π₯) β 1)ππ¦)) |
172 | 168 | oveq2d 7421 |
. . . . . . . . . 10
β’ ((π₯ = 1 β§ π¦ = π ) β (2 Β· π₯) = (2 Β· 1)) |
173 | | 2t1e2 12371 |
. . . . . . . . . 10
β’ (2
Β· 1) = 2 |
174 | 172, 173 | eqtrdi 2788 |
. . . . . . . . 9
β’ ((π₯ = 1 β§ π¦ = π ) β (2 Β· π₯) = 2) |
175 | 174 | oveq1d 7420 |
. . . . . . . 8
β’ ((π₯ = 1 β§ π¦ = π ) β ((2 Β· π₯) β 1) = (2 β
1)) |
176 | | 2m1e1 12334 |
. . . . . . . 8
β’ (2
β 1) = 1 |
177 | 175, 176 | eqtrdi 2788 |
. . . . . . 7
β’ ((π₯ = 1 β§ π¦ = π ) β ((2 Β· π₯) β 1) = 1) |
178 | | simpr 485 |
. . . . . . 7
β’ ((π₯ = 1 β§ π¦ = π ) β π¦ = π ) |
179 | 177, 178 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = 1 β§ π¦ = π ) β (((2 Β· π₯) β 1)ππ¦) = (1ππ )) |
180 | 171, 179 | eqtrd 2772 |
. . . . 5
β’ ((π₯ = 1 β§ π¦ = π ) β if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦)) = (1ππ )) |
181 | | ovex 7438 |
. . . . 5
β’ (1ππ ) β V |
182 | 180, 21, 181 | ovmpoa 7559 |
. . . 4
β’ ((1
β (0[,]1) β§ π
β (0[,]1)) β (1ππ ) = (1ππ )) |
183 | 131, 111,
182 | sylancr 587 |
. . 3
β’ ((π β§ π β (0[,]1)) β (1ππ ) = (1ππ )) |
184 | 4, 8 | pco1 24522 |
. . . 4
β’ (π β ((πΉ(*πβπ½)πΊ)β1) = (πΊβ1)) |
185 | 184 | adantr 481 |
. . 3
β’ ((π β§ π β (0[,]1)) β ((πΉ(*πβπ½)πΊ)β1) = (πΊβ1)) |
186 | 165, 183,
185 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π β (0[,]1)) β (1ππ ) = ((πΉ(*πβπ½)πΊ)β1)) |
187 | 10, 20, 89, 127, 146, 163, 186 | isphtpy2d 24494 |
1
β’ (π β π β ((πΉ(*πβπ½)πΊ)(PHtpyβπ½)(π»(*πβπ½)πΎ))) |