Step | Hyp | Ref
| Expression |
1 | | inelr 8541 |
. . 3
โข ยฌ i
โ โ |
2 | | recexre 8535 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด #โ 0) โ
โ๐ฅ โ โ
(๐ด ยท ๐ฅ) = 1) |
3 | 2 | adantlr 477 |
. . . . 5
โข (((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โ โ๐ฅ โ
โ (๐ด ยท ๐ฅ) = 1) |
4 | | simplll 533 |
. . . . . . . . 9
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ ๐ด โ โ) |
5 | 4 | recnd 7986 |
. . . . . . . 8
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ ๐ด โ โ) |
6 | | simprl 529 |
. . . . . . . . 9
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ ๐ฅ โ
โ) |
7 | 6 | recnd 7986 |
. . . . . . . 8
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ ๐ฅ โ
โ) |
8 | | ax-icn 7906 |
. . . . . . . . 9
โข i โ
โ |
9 | | mulass 7942 |
. . . . . . . . 9
โข ((i
โ โ โง ๐ด
โ โ โง ๐ฅ
โ โ) โ ((i ยท ๐ด) ยท ๐ฅ) = (i ยท (๐ด ยท ๐ฅ))) |
10 | 8, 9 | mp3an1 1324 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ฅ โ โ) โ ((i
ยท ๐ด) ยท ๐ฅ) = (i ยท (๐ด ยท ๐ฅ))) |
11 | 5, 7, 10 | syl2anc 411 |
. . . . . . 7
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ ((i ยท
๐ด) ยท ๐ฅ) = (i ยท (๐ด ยท ๐ฅ))) |
12 | | oveq2 5883 |
. . . . . . . . 9
โข ((๐ด ยท ๐ฅ) = 1 โ (i ยท (๐ด ยท ๐ฅ)) = (i ยท 1)) |
13 | 8 | mulid1i 7959 |
. . . . . . . . 9
โข (i
ยท 1) = i |
14 | 12, 13 | eqtrdi 2226 |
. . . . . . . 8
โข ((๐ด ยท ๐ฅ) = 1 โ (i ยท (๐ด ยท ๐ฅ)) = i) |
15 | 14 | ad2antll 491 |
. . . . . . 7
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ (i ยท
(๐ด ยท ๐ฅ)) = i) |
16 | 11, 15 | eqtrd 2210 |
. . . . . 6
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ ((i ยท
๐ด) ยท ๐ฅ) = i) |
17 | | simpllr 534 |
. . . . . . 7
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ (i ยท ๐ด) โ
โ) |
18 | 17, 6 | remulcld 7988 |
. . . . . 6
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ ((i ยท
๐ด) ยท ๐ฅ) โ
โ) |
19 | 16, 18 | eqeltrrd 2255 |
. . . . 5
โข ((((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โง (๐ฅ โ โ
โง (๐ด ยท ๐ฅ) = 1)) โ i โ
โ) |
20 | 3, 19 | rexlimddv 2599 |
. . . 4
โข (((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โง ๐ด #โ
0) โ i โ โ) |
21 | 20 | ex 115 |
. . 3
โข ((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โ (๐ด
#โ 0 โ i โ โ)) |
22 | 1, 21 | mtoi 664 |
. 2
โข ((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โ ยฌ ๐ด
#โ 0) |
23 | | 0re 7957 |
. . . 4
โข 0 โ
โ |
24 | | reapti 8536 |
. . . 4
โข ((๐ด โ โ โง 0 โ
โ) โ (๐ด = 0
โ ยฌ ๐ด
#โ 0)) |
25 | 23, 24 | mpan2 425 |
. . 3
โข (๐ด โ โ โ (๐ด = 0 โ ยฌ ๐ด #โ
0)) |
26 | 25 | adantr 276 |
. 2
โข ((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โ (๐ด = 0 โ ยฌ
๐ด #โ
0)) |
27 | 22, 26 | mpbird 167 |
1
โข ((๐ด โ โ โง (i
ยท ๐ด) โ โ)
โ ๐ด =
0) |