Step | Hyp | Ref
| Expression |
1 | | 0re 11165 |
. . . . . 6
β’ 0 β
β |
2 | | 1re 11163 |
. . . . . 6
β’ 1 β
β |
3 | 1, 2 | ifcli 4537 |
. . . . 5
β’ if(π₯ = π¦, 0, 1) β β |
4 | 3 | rgen2w 3066 |
. . . 4
β’
βπ₯ β
π βπ¦ β π if(π₯ = π¦, 0, 1) β β |
5 | | dscmet.1 |
. . . . 5
β’ π· = (π₯ β π, π¦ β π β¦ if(π₯ = π¦, 0, 1)) |
6 | 5 | fmpo 8004 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π if(π₯ = π¦, 0, 1) β β β π·:(π Γ π)βΆβ) |
7 | 4, 6 | mpbi 229 |
. . 3
β’ π·:(π Γ π)βΆβ |
8 | | equequ1 2029 |
. . . . . . . . 9
β’ (π₯ = π€ β (π₯ = π¦ β π€ = π¦)) |
9 | 8 | ifbid 4513 |
. . . . . . . 8
β’ (π₯ = π€ β if(π₯ = π¦, 0, 1) = if(π€ = π¦, 0, 1)) |
10 | | equequ2 2030 |
. . . . . . . . 9
β’ (π¦ = π£ β (π€ = π¦ β π€ = π£)) |
11 | 10 | ifbid 4513 |
. . . . . . . 8
β’ (π¦ = π£ β if(π€ = π¦, 0, 1) = if(π€ = π£, 0, 1)) |
12 | | 0nn0 12436 |
. . . . . . . . . 10
β’ 0 β
β0 |
13 | | 1nn0 12437 |
. . . . . . . . . 10
β’ 1 β
β0 |
14 | 12, 13 | ifcli 4537 |
. . . . . . . . 9
β’ if(π€ = π£, 0, 1) β
β0 |
15 | 14 | elexi 3466 |
. . . . . . . 8
β’ if(π€ = π£, 0, 1) β V |
16 | 9, 11, 5, 15 | ovmpo 7519 |
. . . . . . 7
β’ ((π€ β π β§ π£ β π) β (π€π·π£) = if(π€ = π£, 0, 1)) |
17 | 16 | eqeq1d 2735 |
. . . . . 6
β’ ((π€ β π β§ π£ β π) β ((π€π·π£) = 0 β if(π€ = π£, 0, 1) = 0)) |
18 | | iffalse 4499 |
. . . . . . . . . 10
β’ (Β¬
π€ = π£ β if(π€ = π£, 0, 1) = 1) |
19 | | ax-1ne0 11128 |
. . . . . . . . . . 11
β’ 1 β
0 |
20 | 19 | a1i 11 |
. . . . . . . . . 10
β’ (Β¬
π€ = π£ β 1 β 0) |
21 | 18, 20 | eqnetrd 3008 |
. . . . . . . . 9
β’ (Β¬
π€ = π£ β if(π€ = π£, 0, 1) β 0) |
22 | 21 | neneqd 2945 |
. . . . . . . 8
β’ (Β¬
π€ = π£ β Β¬ if(π€ = π£, 0, 1) = 0) |
23 | 22 | con4i 114 |
. . . . . . 7
β’ (if(π€ = π£, 0, 1) = 0 β π€ = π£) |
24 | | iftrue 4496 |
. . . . . . 7
β’ (π€ = π£ β if(π€ = π£, 0, 1) = 0) |
25 | 23, 24 | impbii 208 |
. . . . . 6
β’ (if(π€ = π£, 0, 1) = 0 β π€ = π£) |
26 | 17, 25 | bitrdi 287 |
. . . . 5
β’ ((π€ β π β§ π£ β π) β ((π€π·π£) = 0 β π€ = π£)) |
27 | 12, 13 | ifcli 4537 |
. . . . . . . . . . 11
β’ if(π’ = π€, 0, 1) β
β0 |
28 | 12, 13 | ifcli 4537 |
. . . . . . . . . . 11
β’ if(π’ = π£, 0, 1) β
β0 |
29 | 27, 28 | nn0addcli 12458 |
. . . . . . . . . 10
β’ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) β
β0 |
30 | | elnn0 12423 |
. . . . . . . . . 10
β’
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) β β0 β
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) β β β¨ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0)) |
31 | 29, 30 | mpbi 229 |
. . . . . . . . 9
β’
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) β β β¨ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0) |
32 | | breq1 5112 |
. . . . . . . . . . . 12
β’ (0 =
if(π€ = π£, 0, 1) β (0 β€ 1 β if(π€ = π£, 0, 1) β€ 1)) |
33 | | breq1 5112 |
. . . . . . . . . . . 12
β’ (1 =
if(π€ = π£, 0, 1) β (1 β€ 1 β if(π€ = π£, 0, 1) β€ 1)) |
34 | | 0le1 11686 |
. . . . . . . . . . . 12
β’ 0 β€
1 |
35 | 2 | leidi 11697 |
. . . . . . . . . . . 12
β’ 1 β€
1 |
36 | 32, 33, 34, 35 | keephyp 4561 |
. . . . . . . . . . 11
β’ if(π€ = π£, 0, 1) β€ 1 |
37 | | nnge1 12189 |
. . . . . . . . . . 11
β’
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) β β β 1 β€
(if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1))) |
38 | 14 | nn0rei 12432 |
. . . . . . . . . . . 12
β’ if(π€ = π£, 0, 1) β β |
39 | 29 | nn0rei 12432 |
. . . . . . . . . . . 12
β’ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) β β |
40 | 38, 2, 39 | letri 11292 |
. . . . . . . . . . 11
β’
((if(π€ = π£, 0, 1) β€ 1 β§ 1 β€
(if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1))) β if(π€ = π£, 0, 1) β€ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1))) |
41 | 36, 37, 40 | sylancr 588 |
. . . . . . . . . 10
β’
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) β β β if(π€ = π£, 0, 1) β€ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1))) |
42 | 27 | nn0ge0i 12448 |
. . . . . . . . . . . . 13
β’ 0 β€
if(π’ = π€, 0, 1) |
43 | 28 | nn0ge0i 12448 |
. . . . . . . . . . . . 13
β’ 0 β€
if(π’ = π£, 0, 1) |
44 | 27 | nn0rei 12432 |
. . . . . . . . . . . . . 14
β’ if(π’ = π€, 0, 1) β β |
45 | 28 | nn0rei 12432 |
. . . . . . . . . . . . . 14
β’ if(π’ = π£, 0, 1) β β |
46 | 44, 45 | add20i 11706 |
. . . . . . . . . . . . 13
β’ ((0 β€
if(π’ = π€, 0, 1) β§ 0 β€ if(π’ = π£, 0, 1)) β ((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0 β (if(π’ = π€, 0, 1) = 0 β§ if(π’ = π£, 0, 1) = 0))) |
47 | 42, 43, 46 | mp2an 691 |
. . . . . . . . . . . 12
β’
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0 β (if(π’ = π€, 0, 1) = 0 β§ if(π’ = π£, 0, 1) = 0)) |
48 | | equequ2 2030 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ = π€ β (π’ = π£ β π’ = π€)) |
49 | 48 | ifbid 4513 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ = π€ β if(π’ = π£, 0, 1) = if(π’ = π€, 0, 1)) |
50 | 49 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = π€ β (if(π’ = π£, 0, 1) = 0 β if(π’ = π€, 0, 1) = 0)) |
51 | 50, 48 | bibi12d 346 |
. . . . . . . . . . . . . . . 16
β’ (π£ = π€ β ((if(π’ = π£, 0, 1) = 0 β π’ = π£) β (if(π’ = π€, 0, 1) = 0 β π’ = π€))) |
52 | | equequ1 2029 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = π’ β (π€ = π£ β π’ = π£)) |
53 | 52 | ifbid 4513 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ = π’ β if(π€ = π£, 0, 1) = if(π’ = π£, 0, 1)) |
54 | 53 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = π’ β (if(π€ = π£, 0, 1) = 0 β if(π’ = π£, 0, 1) = 0)) |
55 | 54, 52 | bibi12d 346 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π’ β ((if(π€ = π£, 0, 1) = 0 β π€ = π£) β (if(π’ = π£, 0, 1) = 0 β π’ = π£))) |
56 | 55, 25 | chvarvv 2003 |
. . . . . . . . . . . . . . . 16
β’ (if(π’ = π£, 0, 1) = 0 β π’ = π£) |
57 | 51, 56 | chvarvv 2003 |
. . . . . . . . . . . . . . 15
β’ (if(π’ = π€, 0, 1) = 0 β π’ = π€) |
58 | | eqtr2 2757 |
. . . . . . . . . . . . . . 15
β’ ((π’ = π€ β§ π’ = π£) β π€ = π£) |
59 | 57, 56, 58 | syl2anb 599 |
. . . . . . . . . . . . . 14
β’
((if(π’ = π€, 0, 1) = 0 β§ if(π’ = π£, 0, 1) = 0) β π€ = π£) |
60 | 59 | iftrued 4498 |
. . . . . . . . . . . . 13
β’
((if(π’ = π€, 0, 1) = 0 β§ if(π’ = π£, 0, 1) = 0) β if(π€ = π£, 0, 1) = 0) |
61 | 1 | leidi 11697 |
. . . . . . . . . . . . 13
β’ 0 β€
0 |
62 | 60, 61 | eqbrtrdi 5148 |
. . . . . . . . . . . 12
β’
((if(π’ = π€, 0, 1) = 0 β§ if(π’ = π£, 0, 1) = 0) β if(π€ = π£, 0, 1) β€ 0) |
63 | 47, 62 | sylbi 216 |
. . . . . . . . . . 11
β’
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0 β if(π€ = π£, 0, 1) β€ 0) |
64 | | id 22 |
. . . . . . . . . . 11
β’
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0 β (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0) |
65 | 63, 64 | breqtrrd 5137 |
. . . . . . . . . 10
β’
((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0 β if(π€ = π£, 0, 1) β€ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1))) |
66 | 41, 65 | jaoi 856 |
. . . . . . . . 9
β’
(((if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) β β β¨ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1)) = 0) β if(π€ = π£, 0, 1) β€ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1))) |
67 | 31, 66 | mp1i 13 |
. . . . . . . 8
β’ ((π’ β π β§ (π€ β π β§ π£ β π)) β if(π€ = π£, 0, 1) β€ (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1))) |
68 | 16 | adantl 483 |
. . . . . . . 8
β’ ((π’ β π β§ (π€ β π β§ π£ β π)) β (π€π·π£) = if(π€ = π£, 0, 1)) |
69 | | eqeq12 2750 |
. . . . . . . . . . . 12
β’ ((π₯ = π’ β§ π¦ = π€) β (π₯ = π¦ β π’ = π€)) |
70 | 69 | ifbid 4513 |
. . . . . . . . . . 11
β’ ((π₯ = π’ β§ π¦ = π€) β if(π₯ = π¦, 0, 1) = if(π’ = π€, 0, 1)) |
71 | 27 | elexi 3466 |
. . . . . . . . . . 11
β’ if(π’ = π€, 0, 1) β V |
72 | 70, 5, 71 | ovmpoa 7514 |
. . . . . . . . . 10
β’ ((π’ β π β§ π€ β π) β (π’π·π€) = if(π’ = π€, 0, 1)) |
73 | 72 | adantrr 716 |
. . . . . . . . 9
β’ ((π’ β π β§ (π€ β π β§ π£ β π)) β (π’π·π€) = if(π’ = π€, 0, 1)) |
74 | | eqeq12 2750 |
. . . . . . . . . . . 12
β’ ((π₯ = π’ β§ π¦ = π£) β (π₯ = π¦ β π’ = π£)) |
75 | 74 | ifbid 4513 |
. . . . . . . . . . 11
β’ ((π₯ = π’ β§ π¦ = π£) β if(π₯ = π¦, 0, 1) = if(π’ = π£, 0, 1)) |
76 | 28 | elexi 3466 |
. . . . . . . . . . 11
β’ if(π’ = π£, 0, 1) β V |
77 | 75, 5, 76 | ovmpoa 7514 |
. . . . . . . . . 10
β’ ((π’ β π β§ π£ β π) β (π’π·π£) = if(π’ = π£, 0, 1)) |
78 | 77 | adantrl 715 |
. . . . . . . . 9
β’ ((π’ β π β§ (π€ β π β§ π£ β π)) β (π’π·π£) = if(π’ = π£, 0, 1)) |
79 | 73, 78 | oveq12d 7379 |
. . . . . . . 8
β’ ((π’ β π β§ (π€ β π β§ π£ β π)) β ((π’π·π€) + (π’π·π£)) = (if(π’ = π€, 0, 1) + if(π’ = π£, 0, 1))) |
80 | 67, 68, 79 | 3brtr4d 5141 |
. . . . . . 7
β’ ((π’ β π β§ (π€ β π β§ π£ β π)) β (π€π·π£) β€ ((π’π·π€) + (π’π·π£))) |
81 | 80 | expcom 415 |
. . . . . 6
β’ ((π€ β π β§ π£ β π) β (π’ β π β (π€π·π£) β€ ((π’π·π€) + (π’π·π£)))) |
82 | 81 | ralrimiv 3139 |
. . . . 5
β’ ((π€ β π β§ π£ β π) β βπ’ β π (π€π·π£) β€ ((π’π·π€) + (π’π·π£))) |
83 | 26, 82 | jca 513 |
. . . 4
β’ ((π€ β π β§ π£ β π) β (((π€π·π£) = 0 β π€ = π£) β§ βπ’ β π (π€π·π£) β€ ((π’π·π€) + (π’π·π£)))) |
84 | 83 | rgen2 3191 |
. . 3
β’
βπ€ β
π βπ£ β π (((π€π·π£) = 0 β π€ = π£) β§ βπ’ β π (π€π·π£) β€ ((π’π·π€) + (π’π·π£))) |
85 | 7, 84 | pm3.2i 472 |
. 2
β’ (π·:(π Γ π)βΆβ β§ βπ€ β π βπ£ β π (((π€π·π£) = 0 β π€ = π£) β§ βπ’ β π (π€π·π£) β€ ((π’π·π€) + (π’π·π£)))) |
86 | | ismet 23699 |
. 2
β’ (π β π β (π· β (Metβπ) β (π·:(π Γ π)βΆβ β§ βπ€ β π βπ£ β π (((π€π·π£) = 0 β π€ = π£) β§ βπ’ β π (π€π·π£) β€ ((π’π·π€) + (π’π·π£)))))) |
87 | 85, 86 | mpbiri 258 |
1
β’ (π β π β π· β (Metβπ)) |