Step | Hyp | Ref
| Expression |
1 | | odval.1 |
. . 3
โข ๐ = (Baseโ๐บ) |
2 | | odval.2 |
. . 3
โข ยท =
(.gโ๐บ) |
3 | | odval.3 |
. . 3
โข 0 =
(0gโ๐บ) |
4 | | odval.4 |
. . 3
โข ๐ = (odโ๐บ) |
5 | | odval.i |
. . 3
โข ๐ผ = {๐ฆ โ โ โฃ (๐ฆ ยท ๐ด) = 0 } |
6 | 1, 2, 3, 4, 5 | odval 19316 |
. 2
โข (๐ด โ ๐ โ (๐โ๐ด) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < ))) |
7 | | eqeq2 2748 |
. . . 4
โข (0 =
if(๐ผ = โ
, 0,
inf(๐ผ, โ, < ))
โ ((๐โ๐ด) = 0 โ (๐โ๐ด) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < )))) |
8 | 7 | imbi1d 341 |
. . 3
โข (0 =
if(๐ผ = โ
, 0,
inf(๐ผ, โ, < ))
โ (((๐โ๐ด) = 0 โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ)) โ ((๐โ๐ด) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < )) โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ)))) |
9 | | eqeq2 2748 |
. . . 4
โข
(inf(๐ผ, โ,
< ) = if(๐ผ = โ
, 0,
inf(๐ผ, โ, < ))
โ ((๐โ๐ด) = inf(๐ผ, โ, < ) โ (๐โ๐ด) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < )))) |
10 | 9 | imbi1d 341 |
. . 3
โข
(inf(๐ผ, โ,
< ) = if(๐ผ = โ
, 0,
inf(๐ผ, โ, < ))
โ (((๐โ๐ด) = inf(๐ผ, โ, < ) โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ)) โ ((๐โ๐ด) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < )) โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ)))) |
11 | | orc 865 |
. . . . 5
โข (((๐โ๐ด) = 0 โง ๐ผ = โ
) โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ)) |
12 | 11 | expcom 414 |
. . . 4
โข (๐ผ = โ
โ ((๐โ๐ด) = 0 โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ))) |
13 | 12 | adantl 482 |
. . 3
โข ((๐ด โ ๐ โง ๐ผ = โ
) โ ((๐โ๐ด) = 0 โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ))) |
14 | | ssrab2 4037 |
. . . . . . 7
โข {๐ฆ โ โ โฃ (๐ฆ ยท ๐ด) = 0 } โ
โ |
15 | | nnuz 12806 |
. . . . . . . 8
โข โ =
(โคโฅโ1) |
16 | 15 | eqcomi 2745 |
. . . . . . 7
โข
(โคโฅโ1) = โ |
17 | 14, 5, 16 | 3sstr4i 3987 |
. . . . . 6
โข ๐ผ โ
(โคโฅโ1) |
18 | | neqne 2951 |
. . . . . . 7
โข (ยฌ
๐ผ = โ
โ ๐ผ โ โ
) |
19 | 18 | adantl 482 |
. . . . . 6
โข ((๐ด โ ๐ โง ยฌ ๐ผ = โ
) โ ๐ผ โ โ
) |
20 | | infssuzcl 12857 |
. . . . . 6
โข ((๐ผ โ
(โคโฅโ1) โง ๐ผ โ โ
) โ inf(๐ผ, โ, < ) โ ๐ผ) |
21 | 17, 19, 20 | sylancr 587 |
. . . . 5
โข ((๐ด โ ๐ โง ยฌ ๐ผ = โ
) โ inf(๐ผ, โ, < ) โ ๐ผ) |
22 | | eleq1a 2832 |
. . . . 5
โข
(inf(๐ผ, โ,
< ) โ ๐ผ โ
((๐โ๐ด) = inf(๐ผ, โ, < ) โ (๐โ๐ด) โ ๐ผ)) |
23 | 21, 22 | syl 17 |
. . . 4
โข ((๐ด โ ๐ โง ยฌ ๐ผ = โ
) โ ((๐โ๐ด) = inf(๐ผ, โ, < ) โ (๐โ๐ด) โ ๐ผ)) |
24 | | olc 866 |
. . . 4
โข ((๐โ๐ด) โ ๐ผ โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ)) |
25 | 23, 24 | syl6 35 |
. . 3
โข ((๐ด โ ๐ โง ยฌ ๐ผ = โ
) โ ((๐โ๐ด) = inf(๐ผ, โ, < ) โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ))) |
26 | 8, 10, 13, 25 | ifbothda 4524 |
. 2
โข (๐ด โ ๐ โ ((๐โ๐ด) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < )) โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ))) |
27 | 6, 26 | mpd 15 |
1
โข (๐ด โ ๐ โ (((๐โ๐ด) = 0 โง ๐ผ = โ
) โจ (๐โ๐ด) โ ๐ผ)) |