Step | Hyp | Ref
| Expression |
1 | | 1re 11162 |
. 2
โข 1 โ
โ |
2 | | ax-rnegex 11129 |
. 2
โข (1 โ
โ โ โ๐
โ โ (1 + ๐) =
0) |
3 | | ax-1ne0 11127 |
. . . . . 6
โข 1 โ
0 |
4 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ = 0 โ (1 + ๐) = (1 + 0)) |
5 | 4 | eqeq1d 2739 |
. . . . . . . . 9
โข (๐ = 0 โ ((1 + ๐) = 0 โ (1 + 0) =
0)) |
6 | 5 | biimpcd 249 |
. . . . . . . 8
โข ((1 +
๐) = 0 โ (๐ = 0 โ (1 + 0) =
0)) |
7 | | oveq2 7370 |
. . . . . . . . 9
โข ((1 + 0)
= 0 โ (((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i
ยท i) ยท (i ยท i)) ยท 0)) |
8 | | ax-icn 11117 |
. . . . . . . . . . . . . . 15
โข i โ
โ |
9 | 8, 8 | mulcli 11169 |
. . . . . . . . . . . . . 14
โข (i
ยท i) โ โ |
10 | 9, 9 | mulcli 11169 |
. . . . . . . . . . . . 13
โข ((i
ยท i) ยท (i ยท i)) โ โ |
11 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
12 | | 0cn 11154 |
. . . . . . . . . . . . 13
โข 0 โ
โ |
13 | 10, 11, 12 | adddii 11174 |
. . . . . . . . . . . 12
โข (((i
ยท i) ยท (i ยท i)) ยท (1 + 0)) = ((((i ยท i)
ยท (i ยท i)) ยท 1) + (((i ยท i) ยท (i ยท
i)) ยท 0)) |
14 | 10 | mulid1i 11166 |
. . . . . . . . . . . . 13
โข (((i
ยท i) ยท (i ยท i)) ยท 1) = ((i ยท i) ยท (i
ยท i)) |
15 | | mul01 11341 |
. . . . . . . . . . . . . . 15
โข (((i
ยท i) ยท (i ยท i)) โ โ โ (((i ยท i)
ยท (i ยท i)) ยท 0) = 0) |
16 | 10, 15 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข (((i
ยท i) ยท (i ยท i)) ยท 0) = 0 |
17 | | ax-i2m1 11126 |
. . . . . . . . . . . . . 14
โข ((i
ยท i) + 1) = 0 |
18 | 16, 17 | eqtr4i 2768 |
. . . . . . . . . . . . 13
โข (((i
ยท i) ยท (i ยท i)) ยท 0) = ((i ยท i) +
1) |
19 | 14, 18 | oveq12i 7374 |
. . . . . . . . . . . 12
โข ((((i
ยท i) ยท (i ยท i)) ยท 1) + (((i ยท i) ยท (i
ยท i)) ยท 0)) = (((i ยท i) ยท (i ยท i)) + ((i
ยท i) + 1)) |
20 | 13, 19 | eqtri 2765 |
. . . . . . . . . . 11
โข (((i
ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i)
ยท (i ยท i)) + ((i ยท i) + 1)) |
21 | 20, 16 | eqeq12i 2755 |
. . . . . . . . . 10
โข ((((i
ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i)
ยท (i ยท i)) ยท 0) โ (((i ยท i) ยท (i
ยท i)) + ((i ยท i) + 1)) = 0) |
22 | 10, 9, 11 | addassi 11172 |
. . . . . . . . . . . 12
โข ((((i
ยท i) ยท (i ยท i)) + (i ยท i)) + 1) = (((i ยท i)
ยท (i ยท i)) + ((i ยท i) + 1)) |
23 | 9 | mulid1i 11166 |
. . . . . . . . . . . . . . 15
โข ((i
ยท i) ยท 1) = (i ยท i) |
24 | 23 | oveq2i 7373 |
. . . . . . . . . . . . . 14
โข (((i
ยท i) ยท (i ยท i)) + ((i ยท i) ยท 1)) = (((i
ยท i) ยท (i ยท i)) + (i ยท i)) |
25 | 9, 9, 11 | adddii 11174 |
. . . . . . . . . . . . . . 15
โข ((i
ยท i) ยท ((i ยท i) + 1)) = (((i ยท i) ยท (i
ยท i)) + ((i ยท i) ยท 1)) |
26 | 17 | oveq2i 7373 |
. . . . . . . . . . . . . . . 16
โข ((i
ยท i) ยท ((i ยท i) + 1)) = ((i ยท i) ยท
0) |
27 | | mul01 11341 |
. . . . . . . . . . . . . . . . 17
โข ((i
ยท i) โ โ โ ((i ยท i) ยท 0) =
0) |
28 | 9, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข ((i
ยท i) ยท 0) = 0 |
29 | 26, 28 | eqtri 2765 |
. . . . . . . . . . . . . . 15
โข ((i
ยท i) ยท ((i ยท i) + 1)) = 0 |
30 | 25, 29 | eqtr3i 2767 |
. . . . . . . . . . . . . 14
โข (((i
ยท i) ยท (i ยท i)) + ((i ยท i) ยท 1)) =
0 |
31 | 24, 30 | eqtr3i 2767 |
. . . . . . . . . . . . 13
โข (((i
ยท i) ยท (i ยท i)) + (i ยท i)) = 0 |
32 | 31 | oveq1i 7372 |
. . . . . . . . . . . 12
โข ((((i
ยท i) ยท (i ยท i)) + (i ยท i)) + 1) = (0 +
1) |
33 | 22, 32 | eqtr3i 2767 |
. . . . . . . . . . 11
โข (((i
ยท i) ยท (i ยท i)) + ((i ยท i) + 1)) = (0 +
1) |
34 | | 00id 11337 |
. . . . . . . . . . . 12
โข (0 + 0) =
0 |
35 | 34 | eqcomi 2746 |
. . . . . . . . . . 11
โข 0 = (0 +
0) |
36 | 33, 35 | eqeq12i 2755 |
. . . . . . . . . 10
โข ((((i
ยท i) ยท (i ยท i)) + ((i ยท i) + 1)) = 0 โ (0 + 1)
= (0 + 0)) |
37 | | 0re 11164 |
. . . . . . . . . . 11
โข 0 โ
โ |
38 | | readdcan 11336 |
. . . . . . . . . . 11
โข ((1
โ โ โง 0 โ โ โง 0 โ โ) โ ((0 + 1) =
(0 + 0) โ 1 = 0)) |
39 | 1, 37, 37, 38 | mp3an 1462 |
. . . . . . . . . 10
โข ((0 + 1)
= (0 + 0) โ 1 = 0) |
40 | 21, 36, 39 | 3bitri 297 |
. . . . . . . . 9
โข ((((i
ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i)
ยท (i ยท i)) ยท 0) โ 1 = 0) |
41 | 7, 40 | sylib 217 |
. . . . . . . 8
โข ((1 + 0)
= 0 โ 1 = 0) |
42 | 6, 41 | syl6 35 |
. . . . . . 7
โข ((1 +
๐) = 0 โ (๐ = 0 โ 1 =
0)) |
43 | 42 | necon3d 2965 |
. . . . . 6
โข ((1 +
๐) = 0 โ (1 โ 0
โ ๐ โ
0)) |
44 | 3, 43 | mpi 20 |
. . . . 5
โข ((1 +
๐) = 0 โ ๐ โ 0) |
45 | | ax-rrecex 11130 |
. . . . 5
โข ((๐ โ โ โง ๐ โ 0) โ โ๐ฅ โ โ (๐ ยท ๐ฅ) = 1) |
46 | 44, 45 | sylan2 594 |
. . . 4
โข ((๐ โ โ โง (1 + ๐) = 0) โ โ๐ฅ โ โ (๐ ยท ๐ฅ) = 1) |
47 | | simpr 486 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ๐ด โ โ) |
48 | | simplrl 776 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ๐ฅ โ โ) |
49 | 48 | recnd 11190 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ๐ฅ โ โ) |
50 | 47, 49 | mulcld 11182 |
. . . . . . . . 9
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (๐ด ยท ๐ฅ) โ โ) |
51 | | simplll 774 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ๐ โ โ) |
52 | 51 | recnd 11190 |
. . . . . . . . 9
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ๐ โ โ) |
53 | 12 | a1i 11 |
. . . . . . . . 9
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ 0 โ
โ) |
54 | 50, 52, 53 | adddid 11186 |
. . . . . . . 8
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((๐ด ยท ๐ฅ) ยท (๐ + 0)) = (((๐ด ยท ๐ฅ) ยท ๐) + ((๐ด ยท ๐ฅ) ยท 0))) |
55 | 11 | a1i 11 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ 1 โ
โ) |
56 | 55, 52, 53 | addassd 11184 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((1 + ๐) + 0) = (1 + (๐ + 0))) |
57 | | simpllr 775 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (1 + ๐) = 0) |
58 | 57 | oveq1d 7377 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((1 + ๐) + 0) = (0 +
0)) |
59 | 56, 58 | eqtr3d 2779 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (1 + (๐ + 0)) = (0 +
0)) |
60 | 34, 59, 57 | 3eqtr4a 2803 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (1 + (๐ + 0)) = (1 + ๐)) |
61 | 37 | a1i 11 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ 0 โ
โ) |
62 | 51, 61 | readdcld 11191 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (๐ + 0) โ โ) |
63 | 1 | a1i 11 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ 1 โ
โ) |
64 | | readdcan 11336 |
. . . . . . . . . . 11
โข (((๐ + 0) โ โ โง ๐ โ โ โง 1 โ
โ) โ ((1 + (๐ +
0)) = (1 + ๐) โ (๐ + 0) = ๐)) |
65 | 62, 51, 63, 64 | syl3anc 1372 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((1 + (๐ + 0)) = (1 + ๐) โ (๐ + 0) = ๐)) |
66 | 60, 65 | mpbid 231 |
. . . . . . . . 9
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (๐ + 0) = ๐) |
67 | 66 | oveq2d 7378 |
. . . . . . . 8
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((๐ด ยท ๐ฅ) ยท (๐ + 0)) = ((๐ด ยท ๐ฅ) ยท ๐)) |
68 | 54, 67 | eqtr3d 2779 |
. . . . . . 7
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (((๐ด ยท ๐ฅ) ยท ๐) + ((๐ด ยท ๐ฅ) ยท 0)) = ((๐ด ยท ๐ฅ) ยท ๐)) |
69 | | mul31 11329 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ฅ โ โ โง ๐ โ โ) โ ((๐ด ยท ๐ฅ) ยท ๐) = ((๐ ยท ๐ฅ) ยท ๐ด)) |
70 | 47, 49, 52, 69 | syl3anc 1372 |
. . . . . . . . 9
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((๐ด ยท ๐ฅ) ยท ๐) = ((๐ ยท ๐ฅ) ยท ๐ด)) |
71 | | simplrr 777 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (๐ ยท ๐ฅ) = 1) |
72 | 71 | oveq1d 7377 |
. . . . . . . . 9
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((๐ ยท ๐ฅ) ยท ๐ด) = (1 ยท ๐ด)) |
73 | 47 | mulid2d 11180 |
. . . . . . . . 9
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (1 ยท ๐ด) = ๐ด) |
74 | 70, 72, 73 | 3eqtrd 2781 |
. . . . . . . 8
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((๐ด ยท ๐ฅ) ยท ๐) = ๐ด) |
75 | | mul01 11341 |
. . . . . . . . 9
โข ((๐ด ยท ๐ฅ) โ โ โ ((๐ด ยท ๐ฅ) ยท 0) = 0) |
76 | 50, 75 | syl 17 |
. . . . . . . 8
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ ((๐ด ยท ๐ฅ) ยท 0) = 0) |
77 | 74, 76 | oveq12d 7380 |
. . . . . . 7
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (((๐ด ยท ๐ฅ) ยท ๐) + ((๐ด ยท ๐ฅ) ยท 0)) = (๐ด + 0)) |
78 | 68, 77, 74 | 3eqtr3d 2785 |
. . . . . 6
โข ((((๐ โ โ โง (1 + ๐) = 0) โง (๐ฅ โ โ โง (๐ ยท ๐ฅ) = 1)) โง ๐ด โ โ) โ (๐ด + 0) = ๐ด) |
79 | 78 | exp42 437 |
. . . . 5
โข ((๐ โ โ โง (1 + ๐) = 0) โ (๐ฅ โ โ โ ((๐ ยท ๐ฅ) = 1 โ (๐ด โ โ โ (๐ด + 0) = ๐ด)))) |
80 | 79 | rexlimdv 3151 |
. . . 4
โข ((๐ โ โ โง (1 + ๐) = 0) โ (โ๐ฅ โ โ (๐ ยท ๐ฅ) = 1 โ (๐ด โ โ โ (๐ด + 0) = ๐ด))) |
81 | 46, 80 | mpd 15 |
. . 3
โข ((๐ โ โ โง (1 + ๐) = 0) โ (๐ด โ โ โ (๐ด + 0) = ๐ด)) |
82 | 81 | rexlimiva 3145 |
. 2
โข
(โ๐ โ
โ (1 + ๐) = 0 โ
(๐ด โ โ โ
(๐ด + 0) = ๐ด)) |
83 | 1, 2, 82 | mp2b 10 |
1
โข (๐ด โ โ โ (๐ด + 0) = ๐ด) |