Step | Hyp | Ref
| Expression |
1 | | ax-icn 11171 |
. . . . . . . . . 10
โข i โ
โ |
2 | 1 | a1i 11 |
. . . . . . . . 9
โข (๐ฆ โ โ โ i โ
โ) |
3 | | rernegcl 41546 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (0
โโ ๐ฆ) โ โ) |
4 | 3 | recnd 11246 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (0
โโ ๐ฆ) โ โ) |
5 | 2, 4 | mulcld 11238 |
. . . . . . . 8
โข (๐ฆ โ โ โ (i
ยท (0 โโ ๐ฆ)) โ โ) |
6 | 5 | adantl 480 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (i
ยท (0 โโ ๐ฆ)) โ โ) |
7 | | rernegcl 41546 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (0
โโ ๐ฅ) โ โ) |
8 | 7 | recnd 11246 |
. . . . . . . 8
โข (๐ฅ โ โ โ (0
โโ ๐ฅ) โ โ) |
9 | 8 | adantr 479 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0
โโ ๐ฅ) โ โ) |
10 | 6, 9 | addcld 11237 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((i
ยท (0 โโ ๐ฆ)) + (0 โโ ๐ฅ)) โ
โ) |
11 | 10 | adantl 480 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((i
ยท (0 โโ ๐ฆ)) + (0 โโ ๐ฅ)) โ
โ) |
12 | | eqeq1 2734 |
. . . . . 6
โข (๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โ (๐ = ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ)) โ ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)))) |
13 | 12 | adantl 480 |
. . . . 5
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ))) โ (๐ = ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ)) โ ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)))) |
14 | | eqidd 2731 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((i
ยท (0 โโ ๐ฆ)) + (0 โโ ๐ฅ)) = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ))) |
15 | 11, 13, 14 | rspcedvd 3613 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
โ๐ โ โ
๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ))) |
16 | 15 | ralrimivva 3198 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ โ โ
๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ))) |
17 | | cnre 11215 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |
18 | 16, 17 | r19.29d2r 3138 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
(โ๐ โ โ
๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ)))) |
19 | | oveq1 7418 |
. . . . . . . . . . . 12
โข (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ด + (i ยท (0 โโ
๐ฆ))) = ((๐ฅ + (i ยท ๐ฆ)) + (i ยท (0 โโ
๐ฆ)))) |
20 | 19 | adantl 480 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด + (i ยท (0 โโ
๐ฆ))) = ((๐ฅ + (i ยท ๐ฆ)) + (i ยท (0 โโ
๐ฆ)))) |
21 | | recn 11202 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
22 | 21 | adantr 479 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ๐ฅ โ
โ) |
23 | 1 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ i โ
โ) |
24 | | recn 11202 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
25 | 24 | adantl 480 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ๐ฆ โ
โ) |
26 | 23, 25 | mulcld 11238 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (i
ยท ๐ฆ) โ
โ) |
27 | 22, 26, 6 | addassd 11240 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ + (i ยท ๐ฆ)) + (i ยท (0
โโ ๐ฆ))) = (๐ฅ + ((i ยท ๐ฆ) + (i ยท (0 โโ
๐ฆ))))) |
28 | | renegid 41548 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ โ (๐ฆ + (0 โโ
๐ฆ)) = 0) |
29 | 28 | oveq2d 7427 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (i
ยท (๐ฆ + (0
โโ ๐ฆ))) = (i ยท 0)) |
30 | 2, 24, 4 | adddid 11242 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (i
ยท (๐ฆ + (0
โโ ๐ฆ))) = ((i ยท ๐ฆ) + (i ยท (0 โโ
๐ฆ)))) |
31 | | sn-it0e0 41590 |
. . . . . . . . . . . . . . . . 17
โข (i
ยท 0) = 0 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (i
ยท 0) = 0) |
33 | 29, 30, 32 | 3eqtr3d 2778 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ((i
ยท ๐ฆ) + (i ยท
(0 โโ ๐ฆ))) = 0) |
34 | 33 | oveq2d 7427 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (๐ฅ + ((i ยท ๐ฆ) + (i ยท (0
โโ ๐ฆ)))) = (๐ฅ + 0)) |
35 | 34 | adantl 480 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ + ((i ยท ๐ฆ) + (i ยท (0
โโ ๐ฆ)))) = (๐ฅ + 0)) |
36 | | readdrid 41584 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ (๐ฅ + 0) = ๐ฅ) |
37 | 36 | adantr 479 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ + 0) = ๐ฅ) |
38 | 27, 35, 37 | 3eqtrd 2774 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ + (i ยท ๐ฆ)) + (i ยท (0
โโ ๐ฆ))) = ๐ฅ) |
39 | 38 | ad2antlr 723 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ฅ + (i ยท ๐ฆ)) + (i ยท (0 โโ
๐ฆ))) = ๐ฅ) |
40 | 20, 39 | eqtrd 2770 |
. . . . . . . . . 10
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด + (i ยท (0 โโ
๐ฆ))) = ๐ฅ) |
41 | 40 | oveq1d 7426 |
. . . . . . . . 9
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ด + (i ยท (0 โโ
๐ฆ))) + (0
โโ ๐ฅ)) = (๐ฅ + (0 โโ ๐ฅ))) |
42 | | simpll 763 |
. . . . . . . . . 10
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ด โ โ) |
43 | 6 | ad2antlr 723 |
. . . . . . . . . 10
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (i ยท (0
โโ ๐ฆ)) โ โ) |
44 | 9 | ad2antlr 723 |
. . . . . . . . . 10
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (0 โโ ๐ฅ) โ
โ) |
45 | 42, 43, 44 | addassd 11240 |
. . . . . . . . 9
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ด + (i ยท (0 โโ
๐ฆ))) + (0
โโ ๐ฅ)) = (๐ด + ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ)))) |
46 | | renegid 41548 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ (๐ฅ + (0 โโ
๐ฅ)) = 0) |
47 | 46 | adantr 479 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ + (0 โโ
๐ฅ)) = 0) |
48 | 47 | ad2antlr 723 |
. . . . . . . . 9
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ฅ + (0 โโ ๐ฅ)) = 0) |
49 | 41, 45, 48 | 3eqtr3d 2778 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด + ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ))) = 0) |
50 | | oveq2 7419 |
. . . . . . . . 9
โข (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) + ๐ด) = (((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) + (๐ฅ + (i ยท ๐ฆ)))) |
51 | 22, 26 | addcld 11237 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ + (i ยท ๐ฆ)) โ
โ) |
52 | 6, 9, 51 | addassd 11240 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((i
ยท (0 โโ ๐ฆ)) + (0 โโ ๐ฅ)) + (๐ฅ + (i ยท ๐ฆ))) = ((i ยท (0
โโ ๐ฆ)) + ((0 โโ ๐ฅ) + (๐ฅ + (i ยท ๐ฆ))))) |
53 | 9, 22, 26 | addassd 11240 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((0
โโ ๐ฅ) + ๐ฅ) + (i ยท ๐ฆ)) = ((0 โโ ๐ฅ) + (๐ฅ + (i ยท ๐ฆ)))) |
54 | 53 | oveq2d 7427 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((i
ยท (0 โโ ๐ฆ)) + (((0 โโ ๐ฅ) + ๐ฅ) + (i ยท ๐ฆ))) = ((i ยท (0
โโ ๐ฆ)) + ((0 โโ ๐ฅ) + (๐ฅ + (i ยท ๐ฆ))))) |
55 | | renegid2 41588 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โ โ ((0
โโ ๐ฅ) + ๐ฅ) = 0) |
56 | 55 | adantr 479 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((0
โโ ๐ฅ) + ๐ฅ) = 0) |
57 | 56 | oveq1d 7426 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((0
โโ ๐ฅ) + ๐ฅ) + (i ยท ๐ฆ)) = (0 + (i ยท ๐ฆ))) |
58 | | sn-addlid 41579 |
. . . . . . . . . . . . . . 15
โข ((i
ยท ๐ฆ) โ โ
โ (0 + (i ยท ๐ฆ))
= (i ยท ๐ฆ)) |
59 | 26, 58 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0 + (i
ยท ๐ฆ)) = (i ยท
๐ฆ)) |
60 | 57, 59 | eqtrd 2770 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((0
โโ ๐ฅ) + ๐ฅ) + (i ยท ๐ฆ)) = (i ยท ๐ฆ)) |
61 | 60 | oveq2d 7427 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((i
ยท (0 โโ ๐ฆ)) + (((0 โโ ๐ฅ) + ๐ฅ) + (i ยท ๐ฆ))) = ((i ยท (0
โโ ๐ฆ)) + (i ยท ๐ฆ))) |
62 | 4 | adantl 480 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0
โโ ๐ฆ) โ โ) |
63 | 23, 62, 25 | adddid 11242 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (i
ยท ((0 โโ ๐ฆ) + ๐ฆ)) = ((i ยท (0
โโ ๐ฆ)) + (i ยท ๐ฆ))) |
64 | | renegid2 41588 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ((0
โโ ๐ฆ) + ๐ฆ) = 0) |
65 | 64 | adantl 480 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((0
โโ ๐ฆ) + ๐ฆ) = 0) |
66 | 65 | oveq2d 7427 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (i
ยท ((0 โโ ๐ฆ) + ๐ฆ)) = (i ยท 0)) |
67 | 66, 31 | eqtrdi 2786 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (i
ยท ((0 โโ ๐ฆ) + ๐ฆ)) = 0) |
68 | 61, 63, 67 | 3eqtr2d 2776 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((i
ยท (0 โโ ๐ฆ)) + (((0 โโ ๐ฅ) + ๐ฅ) + (i ยท ๐ฆ))) = 0) |
69 | 52, 54, 68 | 3eqtr2d 2776 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((i
ยท (0 โโ ๐ฆ)) + (0 โโ ๐ฅ)) + (๐ฅ + (i ยท ๐ฆ))) = 0) |
70 | 69 | adantl 480 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((i
ยท (0 โโ ๐ฆ)) + (0 โโ ๐ฅ)) + (๐ฅ + (i ยท ๐ฆ))) = 0) |
71 | 50, 70 | sylan9eqr 2792 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) + ๐ด) = 0) |
72 | 49, 71 | jca 510 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ด + ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ))) = 0 โง (((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) + ๐ด) = 0)) |
73 | | oveq2 7419 |
. . . . . . . . 9
โข (๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โ (๐ด + ๐) = (๐ด + ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ)))) |
74 | 73 | eqeq1d 2732 |
. . . . . . . 8
โข (๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โ ((๐ด + ๐) = 0 โ (๐ด + ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ))) = 0)) |
75 | | oveq1 7418 |
. . . . . . . . 9
โข (๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โ (๐ + ๐ด) = (((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) + ๐ด)) |
76 | 75 | eqeq1d 2732 |
. . . . . . . 8
โข (๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โ ((๐ + ๐ด) = 0 โ (((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) + ๐ด) = 0)) |
77 | 74, 76 | anbi12d 629 |
. . . . . . 7
โข (๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โ (((๐ด + ๐) = 0 โง (๐ + ๐ด) = 0) โ ((๐ด + ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ))) = 0 โง (((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) + ๐ด) = 0))) |
78 | 72, 77 | syl5ibrcom 246 |
. . . . . 6
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ = ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ)) โ ((๐ด + ๐) = 0 โง (๐ + ๐ด) = 0))) |
79 | 78 | reximdv 3168 |
. . . . 5
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (โ๐ โ โ ๐ = ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ)) โ โ๐ โ โ ((๐ด + ๐) = 0 โง (๐ + ๐ด) = 0))) |
80 | 79 | expimpd 452 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด = (๐ฅ + (i ยท ๐ฆ)) โง โ๐ โ โ ๐ = ((i ยท (0 โโ
๐ฆ)) + (0
โโ ๐ฅ))) โ โ๐ โ โ ((๐ด + ๐) = 0 โง (๐ + ๐ด) = 0))) |
81 | 80 | ancomsd 464 |
. . 3
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((โ๐ โ โ
๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ โ๐ โ โ ((๐ด + ๐) = 0 โง (๐ + ๐ด) = 0))) |
82 | 81 | rexlimdvva 3209 |
. 2
โข (๐ด โ โ โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
(โ๐ โ โ
๐ = ((i ยท (0
โโ ๐ฆ)) + (0 โโ ๐ฅ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ โ๐ โ โ ((๐ด + ๐) = 0 โง (๐ + ๐ด) = 0))) |
83 | 18, 82 | mpd 15 |
1
โข (๐ด โ โ โ
โ๐ โ โ
((๐ด + ๐) = 0 โง (๐ + ๐ด) = 0)) |