Step | Hyp | Ref
| Expression |
1 | | oveq2 7419 |
. . . . . . . . . . 11
โข (๐ = 0 โ (1 โ ๐) = (1 โ
0)) |
2 | | 1m0e1 12335 |
. . . . . . . . . . 11
โข (1
โ 0) = 1 |
3 | 1, 2 | eqtrdi 2788 |
. . . . . . . . . 10
โข (๐ = 0 โ (1 โ ๐) = 1) |
4 | 3 | oveq1d 7426 |
. . . . . . . . 9
โข (๐ = 0 โ ((1 โ ๐) ยท (๐ดโ๐)) = (1 ยท (๐ดโ๐))) |
5 | | oveq1 7418 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ ยท (๐ถโ๐)) = (0 ยท (๐ถโ๐))) |
6 | 4, 5 | oveq12d 7429 |
. . . . . . . 8
โข (๐ = 0 โ (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) = ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐)))) |
7 | 6 | eqeq2d 2743 |
. . . . . . 7
โข (๐ = 0 โ ((๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โ (๐ตโ๐) = ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))))) |
8 | 7 | ralbidv 3177 |
. . . . . 6
โข (๐ = 0 โ (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โ โ๐ โ (1...๐)(๐ตโ๐) = ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))))) |
9 | 8 | biimpac 479 |
. . . . 5
โข
((โ๐ โ
(1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โง ๐ = 0) โ โ๐ โ (1...๐)(๐ตโ๐) = ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐)))) |
10 | | eqeefv 28199 |
. . . . . . . 8
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (๐ด = ๐ต โ โ๐ โ (1...๐)(๐ดโ๐) = (๐ตโ๐))) |
11 | 10 | 3adant1 1130 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (๐ด = ๐ต โ โ๐ โ (1...๐)(๐ดโ๐) = (๐ตโ๐))) |
12 | 11 | 3adant3r3 1184 |
. . . . . 6
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โ (๐ด = ๐ต โ โ๐ โ (1...๐)(๐ดโ๐) = (๐ตโ๐))) |
13 | | simplr1 1215 |
. . . . . . . . . . 11
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ๐ด โ (๐ผโ๐)) |
14 | | fveecn 28198 |
. . . . . . . . . . 11
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
15 | 13, 14 | sylancom 588 |
. . . . . . . . . 10
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
16 | | simplr3 1217 |
. . . . . . . . . . 11
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ๐ถ โ (๐ผโ๐)) |
17 | | fveecn 28198 |
. . . . . . . . . . 11
โข ((๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
18 | 16, 17 | sylancom 588 |
. . . . . . . . . 10
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
19 | | mullid 11215 |
. . . . . . . . . . . 12
โข ((๐ดโ๐) โ โ โ (1 ยท (๐ดโ๐)) = (๐ดโ๐)) |
20 | | mul02 11394 |
. . . . . . . . . . . 12
โข ((๐ถโ๐) โ โ โ (0 ยท (๐ถโ๐)) = 0) |
21 | 19, 20 | oveqan12d 7430 |
. . . . . . . . . . 11
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))) = ((๐ดโ๐) + 0)) |
22 | | addrid 11396 |
. . . . . . . . . . . 12
โข ((๐ดโ๐) โ โ โ ((๐ดโ๐) + 0) = (๐ดโ๐)) |
23 | 22 | adantr 481 |
. . . . . . . . . . 11
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ดโ๐) + 0) = (๐ดโ๐)) |
24 | 21, 23 | eqtrd 2772 |
. . . . . . . . . 10
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))) = (๐ดโ๐)) |
25 | 15, 18, 24 | syl2anc 584 |
. . . . . . . . 9
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))) = (๐ดโ๐)) |
26 | 25 | eqeq1d 2734 |
. . . . . . . 8
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))) = (๐ตโ๐) โ (๐ดโ๐) = (๐ตโ๐))) |
27 | | eqcom 2739 |
. . . . . . . 8
โข (((1
ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))) = (๐ตโ๐) โ (๐ตโ๐) = ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐)))) |
28 | 26, 27 | bitr3di 285 |
. . . . . . 7
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((๐ดโ๐) = (๐ตโ๐) โ (๐ตโ๐) = ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))))) |
29 | 28 | ralbidva 3175 |
. . . . . 6
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โ (โ๐ โ (1...๐)(๐ดโ๐) = (๐ตโ๐) โ โ๐ โ (1...๐)(๐ตโ๐) = ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))))) |
30 | 12, 29 | bitrd 278 |
. . . . 5
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โ (๐ด = ๐ต โ โ๐ โ (1...๐)(๐ตโ๐) = ((1 ยท (๐ดโ๐)) + (0 ยท (๐ถโ๐))))) |
31 | 9, 30 | imbitrrid 245 |
. . . 4
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โ ((โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โง ๐ = 0) โ ๐ด = ๐ต)) |
32 | 31 | expdimp 453 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) โ (๐ = 0 โ ๐ด = ๐ต)) |
33 | 32 | necon3d 2961 |
. 2
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) โ (๐ด โ ๐ต โ ๐ โ 0)) |
34 | 33 | 3impia 1117 |
1
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โง ๐ด โ ๐ต) โ ๐ โ 0) |