Step | Hyp | Ref
| Expression |
1 | | ax-rrecex 11147 |
. . . . 5
โข ((๐
โ โ โง ๐
โ 0) โ โ๐ฅ โ โ (๐
ยท ๐ฅ) = 1) |
2 | | sn-inelr 41025 |
. . . . . 6
โข ยฌ i
โ โ |
3 | | simplll 773 |
. . . . . . . . . . 11
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ ๐
โ
โ) |
4 | | simplrl 775 |
. . . . . . . . . . 11
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ ๐ฅ โ
โ) |
5 | | simplrr 776 |
. . . . . . . . . . 11
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ (๐
ยท ๐ฅ) = 1) |
6 | 3, 4, 5 | remulinvcom 40992 |
. . . . . . . . . 10
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ (๐ฅ ยท ๐
) = 1) |
7 | 6 | oveq1d 7392 |
. . . . . . . . 9
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ ((๐ฅ ยท ๐
) ยท i) = (1 ยท
i)) |
8 | 4 | recnd 11207 |
. . . . . . . . . 10
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ ๐ฅ โ
โ) |
9 | 3 | recnd 11207 |
. . . . . . . . . 10
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ ๐
โ
โ) |
10 | | ax-icn 11134 |
. . . . . . . . . . 11
โข i โ
โ |
11 | 10 | a1i 11 |
. . . . . . . . . 10
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ i โ
โ) |
12 | 8, 9, 11 | mulassd 11202 |
. . . . . . . . 9
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ ((๐ฅ ยท ๐
) ยท i) = (๐ฅ ยท (๐
ยท i))) |
13 | | sn-1ticom 40994 |
. . . . . . . . . . 11
โข (1
ยท i) = (i ยท 1) |
14 | | it1ei 40996 |
. . . . . . . . . . 11
โข (i
ยท 1) = i |
15 | 13, 14 | eqtri 2759 |
. . . . . . . . . 10
โข (1
ยท i) = i |
16 | 15 | a1i 11 |
. . . . . . . . 9
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ (1
ยท i) = i) |
17 | 7, 12, 16 | 3eqtr3d 2779 |
. . . . . . . 8
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ (๐ฅ ยท (๐
ยท i)) = i) |
18 | | simpr 485 |
. . . . . . . . 9
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ (๐
ยท i) โ
โ) |
19 | 4, 18 | remulcld 11209 |
. . . . . . . 8
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ (๐ฅ ยท (๐
ยท i)) โ
โ) |
20 | 17, 19 | eqeltrrd 2833 |
. . . . . . 7
โข ((((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โง (๐
ยท i) โ โ) โ i โ
โ) |
21 | 20 | ex 413 |
. . . . . 6
โข (((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โ ((๐
ยท i) โ โ โ i โ
โ)) |
22 | 2, 21 | mtoi 198 |
. . . . 5
โข (((๐
โ โ โง ๐
โ 0) โง (๐ฅ โ โ โง (๐
ยท ๐ฅ) = 1)) โ ยฌ (๐
ยท i) โ
โ) |
23 | 1, 22 | rexlimddv 3160 |
. . . 4
โข ((๐
โ โ โง ๐
โ 0) โ ยฌ (๐
ยท i) โ
โ) |
24 | 23 | ex 413 |
. . 3
โข (๐
โ โ โ (๐
โ 0 โ ยฌ (๐
ยท i) โ
โ)) |
25 | 24 | necon4ad 2958 |
. 2
โข (๐
โ โ โ ((๐
ยท i) โ โ
โ ๐
=
0)) |
26 | | oveq1 7384 |
. . 3
โข (๐
= 0 โ (๐
ยท i) = (0 ยท
i)) |
27 | | sn-0tie0 40999 |
. . . 4
โข (0
ยท i) = 0 |
28 | | 0re 11181 |
. . . 4
โข 0 โ
โ |
29 | 27, 28 | eqeltri 2828 |
. . 3
โข (0
ยท i) โ โ |
30 | 26, 29 | eqeltrdi 2840 |
. 2
โข (๐
= 0 โ (๐
ยท i) โ
โ) |
31 | 25, 30 | impbid1 224 |
1
โข (๐
โ โ โ ((๐
ยท i) โ โ
โ ๐
=
0)) |