Step | Hyp | Ref
| Expression |
1 | | pinn 10869 |
. . . 4
โข (๐ด โ N โ
๐ด โ
ฯ) |
2 | | pinn 10869 |
. . . 4
โข (๐ต โ N โ
๐ต โ
ฯ) |
3 | | pinn 10869 |
. . . 4
โข (๐ถ โ N โ
๐ถ โ
ฯ) |
4 | | nndi 8619 |
. . . 4
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ (๐ด ยทo (๐ต +o ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))) |
5 | 1, 2, 3, 4 | syl3an 1160 |
. . 3
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ (๐ด
ยทo (๐ต
+o ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))) |
6 | | addclpi 10883 |
. . . . . 6
โข ((๐ต โ N โง
๐ถ โ N)
โ (๐ต
+N ๐ถ) โ N) |
7 | | mulpiord 10876 |
. . . . . 6
โข ((๐ด โ N โง
(๐ต
+N ๐ถ) โ N) โ (๐ด
ยทN (๐ต +N ๐ถ)) = (๐ด ยทo (๐ต +N ๐ถ))) |
8 | 6, 7 | sylan2 593 |
. . . . 5
โข ((๐ด โ N โง
(๐ต โ N
โง ๐ถ โ
N)) โ (๐ด
ยทN (๐ต +N ๐ถ)) = (๐ด ยทo (๐ต +N ๐ถ))) |
9 | | addpiord 10875 |
. . . . . . 7
โข ((๐ต โ N โง
๐ถ โ N)
โ (๐ต
+N ๐ถ) = (๐ต +o ๐ถ)) |
10 | 9 | oveq2d 7421 |
. . . . . 6
โข ((๐ต โ N โง
๐ถ โ N)
โ (๐ด
ยทo (๐ต
+N ๐ถ)) = (๐ด ยทo (๐ต +o ๐ถ))) |
11 | 10 | adantl 482 |
. . . . 5
โข ((๐ด โ N โง
(๐ต โ N
โง ๐ถ โ
N)) โ (๐ด
ยทo (๐ต
+N ๐ถ)) = (๐ด ยทo (๐ต +o ๐ถ))) |
12 | 8, 11 | eqtrd 2772 |
. . . 4
โข ((๐ด โ N โง
(๐ต โ N
โง ๐ถ โ
N)) โ (๐ด
ยทN (๐ต +N ๐ถ)) = (๐ด ยทo (๐ต +o ๐ถ))) |
13 | 12 | 3impb 1115 |
. . 3
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ (๐ด
ยทN (๐ต +N ๐ถ)) = (๐ด ยทo (๐ต +o ๐ถ))) |
14 | | mulclpi 10884 |
. . . . . 6
โข ((๐ด โ N โง
๐ต โ N)
โ (๐ด
ยทN ๐ต) โ N) |
15 | | mulclpi 10884 |
. . . . . 6
โข ((๐ด โ N โง
๐ถ โ N)
โ (๐ด
ยทN ๐ถ) โ N) |
16 | | addpiord 10875 |
. . . . . 6
โข (((๐ด
ยทN ๐ต) โ N โง (๐ด
ยทN ๐ถ) โ N) โ ((๐ด
ยทN ๐ต) +N (๐ด
ยทN ๐ถ)) = ((๐ด ยทN ๐ต) +o (๐ด
ยทN ๐ถ))) |
17 | 14, 15, 16 | syl2an 596 |
. . . . 5
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ด โ
N โง ๐ถ
โ N)) โ ((๐ด ยทN ๐ต) +N
(๐ด
ยทN ๐ถ)) = ((๐ด ยทN ๐ต) +o (๐ด
ยทN ๐ถ))) |
18 | | mulpiord 10876 |
. . . . . 6
โข ((๐ด โ N โง
๐ต โ N)
โ (๐ด
ยทN ๐ต) = (๐ด ยทo ๐ต)) |
19 | | mulpiord 10876 |
. . . . . 6
โข ((๐ด โ N โง
๐ถ โ N)
โ (๐ด
ยทN ๐ถ) = (๐ด ยทo ๐ถ)) |
20 | 18, 19 | oveqan12d 7424 |
. . . . 5
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ด โ
N โง ๐ถ
โ N)) โ ((๐ด ยทN ๐ต) +o (๐ด
ยทN ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))) |
21 | 17, 20 | eqtrd 2772 |
. . . 4
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ด โ
N โง ๐ถ
โ N)) โ ((๐ด ยทN ๐ต) +N
(๐ด
ยทN ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))) |
22 | 21 | 3impdi 1350 |
. . 3
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ ((๐ด
ยทN ๐ต) +N (๐ด
ยทN ๐ถ)) = ((๐ด ยทo ๐ต) +o (๐ด ยทo ๐ถ))) |
23 | 5, 13, 22 | 3eqtr4d 2782 |
. 2
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ (๐ด
ยทN (๐ต +N ๐ถ)) = ((๐ด ยทN ๐ต) +N
(๐ด
ยทN ๐ถ))) |
24 | | dmaddpi 10881 |
. . 3
โข dom
+N = (N ร
N) |
25 | | 0npi 10873 |
. . 3
โข ยฌ
โ
โ N |
26 | | dmmulpi 10882 |
. . 3
โข dom
ยทN = (N ร
N) |
27 | 24, 25, 26 | ndmovdistr 7592 |
. 2
โข (ยฌ
(๐ด โ N
โง ๐ต โ
N โง ๐ถ
โ N) โ (๐ด ยทN (๐ต +N
๐ถ)) = ((๐ด ยทN ๐ต) +N
(๐ด
ยทN ๐ถ))) |
28 | 23, 27 | pm2.61i 182 |
1
โข (๐ด
ยทN (๐ต +N ๐ถ)) = ((๐ด ยทN ๐ต) +N
(๐ด
ยทN ๐ถ)) |