Step | Hyp | Ref
| Expression |
1 | | reex 7944 |
. . . 4
β’ β
β V |
2 | 1 | mptex 5742 |
. . 3
β’ (π¦ β β β¦ if(π¦ # 0, 1, 0)) β
V |
3 | 2 | a1i 9 |
. 2
β’
(βπ₯ β
β DECID π₯ # 0 β (π¦ β β β¦ if(π¦ # 0, 1, 0)) β V) |
4 | | 1zzd 9279 |
. . . . 5
β’
((βπ₯ β
β DECID π₯ # 0 β§ π¦ β β) β 1 β
β€) |
5 | | 0zd 9264 |
. . . . 5
β’
((βπ₯ β
β DECID π₯ # 0 β§ π¦ β β) β 0 β
β€) |
6 | | breq1 4006 |
. . . . . . 7
β’ (π₯ = π¦ β (π₯ # 0 β π¦ # 0)) |
7 | 6 | dcbid 838 |
. . . . . 6
β’ (π₯ = π¦ β (DECID π₯ # 0 β DECID
π¦ # 0)) |
8 | 7 | rspccva 2840 |
. . . . 5
β’
((βπ₯ β
β DECID π₯ # 0 β§ π¦ β β) β DECID
π¦ # 0) |
9 | 4, 5, 8 | ifcldcd 3570 |
. . . 4
β’
((βπ₯ β
β DECID π₯ # 0 β§ π¦ β β) β if(π¦ # 0, 1, 0) β β€) |
10 | 9 | fmpttd 5671 |
. . 3
β’
(βπ₯ β
β DECID π₯ # 0 β (π¦ β β β¦ if(π¦ # 0, 1,
0)):ββΆβ€) |
11 | | 0re 7956 |
. . . . . 6
β’ 0 β
β |
12 | | 1zzd 9279 |
. . . . . . . 8
β’ (β€
β 1 β β€) |
13 | | 0zd 9264 |
. . . . . . . 8
β’ (β€
β 0 β β€) |
14 | | 0cn 7948 |
. . . . . . . . . . . 12
β’ 0 β
β |
15 | | apirr 8561 |
. . . . . . . . . . . 12
β’ (0 β
β β Β¬ 0 # 0) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
β’ Β¬ 0
# 0 |
17 | 16 | olci 732 |
. . . . . . . . . 10
β’ (0 # 0
β¨ Β¬ 0 # 0) |
18 | | df-dc 835 |
. . . . . . . . . 10
β’
(DECID 0 # 0 β (0 # 0 β¨ Β¬ 0 #
0)) |
19 | 17, 18 | mpbir 146 |
. . . . . . . . 9
β’
DECID 0 # 0 |
20 | 19 | a1i 9 |
. . . . . . . 8
β’ (β€
β DECID 0 # 0) |
21 | 12, 13, 20 | ifcldcd 3570 |
. . . . . . 7
β’ (β€
β if(0 # 0, 1, 0) β β€) |
22 | 21 | mptru 1362 |
. . . . . 6
β’ if(0 # 0,
1, 0) β β€ |
23 | | breq1 4006 |
. . . . . . . 8
β’ (π¦ = 0 β (π¦ # 0 β 0 # 0)) |
24 | 23 | ifbid 3555 |
. . . . . . 7
β’ (π¦ = 0 β if(π¦ # 0, 1, 0) = if(0 # 0, 1,
0)) |
25 | | eqid 2177 |
. . . . . . 7
β’ (π¦ β β β¦ if(π¦ # 0, 1, 0)) = (π¦ β β β¦ if(π¦ # 0, 1, 0)) |
26 | 24, 25 | fvmptg 5592 |
. . . . . 6
β’ ((0
β β β§ if(0 # 0, 1, 0) β β€) β ((π¦ β β β¦ if(π¦ # 0, 1, 0))β0) = if(0 #
0, 1, 0)) |
27 | 11, 22, 26 | mp2an 426 |
. . . . 5
β’ ((π¦ β β β¦ if(π¦ # 0, 1, 0))β0) = if(0 #
0, 1, 0) |
28 | 16 | iffalsei 3543 |
. . . . 5
β’ if(0 # 0,
1, 0) = 0 |
29 | 27, 28 | eqtri 2198 |
. . . 4
β’ ((π¦ β β β¦ if(π¦ # 0, 1, 0))β0) =
0 |
30 | 29 | a1i 9 |
. . 3
β’
(βπ₯ β
β DECID π₯ # 0 β ((π¦ β β β¦ if(π¦ # 0, 1, 0))β0) = 0) |
31 | | 1ne0 8986 |
. . . . . 6
β’ 1 β
0 |
32 | | breq1 4006 |
. . . . . . . . . 10
β’ (π¦ = π§ β (π¦ # 0 β π§ # 0)) |
33 | 32 | ifbid 3555 |
. . . . . . . . 9
β’ (π¦ = π§ β if(π¦ # 0, 1, 0) = if(π§ # 0, 1, 0)) |
34 | | rpre 9659 |
. . . . . . . . . 10
β’ (π§ β β+
β π§ β
β) |
35 | 34 | adantl 277 |
. . . . . . . . 9
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β π§ β
β) |
36 | | 1zzd 9279 |
. . . . . . . . . 10
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β 1 β
β€) |
37 | | 0zd 9264 |
. . . . . . . . . 10
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β 0 β
β€) |
38 | | breq1 4006 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (π₯ # 0 β π§ # 0)) |
39 | 38 | dcbid 838 |
. . . . . . . . . . 11
β’ (π₯ = π§ β (DECID π₯ # 0 β DECID
π§ # 0)) |
40 | | simpl 109 |
. . . . . . . . . . 11
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β
βπ₯ β β
DECID π₯ #
0) |
41 | 39, 40, 35 | rspcdva 2846 |
. . . . . . . . . 10
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β
DECID π§ #
0) |
42 | 36, 37, 41 | ifcldcd 3570 |
. . . . . . . . 9
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β if(π§ # 0, 1, 0) β
β€) |
43 | 25, 33, 35, 42 | fvmptd3 5609 |
. . . . . . . 8
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ§) = if(π§ # 0, 1, 0)) |
44 | | rpap0 9669 |
. . . . . . . . . 10
β’ (π§ β β+
β π§ #
0) |
45 | 44 | iftrued 3541 |
. . . . . . . . 9
β’ (π§ β β+
β if(π§ # 0, 1, 0) =
1) |
46 | 45 | adantl 277 |
. . . . . . . 8
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β if(π§ # 0, 1, 0) =
1) |
47 | 43, 46 | eqtrd 2210 |
. . . . . . 7
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ§) = 1) |
48 | 47 | neeq1d 2365 |
. . . . . 6
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β (((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ§) β 0 β 1 β
0)) |
49 | 31, 48 | mpbiri 168 |
. . . . 5
β’
((βπ₯ β
β DECID π₯ # 0 β§ π§ β β+) β ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ§) β 0) |
50 | 49 | ralrimiva 2550 |
. . . 4
β’
(βπ₯ β
β DECID π₯ # 0 β βπ§ β β+ ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ§) β 0) |
51 | | fveq2 5515 |
. . . . . 6
β’ (π§ = π₯ β ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ§) = ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ₯)) |
52 | 51 | neeq1d 2365 |
. . . . 5
β’ (π§ = π₯ β (((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ§) β 0 β ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ₯) β 0)) |
53 | 52 | cbvralv 2703 |
. . . 4
β’
(βπ§ β
β+ ((π¦
β β β¦ if(π¦
# 0, 1, 0))βπ§) β 0
β βπ₯ β
β+ ((π¦
β β β¦ if(π¦
# 0, 1, 0))βπ₯) β
0) |
54 | 50, 53 | sylib 122 |
. . 3
β’
(βπ₯ β
β DECID π₯ # 0 β βπ₯ β β+ ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ₯) β 0) |
55 | 10, 30, 54 | 3jca 1177 |
. 2
β’
(βπ₯ β
β DECID π₯ # 0 β ((π¦ β β β¦ if(π¦ # 0, 1, 0)):ββΆβ€ β§
((π¦ β β β¦
if(π¦ # 0, 1, 0))β0) =
0 β§ βπ₯ β
β+ ((π¦
β β β¦ if(π¦
# 0, 1, 0))βπ₯) β
0)) |
56 | | feq1 5348 |
. . 3
β’ (π = (π¦ β β β¦ if(π¦ # 0, 1, 0)) β (π:ββΆβ€ β (π¦ β β β¦ if(π¦ # 0, 1,
0)):ββΆβ€)) |
57 | | fveq1 5514 |
. . . 4
β’ (π = (π¦ β β β¦ if(π¦ # 0, 1, 0)) β (πβ0) = ((π¦ β β β¦ if(π¦ # 0, 1, 0))β0)) |
58 | 57 | eqeq1d 2186 |
. . 3
β’ (π = (π¦ β β β¦ if(π¦ # 0, 1, 0)) β ((πβ0) = 0 β ((π¦ β β β¦ if(π¦ # 0, 1, 0))β0) = 0)) |
59 | | fveq1 5514 |
. . . . 5
β’ (π = (π¦ β β β¦ if(π¦ # 0, 1, 0)) β (πβπ₯) = ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ₯)) |
60 | 59 | neeq1d 2365 |
. . . 4
β’ (π = (π¦ β β β¦ if(π¦ # 0, 1, 0)) β ((πβπ₯) β 0 β ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ₯) β 0)) |
61 | 60 | ralbidv 2477 |
. . 3
β’ (π = (π¦ β β β¦ if(π¦ # 0, 1, 0)) β (βπ₯ β β+
(πβπ₯) β 0 β βπ₯ β β+ ((π¦ β β β¦ if(π¦ # 0, 1, 0))βπ₯) β 0)) |
62 | 56, 58, 61 | 3anbi123d 1312 |
. 2
β’ (π = (π¦ β β β¦ if(π¦ # 0, 1, 0)) β ((π:ββΆβ€ β§ (πβ0) = 0 β§
βπ₯ β
β+ (πβπ₯) β 0) β ((π¦ β β β¦ if(π¦ # 0, 1, 0)):ββΆβ€ β§
((π¦ β β β¦
if(π¦ # 0, 1, 0))β0) =
0 β§ βπ₯ β
β+ ((π¦
β β β¦ if(π¦
# 0, 1, 0))βπ₯) β
0))) |
63 | 3, 55, 62 | elabd 2882 |
1
β’
(βπ₯ β
β DECID π₯ # 0 β βπ(π:ββΆβ€ β§ (πβ0) = 0 β§
βπ₯ β
β+ (πβπ₯) β 0)) |