Step | Hyp | Ref
| Expression |
1 | | mod2xnegi.8 |
. . 3
โข (๐ฟ + ๐พ) = ๐ |
2 | | mod2xnegi.6 |
. . . 4
โข ๐ฟ โ
โ0 |
3 | | mod2xnegi.4 |
. . . 4
โข ๐พ โ โ |
4 | | nn0nnaddcl 12451 |
. . . 4
โข ((๐ฟ โ โ0
โง ๐พ โ โ)
โ (๐ฟ + ๐พ) โ
โ) |
5 | 2, 3, 4 | mp2an 691 |
. . 3
โข (๐ฟ + ๐พ) โ โ |
6 | 1, 5 | eqeltrri 2835 |
. 2
โข ๐ โ โ |
7 | | mod2xnegi.1 |
. 2
โข ๐ด โ โ |
8 | | mod2xnegi.2 |
. 2
โข ๐ต โ
โ0 |
9 | 6 | nnzi 12534 |
. . . 4
โข ๐ โ โค |
10 | | mod2xnegi.3 |
. . . 4
โข ๐ท โ โค |
11 | | zaddcl 12550 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โค) โ (๐ + ๐ท) โ โค) |
12 | 9, 10, 11 | mp2an 691 |
. . 3
โข (๐ + ๐ท) โ โค |
13 | 3 | nnnn0i 12428 |
. . . . 5
โข ๐พ โ
โ0 |
14 | 13, 13 | nn0addcli 12457 |
. . . 4
โข (๐พ + ๐พ) โ
โ0 |
15 | 14 | nn0zi 12535 |
. . 3
โข (๐พ + ๐พ) โ โค |
16 | | zsubcl 12552 |
. . 3
โข (((๐ + ๐ท) โ โค โง (๐พ + ๐พ) โ โค) โ ((๐ + ๐ท) โ (๐พ + ๐พ)) โ โค) |
17 | 12, 15, 16 | mp2an 691 |
. 2
โข ((๐ + ๐ท) โ (๐พ + ๐พ)) โ โค |
18 | | mod2xnegi.5 |
. 2
โข ๐ โ
โ0 |
19 | | mod2xnegi.10 |
. 2
โข ((๐ดโ๐ต) mod ๐) = (๐ฟ mod ๐) |
20 | | mod2xnegi.7 |
. 2
โข (2
ยท ๐ต) = ๐ธ |
21 | 6 | nncni 12170 |
. . . . . 6
โข ๐ โ โ |
22 | | zcn 12511 |
. . . . . . 7
โข (๐ท โ โค โ ๐ท โ
โ) |
23 | 10, 22 | ax-mp 5 |
. . . . . 6
โข ๐ท โ โ |
24 | 21, 23 | addcli 11168 |
. . . . 5
โข (๐ + ๐ท) โ โ |
25 | 3 | nncni 12170 |
. . . . . 6
โข ๐พ โ โ |
26 | 25, 25 | addcli 11168 |
. . . . 5
โข (๐พ + ๐พ) โ โ |
27 | 24, 26, 21 | subdiri 11612 |
. . . 4
โข (((๐ + ๐ท) โ (๐พ + ๐พ)) ยท ๐) = (((๐ + ๐ท) ยท ๐) โ ((๐พ + ๐พ) ยท ๐)) |
28 | 27 | oveq1i 7372 |
. . 3
โข ((((๐ + ๐ท) โ (๐พ + ๐พ)) ยท ๐) + ๐) = ((((๐ + ๐ท) ยท ๐) โ ((๐พ + ๐พ) ยท ๐)) + ๐) |
29 | 24, 21 | mulcli 11169 |
. . . 4
โข ((๐ + ๐ท) ยท ๐) โ โ |
30 | 18 | nn0cni 12432 |
. . . 4
โข ๐ โ โ |
31 | 26, 21 | mulcli 11169 |
. . . 4
โข ((๐พ + ๐พ) ยท ๐) โ โ |
32 | 29, 30, 31 | addsubi 11500 |
. . 3
โข ((((๐ + ๐ท) ยท ๐) + ๐) โ ((๐พ + ๐พ) ยท ๐)) = ((((๐ + ๐ท) ยท ๐) โ ((๐พ + ๐พ) ยท ๐)) + ๐) |
33 | | mod2xnegi.9 |
. . . . . . 7
โข ((๐ท ยท ๐) + ๐) = (๐พ ยท ๐พ) |
34 | 33 | oveq2i 7373 |
. . . . . 6
โข ((๐ ยท ๐) + ((๐ท ยท ๐) + ๐)) = ((๐ ยท ๐) + (๐พ ยท ๐พ)) |
35 | 21, 25, 25 | adddii 11174 |
. . . . . 6
โข (๐ ยท (๐พ + ๐พ)) = ((๐ ยท ๐พ) + (๐ ยท ๐พ)) |
36 | 34, 35 | oveq12i 7374 |
. . . . 5
โข (((๐ ยท ๐) + ((๐ท ยท ๐) + ๐)) โ (๐ ยท (๐พ + ๐พ))) = (((๐ ยท ๐) + (๐พ ยท ๐พ)) โ ((๐ ยท ๐พ) + (๐ ยท ๐พ))) |
37 | 21, 23, 21 | adddiri 11175 |
. . . . . . . 8
โข ((๐ + ๐ท) ยท ๐) = ((๐ ยท ๐) + (๐ท ยท ๐)) |
38 | 37 | oveq1i 7372 |
. . . . . . 7
โข (((๐ + ๐ท) ยท ๐) + ๐) = (((๐ ยท ๐) + (๐ท ยท ๐)) + ๐) |
39 | 21, 21 | mulcli 11169 |
. . . . . . . 8
โข (๐ ยท ๐) โ โ |
40 | 23, 21 | mulcli 11169 |
. . . . . . . 8
โข (๐ท ยท ๐) โ โ |
41 | 39, 40, 30 | addassi 11172 |
. . . . . . 7
โข (((๐ ยท ๐) + (๐ท ยท ๐)) + ๐) = ((๐ ยท ๐) + ((๐ท ยท ๐) + ๐)) |
42 | 38, 41 | eqtr2i 2766 |
. . . . . 6
โข ((๐ ยท ๐) + ((๐ท ยท ๐) + ๐)) = (((๐ + ๐ท) ยท ๐) + ๐) |
43 | 21, 26 | mulcomi 11170 |
. . . . . 6
โข (๐ ยท (๐พ + ๐พ)) = ((๐พ + ๐พ) ยท ๐) |
44 | 42, 43 | oveq12i 7374 |
. . . . 5
โข (((๐ ยท ๐) + ((๐ท ยท ๐) + ๐)) โ (๐ ยท (๐พ + ๐พ))) = ((((๐ + ๐ท) ยท ๐) + ๐) โ ((๐พ + ๐พ) ยท ๐)) |
45 | 36, 44 | eqtr3i 2767 |
. . . 4
โข (((๐ ยท ๐) + (๐พ ยท ๐พ)) โ ((๐ ยท ๐พ) + (๐ ยท ๐พ))) = ((((๐ + ๐ท) ยท ๐) + ๐) โ ((๐พ + ๐พ) ยท ๐)) |
46 | | mulsub 11605 |
. . . . . 6
โข (((๐ โ โ โง ๐พ โ โ) โง (๐ โ โ โง ๐พ โ โ)) โ ((๐ โ ๐พ) ยท (๐ โ ๐พ)) = (((๐ ยท ๐) + (๐พ ยท ๐พ)) โ ((๐ ยท ๐พ) + (๐ ยท ๐พ)))) |
47 | 21, 25, 21, 25, 46 | mp4an 692 |
. . . . 5
โข ((๐ โ ๐พ) ยท (๐ โ ๐พ)) = (((๐ ยท ๐) + (๐พ ยท ๐พ)) โ ((๐ ยท ๐พ) + (๐ ยท ๐พ))) |
48 | 2 | nn0cni 12432 |
. . . . . . . 8
โข ๐ฟ โ โ |
49 | 21, 25, 48 | subadd2i 11496 |
. . . . . . 7
โข ((๐ โ ๐พ) = ๐ฟ โ (๐ฟ + ๐พ) = ๐) |
50 | 1, 49 | mpbir 230 |
. . . . . 6
โข (๐ โ ๐พ) = ๐ฟ |
51 | 50, 50 | oveq12i 7374 |
. . . . 5
โข ((๐ โ ๐พ) ยท (๐ โ ๐พ)) = (๐ฟ ยท ๐ฟ) |
52 | 47, 51 | eqtr3i 2767 |
. . . 4
โข (((๐ ยท ๐) + (๐พ ยท ๐พ)) โ ((๐ ยท ๐พ) + (๐ ยท ๐พ))) = (๐ฟ ยท ๐ฟ) |
53 | 45, 52 | eqtr3i 2767 |
. . 3
โข ((((๐ + ๐ท) ยท ๐) + ๐) โ ((๐พ + ๐พ) ยท ๐)) = (๐ฟ ยท ๐ฟ) |
54 | 28, 32, 53 | 3eqtr2i 2771 |
. 2
โข ((((๐ + ๐ท) โ (๐พ + ๐พ)) ยท ๐) + ๐) = (๐ฟ ยท ๐ฟ) |
55 | 6, 7, 8, 17, 2, 18, 19, 20, 54 | mod2xi 16948 |
1
โข ((๐ดโ๐ธ) mod ๐) = (๐ mod ๐) |