Step | Hyp | Ref
| Expression |
1 | | 0re 11158 |
. 2
โข 0 โ
โ |
2 | | ax-rnegex 11123 |
. 2
โข (0 โ
โ โ โ๐
โ โ (0 + ๐) =
0) |
3 | | oveq2 7366 |
. . . . . . 7
โข (๐ = 0 โ (0 + ๐) = (0 + 0)) |
4 | 3 | eqeq1d 2739 |
. . . . . 6
โข (๐ = 0 โ ((0 + ๐) = 0 โ (0 + 0) =
0)) |
5 | 4 | biimpd 228 |
. . . . 5
โข (๐ = 0 โ ((0 + ๐) = 0 โ (0 + 0) =
0)) |
6 | 5 | adantld 492 |
. . . 4
โข (๐ = 0 โ ((๐ โ โ โง (0 + ๐) = 0) โ (0 + 0) = 0)) |
7 | | ax-rrecex 11124 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ 0) โ โ๐ฆ โ โ (๐ ยท ๐ฆ) = 1) |
8 | 7 | adantlr 714 |
. . . . . 6
โข (((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โ โ๐ฆ โ โ (๐ ยท ๐ฆ) = 1) |
9 | | simplll 774 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ๐ โ โ) |
10 | 9 | recnd 11184 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ๐ โ โ) |
11 | | simprl 770 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ๐ฆ โ โ) |
12 | 11 | recnd 11184 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ๐ฆ โ โ) |
13 | | 0cn 11148 |
. . . . . . . . . . 11
โข 0 โ
โ |
14 | | mulass 11140 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฆ โ โ โง 0 โ
โ) โ ((๐
ยท ๐ฆ) ยท 0) =
(๐ ยท (๐ฆ ยท 0))) |
15 | 13, 14 | mp3an3 1451 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ฆ โ โ) โ ((๐ ยท ๐ฆ) ยท 0) = (๐ ยท (๐ฆ ยท 0))) |
16 | 10, 12, 15 | syl2anc 585 |
. . . . . . . . 9
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((๐ ยท ๐ฆ) ยท 0) = (๐ ยท (๐ฆ ยท 0))) |
17 | | oveq1 7365 |
. . . . . . . . . . 11
โข ((๐ ยท ๐ฆ) = 1 โ ((๐ ยท ๐ฆ) ยท 0) = (1 ยท
0)) |
18 | 13 | mulid2i 11161 |
. . . . . . . . . . 11
โข (1
ยท 0) = 0 |
19 | 17, 18 | eqtrdi 2793 |
. . . . . . . . . 10
โข ((๐ ยท ๐ฆ) = 1 โ ((๐ ยท ๐ฆ) ยท 0) = 0) |
20 | 19 | ad2antll 728 |
. . . . . . . . 9
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((๐ ยท ๐ฆ) ยท 0) = 0) |
21 | 16, 20 | eqtr3d 2779 |
. . . . . . . 8
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (๐ ยท (๐ฆ ยท 0)) = 0) |
22 | 21 | oveq1d 7373 |
. . . . . . 7
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((๐ ยท (๐ฆ ยท 0)) + 0) = (0 +
0)) |
23 | | simpllr 775 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (0 + ๐) = 0) |
24 | 23 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((0 + ๐) ยท (๐ฆ ยท 0)) = (0 ยท (๐ฆ ยท 0))) |
25 | | remulcl 11137 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง 0 โ
โ) โ (๐ฆ ยท
0) โ โ) |
26 | 1, 25 | mpan2 690 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (๐ฆ ยท 0) โ
โ) |
27 | 26 | ad2antrl 727 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (๐ฆ ยท 0) โ โ) |
28 | 27 | recnd 11184 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (๐ฆ ยท 0) โ โ) |
29 | | adddir 11147 |
. . . . . . . . . . . 12
โข ((0
โ โ โง ๐
โ โ โง (๐ฆ
ยท 0) โ โ) โ ((0 + ๐) ยท (๐ฆ ยท 0)) = ((0 ยท (๐ฆ ยท 0)) + (๐ ยท (๐ฆ ยท 0)))) |
30 | 13, 10, 28, 29 | mp3an2i 1467 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((0 + ๐) ยท (๐ฆ ยท 0)) = ((0 ยท (๐ฆ ยท 0)) + (๐ ยท (๐ฆ ยท 0)))) |
31 | 24, 30 | eqtr3d 2779 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (0 ยท (๐ฆ ยท 0)) = ((0 ยท
(๐ฆ ยท 0)) + (๐ ยท (๐ฆ ยท 0)))) |
32 | 31 | oveq1d 7373 |
. . . . . . . . 9
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((0 ยท (๐ฆ ยท 0)) + 0) = (((0
ยท (๐ฆ ยท 0)) +
(๐ ยท (๐ฆ ยท 0))) +
0)) |
33 | | remulcl 11137 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง (๐ฆ
ยท 0) โ โ) โ (0 ยท (๐ฆ ยท 0)) โ
โ) |
34 | 1, 26, 33 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ (0
ยท (๐ฆ ยท 0))
โ โ) |
35 | 34 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (0 ยท (๐ฆ ยท 0)) โ
โ) |
36 | 35 | recnd 11184 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (0 ยท (๐ฆ ยท 0)) โ
โ) |
37 | | remulcl 11137 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ฆ ยท 0) โ โ)
โ (๐ ยท (๐ฆ ยท 0)) โ
โ) |
38 | 9, 27, 37 | syl2anc 585 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (๐ ยท (๐ฆ ยท 0)) โ
โ) |
39 | 38 | recnd 11184 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (๐ ยท (๐ฆ ยท 0)) โ
โ) |
40 | | addass 11139 |
. . . . . . . . . . 11
โข (((0
ยท (๐ฆ ยท 0))
โ โ โง (๐
ยท (๐ฆ ยท 0))
โ โ โง 0 โ โ) โ (((0 ยท (๐ฆ ยท 0)) + (๐ ยท (๐ฆ ยท 0))) + 0) = ((0 ยท (๐ฆ ยท 0)) + ((๐ ยท (๐ฆ ยท 0)) + 0))) |
41 | 13, 40 | mp3an3 1451 |
. . . . . . . . . 10
โข (((0
ยท (๐ฆ ยท 0))
โ โ โง (๐
ยท (๐ฆ ยท 0))
โ โ) โ (((0 ยท (๐ฆ ยท 0)) + (๐ ยท (๐ฆ ยท 0))) + 0) = ((0 ยท (๐ฆ ยท 0)) + ((๐ ยท (๐ฆ ยท 0)) + 0))) |
42 | 36, 39, 41 | syl2anc 585 |
. . . . . . . . 9
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (((0 ยท (๐ฆ ยท 0)) + (๐ ยท (๐ฆ ยท 0))) + 0) = ((0 ยท (๐ฆ ยท 0)) + ((๐ ยท (๐ฆ ยท 0)) + 0))) |
43 | 32, 42 | eqtr2d 2778 |
. . . . . . . 8
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((0 ยท (๐ฆ ยท 0)) + ((๐ ยท (๐ฆ ยท 0)) + 0)) = ((0 ยท (๐ฆ ยท 0)) +
0)) |
44 | 26, 37 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฆ โ โ) โ (๐ ยท (๐ฆ ยท 0)) โ
โ) |
45 | | readdcl 11135 |
. . . . . . . . . . 11
โข (((๐ ยท (๐ฆ ยท 0)) โ โ โง 0 โ
โ) โ ((๐
ยท (๐ฆ ยท 0)) +
0) โ โ) |
46 | 44, 1, 45 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ฆ โ โ) โ ((๐ ยท (๐ฆ ยท 0)) + 0) โ
โ) |
47 | 9, 11, 46 | syl2anc 585 |
. . . . . . . . 9
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((๐ ยท (๐ฆ ยท 0)) + 0) โ
โ) |
48 | | readdcan 11330 |
. . . . . . . . . 10
โข ((((๐ ยท (๐ฆ ยท 0)) + 0) โ โ โง 0
โ โ โง (0 ยท (๐ฆ ยท 0)) โ โ) โ (((0
ยท (๐ฆ ยท 0)) +
((๐ ยท (๐ฆ ยท 0)) + 0)) = ((0
ยท (๐ฆ ยท 0)) +
0) โ ((๐ ยท
(๐ฆ ยท 0)) + 0) =
0)) |
49 | 1, 48 | mp3an2 1450 |
. . . . . . . . 9
โข ((((๐ ยท (๐ฆ ยท 0)) + 0) โ โ โง (0
ยท (๐ฆ ยท 0))
โ โ) โ (((0 ยท (๐ฆ ยท 0)) + ((๐ ยท (๐ฆ ยท 0)) + 0)) = ((0 ยท (๐ฆ ยท 0)) + 0) โ
((๐ ยท (๐ฆ ยท 0)) + 0) =
0)) |
50 | 47, 35, 49 | syl2anc 585 |
. . . . . . . 8
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (((0 ยท (๐ฆ ยท 0)) + ((๐ ยท (๐ฆ ยท 0)) + 0)) = ((0 ยท (๐ฆ ยท 0)) + 0) โ
((๐ ยท (๐ฆ ยท 0)) + 0) =
0)) |
51 | 43, 50 | mpbid 231 |
. . . . . . 7
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ ((๐ ยท (๐ฆ ยท 0)) + 0) = 0) |
52 | 22, 51 | eqtr3d 2779 |
. . . . . 6
โข ((((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โง (๐ฆ โ โ โง (๐ ยท ๐ฆ) = 1)) โ (0 + 0) = 0) |
53 | 8, 52 | rexlimddv 3159 |
. . . . 5
โข (((๐ โ โ โง (0 + ๐) = 0) โง ๐ โ 0) โ (0 + 0) = 0) |
54 | 53 | expcom 415 |
. . . 4
โข (๐ โ 0 โ ((๐ โ โ โง (0 + ๐) = 0) โ (0 + 0) =
0)) |
55 | 6, 54 | pm2.61ine 3029 |
. . 3
โข ((๐ โ โ โง (0 + ๐) = 0) โ (0 + 0) =
0) |
56 | 55 | rexlimiva 3145 |
. 2
โข
(โ๐ โ
โ (0 + ๐) = 0 โ
(0 + 0) = 0) |
57 | 1, 2, 56 | mp2b 10 |
1
โข (0 + 0) =
0 |