Step | Hyp | Ref
| Expression |
1 | | breq2 4008 |
. . . . . . . . . . . 12
β’ (π₯ = π΄ β (0 < π₯ β 0 < π΄)) |
2 | | fveq2 5516 |
. . . . . . . . . . . . 13
β’ (π₯ = π΄ β (πΉβπ₯) = (πΉβπ΄)) |
3 | 2 | neeq1d 2365 |
. . . . . . . . . . . 12
β’ (π₯ = π΄ β ((πΉβπ₯) β 0 β (πΉβπ΄) β 0)) |
4 | 1, 3 | imbi12d 234 |
. . . . . . . . . . 11
β’ (π₯ = π΄ β ((0 < π₯ β (πΉβπ₯) β 0) β (0 < π΄ β (πΉβπ΄) β 0))) |
5 | | elrp 9655 |
. . . . . . . . . . . . . 14
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
6 | | nconstwlpo.rp |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β (πΉβπ₯) β 0) |
7 | 5, 6 | sylan2br 288 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β β§ 0 < π₯)) β (πΉβπ₯) β 0) |
8 | 7 | expr 375 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (0 < π₯ β (πΉβπ₯) β 0)) |
9 | 8 | ralrimiva 2550 |
. . . . . . . . . . 11
β’ (π β βπ₯ β β (0 < π₯ β (πΉβπ₯) β 0)) |
10 | | nconstwlpo.g |
. . . . . . . . . . . 12
β’ (π β πΊ:ββΆ{0, 1}) |
11 | | nconstwlpo.a |
. . . . . . . . . . . 12
β’ π΄ = Ξ£π β β ((1 / (2βπ)) Β· (πΊβπ)) |
12 | 10, 11 | trilpolemcl 14788 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
13 | 4, 9, 12 | rspcdva 2847 |
. . . . . . . . . 10
β’ (π β (0 < π΄ β (πΉβπ΄) β 0)) |
14 | 13 | necon2bd 2405 |
. . . . . . . . 9
β’ (π β ((πΉβπ΄) = 0 β Β¬ 0 < π΄)) |
15 | 14 | imp 124 |
. . . . . . . 8
β’ ((π β§ (πΉβπ΄) = 0) β Β¬ 0 < π΄) |
16 | 10 | adantr 276 |
. . . . . . . . . . . 12
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 1) β πΊ:ββΆ{0, 1}) |
17 | | simpr 110 |
. . . . . . . . . . . . 13
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 1) β βπ¦ β β (πΊβπ¦) = 1) |
18 | | fveqeq2 5525 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β ((πΊβπ¦) = 1 β (πΊβπ) = 1)) |
19 | 18 | cbvrexv 2705 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
β (πΊβπ¦) = 1 β βπ β β (πΊβπ) = 1) |
20 | 17, 19 | sylib 122 |
. . . . . . . . . . . 12
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 1) β βπ β β (πΊβπ) = 1) |
21 | 16, 11, 20 | nconstwlpolemgt0 14814 |
. . . . . . . . . . 11
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 1) β 0 < π΄) |
22 | 21 | ex 115 |
. . . . . . . . . 10
β’ (π β (βπ¦ β β (πΊβπ¦) = 1 β 0 < π΄)) |
23 | 22 | con3d 631 |
. . . . . . . . 9
β’ (π β (Β¬ 0 < π΄ β Β¬ βπ¦ β β (πΊβπ¦) = 1)) |
24 | 23 | adantr 276 |
. . . . . . . 8
β’ ((π β§ (πΉβπ΄) = 0) β (Β¬ 0 < π΄ β Β¬ βπ¦ β β (πΊβπ¦) = 1)) |
25 | 15, 24 | mpd 13 |
. . . . . . 7
β’ ((π β§ (πΉβπ΄) = 0) β Β¬ βπ¦ β β (πΊβπ¦) = 1) |
26 | | ralnex 2465 |
. . . . . . 7
β’
(βπ¦ β
β Β¬ (πΊβπ¦) = 1 β Β¬ βπ¦ β β (πΊβπ¦) = 1) |
27 | 25, 26 | sylibr 134 |
. . . . . 6
β’ ((π β§ (πΉβπ΄) = 0) β βπ¦ β β Β¬ (πΊβπ¦) = 1) |
28 | 27 | r19.21bi 2565 |
. . . . 5
β’ (((π β§ (πΉβπ΄) = 0) β§ π¦ β β) β Β¬ (πΊβπ¦) = 1) |
29 | 10 | ad2antrr 488 |
. . . . . . 7
β’ (((π β§ (πΉβπ΄) = 0) β§ π¦ β β) β πΊ:ββΆ{0, 1}) |
30 | | simpr 110 |
. . . . . . 7
β’ (((π β§ (πΉβπ΄) = 0) β§ π¦ β β) β π¦ β β) |
31 | 29, 30 | ffvelcdmd 5653 |
. . . . . 6
β’ (((π β§ (πΉβπ΄) = 0) β§ π¦ β β) β (πΊβπ¦) β {0, 1}) |
32 | | elpri 3616 |
. . . . . 6
β’ ((πΊβπ¦) β {0, 1} β ((πΊβπ¦) = 0 β¨ (πΊβπ¦) = 1)) |
33 | 31, 32 | syl 14 |
. . . . 5
β’ (((π β§ (πΉβπ΄) = 0) β§ π¦ β β) β ((πΊβπ¦) = 0 β¨ (πΊβπ¦) = 1)) |
34 | 28, 33 | ecased 1349 |
. . . 4
β’ (((π β§ (πΉβπ΄) = 0) β§ π¦ β β) β (πΊβπ¦) = 0) |
35 | 34 | ralrimiva 2550 |
. . 3
β’ ((π β§ (πΉβπ΄) = 0) β βπ¦ β β (πΊβπ¦) = 0) |
36 | 35 | orcd 733 |
. 2
β’ ((π β§ (πΉβπ΄) = 0) β (βπ¦ β β (πΊβπ¦) = 0 β¨ Β¬ βπ¦ β β (πΊβπ¦) = 0)) |
37 | 10 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 0) β πΊ:ββΆ{0, 1}) |
38 | | simpr 110 |
. . . . . . . . 9
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 0) β βπ¦ β β (πΊβπ¦) = 0) |
39 | 37, 11, 38 | nconstwlpolem0 14813 |
. . . . . . . 8
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 0) β π΄ = 0) |
40 | 39 | fveq2d 5520 |
. . . . . . 7
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 0) β (πΉβπ΄) = (πΉβ0)) |
41 | | nconstwlpo.0 |
. . . . . . . 8
β’ (π β (πΉβ0) = 0) |
42 | 41 | adantr 276 |
. . . . . . 7
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 0) β (πΉβ0) = 0) |
43 | 40, 42 | eqtrd 2210 |
. . . . . 6
β’ ((π β§ βπ¦ β β (πΊβπ¦) = 0) β (πΉβπ΄) = 0) |
44 | 43 | ex 115 |
. . . . 5
β’ (π β (βπ¦ β β (πΊβπ¦) = 0 β (πΉβπ΄) = 0)) |
45 | 44 | con3d 631 |
. . . 4
β’ (π β (Β¬ (πΉβπ΄) = 0 β Β¬ βπ¦ β β (πΊβπ¦) = 0)) |
46 | 45 | imp 124 |
. . 3
β’ ((π β§ Β¬ (πΉβπ΄) = 0) β Β¬ βπ¦ β β (πΊβπ¦) = 0) |
47 | 46 | olcd 734 |
. 2
β’ ((π β§ Β¬ (πΉβπ΄) = 0) β (βπ¦ β β (πΊβπ¦) = 0 β¨ Β¬ βπ¦ β β (πΊβπ¦) = 0)) |
48 | | nconstwlpo.f |
. . . . 5
β’ (π β πΉ:ββΆβ€) |
49 | 48, 12 | ffvelcdmd 5653 |
. . . 4
β’ (π β (πΉβπ΄) β β€) |
50 | | 0z 9264 |
. . . 4
β’ 0 β
β€ |
51 | | zdceq 9328 |
. . . 4
β’ (((πΉβπ΄) β β€ β§ 0 β β€)
β DECID (πΉβπ΄) = 0) |
52 | 49, 50, 51 | sylancl 413 |
. . 3
β’ (π β DECID
(πΉβπ΄) = 0) |
53 | | exmiddc 836 |
. . 3
β’
(DECID (πΉβπ΄) = 0 β ((πΉβπ΄) = 0 β¨ Β¬ (πΉβπ΄) = 0)) |
54 | 52, 53 | syl 14 |
. 2
β’ (π β ((πΉβπ΄) = 0 β¨ Β¬ (πΉβπ΄) = 0)) |
55 | 36, 47, 54 | mpjaodan 798 |
1
β’ (π β (βπ¦ β β (πΊβπ¦) = 0 β¨ Β¬ βπ¦ β β (πΊβπ¦) = 0)) |