Step | Hyp | Ref
| Expression |
1 | | modxai.9 |
. . . . 5
โข (๐ต + ๐ถ) = ๐ธ |
2 | 1 | oveq2i 7373 |
. . . 4
โข (๐ดโ(๐ต + ๐ถ)) = (๐ดโ๐ธ) |
3 | | modxai.2 |
. . . . . 6
โข ๐ด โ โ |
4 | 3 | nncni 12170 |
. . . . 5
โข ๐ด โ โ |
5 | | modxai.3 |
. . . . 5
โข ๐ต โ
โ0 |
6 | | modxai.7 |
. . . . 5
โข ๐ถ โ
โ0 |
7 | | expadd 14017 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ0
โง ๐ถ โ
โ0) โ (๐ดโ(๐ต + ๐ถ)) = ((๐ดโ๐ต) ยท (๐ดโ๐ถ))) |
8 | 4, 5, 6, 7 | mp3an 1462 |
. . . 4
โข (๐ดโ(๐ต + ๐ถ)) = ((๐ดโ๐ต) ยท (๐ดโ๐ถ)) |
9 | 2, 8 | eqtr3i 2767 |
. . 3
โข (๐ดโ๐ธ) = ((๐ดโ๐ต) ยท (๐ดโ๐ถ)) |
10 | 9 | oveq1i 7372 |
. 2
โข ((๐ดโ๐ธ) mod ๐) = (((๐ดโ๐ต) ยท (๐ดโ๐ถ)) mod ๐) |
11 | | nnexpcl 13987 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ0)
โ (๐ดโ๐ต) โ
โ) |
12 | 3, 5, 11 | mp2an 691 |
. . . . . . . 8
โข (๐ดโ๐ต) โ โ |
13 | 12 | nnzi 12534 |
. . . . . . 7
โข (๐ดโ๐ต) โ โค |
14 | 13 | a1i 11 |
. . . . . 6
โข (โค
โ (๐ดโ๐ต) โ
โค) |
15 | | modxai.5 |
. . . . . . . 8
โข ๐พ โ
โ0 |
16 | 15 | nn0zi 12535 |
. . . . . . 7
โข ๐พ โ โค |
17 | 16 | a1i 11 |
. . . . . 6
โข (โค
โ ๐พ โ
โค) |
18 | | nnexpcl 13987 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ถ โ โ0)
โ (๐ดโ๐ถ) โ
โ) |
19 | 3, 6, 18 | mp2an 691 |
. . . . . . . 8
โข (๐ดโ๐ถ) โ โ |
20 | 19 | nnzi 12534 |
. . . . . . 7
โข (๐ดโ๐ถ) โ โค |
21 | 20 | a1i 11 |
. . . . . 6
โข (โค
โ (๐ดโ๐ถ) โ
โค) |
22 | | modxai.8 |
. . . . . . . 8
โข ๐ฟ โ
โ0 |
23 | 22 | nn0zi 12535 |
. . . . . . 7
โข ๐ฟ โ โค |
24 | 23 | a1i 11 |
. . . . . 6
โข (โค
โ ๐ฟ โ
โค) |
25 | | modxai.1 |
. . . . . . . 8
โข ๐ โ โ |
26 | | nnrp 12933 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ+) |
27 | 25, 26 | ax-mp 5 |
. . . . . . 7
โข ๐ โ
โ+ |
28 | 27 | a1i 11 |
. . . . . 6
โข (โค
โ ๐ โ
โ+) |
29 | | modxai.11 |
. . . . . . 7
โข ((๐ดโ๐ต) mod ๐) = (๐พ mod ๐) |
30 | 29 | a1i 11 |
. . . . . 6
โข (โค
โ ((๐ดโ๐ต) mod ๐) = (๐พ mod ๐)) |
31 | | modxai.12 |
. . . . . . 7
โข ((๐ดโ๐ถ) mod ๐) = (๐ฟ mod ๐) |
32 | 31 | a1i 11 |
. . . . . 6
โข (โค
โ ((๐ดโ๐ถ) mod ๐) = (๐ฟ mod ๐)) |
33 | 14, 17, 21, 24, 28, 30, 32 | modmul12d 13837 |
. . . . 5
โข (โค
โ (((๐ดโ๐ต) ยท (๐ดโ๐ถ)) mod ๐) = ((๐พ ยท ๐ฟ) mod ๐)) |
34 | 33 | mptru 1549 |
. . . 4
โข (((๐ดโ๐ต) ยท (๐ดโ๐ถ)) mod ๐) = ((๐พ ยท ๐ฟ) mod ๐) |
35 | | modxai.10 |
. . . . . 6
โข ((๐ท ยท ๐) + ๐) = (๐พ ยท ๐ฟ) |
36 | | modxai.4 |
. . . . . . . . 9
โข ๐ท โ โค |
37 | | zcn 12511 |
. . . . . . . . 9
โข (๐ท โ โค โ ๐ท โ
โ) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . 8
โข ๐ท โ โ |
39 | 25 | nncni 12170 |
. . . . . . . 8
โข ๐ โ โ |
40 | 38, 39 | mulcli 11169 |
. . . . . . 7
โข (๐ท ยท ๐) โ โ |
41 | | modxai.6 |
. . . . . . . 8
โข ๐ โ
โ0 |
42 | 41 | nn0cni 12432 |
. . . . . . 7
โข ๐ โ โ |
43 | 40, 42 | addcomi 11353 |
. . . . . 6
โข ((๐ท ยท ๐) + ๐) = (๐ + (๐ท ยท ๐)) |
44 | 35, 43 | eqtr3i 2767 |
. . . . 5
โข (๐พ ยท ๐ฟ) = (๐ + (๐ท ยท ๐)) |
45 | 44 | oveq1i 7372 |
. . . 4
โข ((๐พ ยท ๐ฟ) mod ๐) = ((๐ + (๐ท ยท ๐)) mod ๐) |
46 | 34, 45 | eqtri 2765 |
. . 3
โข (((๐ดโ๐ต) ยท (๐ดโ๐ถ)) mod ๐) = ((๐ + (๐ท ยท ๐)) mod ๐) |
47 | 41 | nn0rei 12431 |
. . . 4
โข ๐ โ โ |
48 | | modcyc 13818 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ+
โง ๐ท โ โค)
โ ((๐ + (๐ท ยท ๐)) mod ๐) = (๐ mod ๐)) |
49 | 47, 27, 36, 48 | mp3an 1462 |
. . 3
โข ((๐ + (๐ท ยท ๐)) mod ๐) = (๐ mod ๐) |
50 | 46, 49 | eqtri 2765 |
. 2
โข (((๐ดโ๐ต) ยท (๐ดโ๐ถ)) mod ๐) = (๐ mod ๐) |
51 | 10, 50 | eqtri 2765 |
1
โข ((๐ดโ๐ธ) mod ๐) = (๐ mod ๐) |