Step | Hyp | Ref
| Expression |
1 | | prodeq1 15797 |
. . . 4
โข (๐ฅ = โ
โ โ๐ โ ๐ฅ ๐ต = โ๐ โ โ
๐ต) |
2 | 1 | oveq1d 7373 |
. . 3
โข (๐ฅ = โ
โ (โ๐ โ ๐ฅ ๐ต mod ๐) = (โ๐ โ โ
๐ต mod ๐)) |
3 | | prodeq1 15797 |
. . . 4
โข (๐ฅ = โ
โ โ๐ โ ๐ฅ ๐ถ = โ๐ โ โ
๐ถ) |
4 | 3 | oveq1d 7373 |
. . 3
โข (๐ฅ = โ
โ (โ๐ โ ๐ฅ ๐ถ mod ๐) = (โ๐ โ โ
๐ถ mod ๐)) |
5 | 2, 4 | eqeq12d 2749 |
. 2
โข (๐ฅ = โ
โ ((โ๐ โ ๐ฅ ๐ต mod ๐) = (โ๐ โ ๐ฅ ๐ถ mod ๐) โ (โ๐ โ โ
๐ต mod ๐) = (โ๐ โ โ
๐ถ mod ๐))) |
6 | | prodeq1 15797 |
. . . 4
โข (๐ฅ = ๐ฆ โ โ๐ โ ๐ฅ ๐ต = โ๐ โ ๐ฆ ๐ต) |
7 | 6 | oveq1d 7373 |
. . 3
โข (๐ฅ = ๐ฆ โ (โ๐ โ ๐ฅ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ต mod ๐)) |
8 | | prodeq1 15797 |
. . . 4
โข (๐ฅ = ๐ฆ โ โ๐ โ ๐ฅ ๐ถ = โ๐ โ ๐ฆ ๐ถ) |
9 | 8 | oveq1d 7373 |
. . 3
โข (๐ฅ = ๐ฆ โ (โ๐ โ ๐ฅ ๐ถ mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) |
10 | 7, 9 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ฆ โ ((โ๐ โ ๐ฅ ๐ต mod ๐) = (โ๐ โ ๐ฅ ๐ถ mod ๐) โ (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐))) |
11 | | prodeq1 15797 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐}) โ โ๐ โ ๐ฅ ๐ต = โ๐ โ (๐ฆ โช {๐})๐ต) |
12 | 11 | oveq1d 7373 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐}) โ (โ๐ โ ๐ฅ ๐ต mod ๐) = (โ๐ โ (๐ฆ โช {๐})๐ต mod ๐)) |
13 | | prodeq1 15797 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐}) โ โ๐ โ ๐ฅ ๐ถ = โ๐ โ (๐ฆ โช {๐})๐ถ) |
14 | 13 | oveq1d 7373 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐}) โ (โ๐ โ ๐ฅ ๐ถ mod ๐) = (โ๐ โ (๐ฆ โช {๐})๐ถ mod ๐)) |
15 | 12, 14 | eqeq12d 2749 |
. 2
โข (๐ฅ = (๐ฆ โช {๐}) โ ((โ๐ โ ๐ฅ ๐ต mod ๐) = (โ๐ โ ๐ฅ ๐ถ mod ๐) โ (โ๐ โ (๐ฆ โช {๐})๐ต mod ๐) = (โ๐ โ (๐ฆ โช {๐})๐ถ mod ๐))) |
16 | | prodeq1 15797 |
. . . 4
โข (๐ฅ = ๐ด โ โ๐ โ ๐ฅ ๐ต = โ๐ โ ๐ด ๐ต) |
17 | 16 | oveq1d 7373 |
. . 3
โข (๐ฅ = ๐ด โ (โ๐ โ ๐ฅ ๐ต mod ๐) = (โ๐ โ ๐ด ๐ต mod ๐)) |
18 | | prodeq1 15797 |
. . . 4
โข (๐ฅ = ๐ด โ โ๐ โ ๐ฅ ๐ถ = โ๐ โ ๐ด ๐ถ) |
19 | 18 | oveq1d 7373 |
. . 3
โข (๐ฅ = ๐ด โ (โ๐ โ ๐ฅ ๐ถ mod ๐) = (โ๐ โ ๐ด ๐ถ mod ๐)) |
20 | 17, 19 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ด โ ((โ๐ โ ๐ฅ ๐ต mod ๐) = (โ๐ โ ๐ฅ ๐ถ mod ๐) โ (โ๐ โ ๐ด ๐ต mod ๐) = (โ๐ โ ๐ด ๐ถ mod ๐))) |
21 | | prod0 15831 |
. . . . 5
โข
โ๐ โ
โ
๐ต =
1 |
22 | 21 | a1i 11 |
. . . 4
โข (๐ โ โ๐ โ โ
๐ต = 1) |
23 | 22 | oveq1d 7373 |
. . 3
โข (๐ โ (โ๐ โ โ
๐ต mod ๐) = (1 mod ๐)) |
24 | | prod0 15831 |
. . . . 5
โข
โ๐ โ
โ
๐ถ =
1 |
25 | 24 | eqcomi 2742 |
. . . 4
โข 1 =
โ๐ โ โ
๐ถ |
26 | 25 | oveq1i 7368 |
. . 3
โข (1 mod
๐) = (โ๐ โ โ
๐ถ mod ๐) |
27 | 23, 26 | eqtrdi 2789 |
. 2
โข (๐ โ (โ๐ โ โ
๐ต mod ๐) = (โ๐ โ โ
๐ถ mod ๐)) |
28 | | nfv 1918 |
. . . . . . 7
โข
โฒ๐(๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) |
29 | | nfcsb1v 3881 |
. . . . . . 7
โข
โฒ๐โฆ๐ / ๐โฆ๐ต |
30 | | ssfi 9120 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง ๐ฆ โ ๐ด) โ ๐ฆ โ Fin) |
31 | 30 | ex 414 |
. . . . . . . . . 10
โข (๐ด โ Fin โ (๐ฆ โ ๐ด โ ๐ฆ โ Fin)) |
32 | | fprodmodd.a |
. . . . . . . . . 10
โข (๐ โ ๐ด โ Fin) |
33 | 31, 32 | syl11 33 |
. . . . . . . . 9
โข (๐ฆ โ ๐ด โ (๐ โ ๐ฆ โ Fin)) |
34 | 33 | adantr 482 |
. . . . . . . 8
โข ((๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ)) โ (๐ โ ๐ฆ โ Fin)) |
35 | 34 | impcom 409 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ ๐ฆ โ Fin) |
36 | | simpr 486 |
. . . . . . . 8
โข ((๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ)) โ ๐ โ (๐ด โ ๐ฆ)) |
37 | 36 | adantl 483 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ ๐ โ (๐ด โ ๐ฆ)) |
38 | | eldifn 4088 |
. . . . . . . . 9
โข (๐ โ (๐ด โ ๐ฆ) โ ยฌ ๐ โ ๐ฆ) |
39 | 38 | adantl 483 |
. . . . . . . 8
โข ((๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ)) โ ยฌ ๐ โ ๐ฆ) |
40 | 39 | adantl 483 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ ยฌ ๐ โ ๐ฆ) |
41 | | simpll 766 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐) |
42 | | ssel 3938 |
. . . . . . . . . . . 12
โข (๐ฆ โ ๐ด โ (๐ โ ๐ฆ โ ๐ โ ๐ด)) |
43 | 42 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ)) โ (๐ โ ๐ฆ โ ๐ โ ๐ด)) |
44 | 43 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ (๐ โ ๐ฆ โ ๐ โ ๐ด)) |
45 | 44 | imp 408 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ โ ๐ด) |
46 | | fprodmodd.b |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โค) |
47 | 41, 45, 46 | syl2anc 585 |
. . . . . . . 8
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โค) |
48 | 47 | zcnd 12613 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
49 | | csbeq1a 3870 |
. . . . . . 7
โข (๐ = ๐ โ ๐ต = โฆ๐ / ๐โฆ๐ต) |
50 | | eldifi 4087 |
. . . . . . . . . 10
โข (๐ โ (๐ด โ ๐ฆ) โ ๐ โ ๐ด) |
51 | 50 | adantl 483 |
. . . . . . . . 9
โข ((๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ)) โ ๐ โ ๐ด) |
52 | 46 | ralrimiva 3140 |
. . . . . . . . 9
โข (๐ โ โ๐ โ ๐ด ๐ต โ โค) |
53 | | rspcsbela 4396 |
. . . . . . . . 9
โข ((๐ โ ๐ด โง โ๐ โ ๐ด ๐ต โ โค) โ โฆ๐ / ๐โฆ๐ต โ โค) |
54 | 51, 52, 53 | syl2anr 598 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โฆ๐ / ๐โฆ๐ต โ โค) |
55 | 54 | zcnd 12613 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โฆ๐ / ๐โฆ๐ต โ โ) |
56 | 28, 29, 35, 37, 40, 48, 49, 55 | fprodsplitsn 15877 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ / ๐โฆ๐ต)) |
57 | 56 | oveq1d 7373 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ (โ๐ โ (๐ฆ โช {๐})๐ต mod ๐) = ((โ๐ โ ๐ฆ ๐ต ยท โฆ๐ / ๐โฆ๐ต) mod ๐)) |
58 | 57 | adantr 482 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ (โ๐ โ (๐ฆ โช {๐})๐ต mod ๐) = ((โ๐ โ ๐ฆ ๐ต ยท โฆ๐ / ๐โฆ๐ต) mod ๐)) |
59 | 35, 47 | fprodzcl 15842 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ต โ โค) |
60 | 59 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ โ๐ โ ๐ฆ ๐ต โ โค) |
61 | | fprodmodd.c |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โค) |
62 | 41, 45, 61 | syl2anc 585 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ถ โ โค) |
63 | 35, 62 | fprodzcl 15842 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ถ โ โค) |
64 | 63 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ โ๐ โ ๐ฆ ๐ถ โ โค) |
65 | 54 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ โฆ๐ / ๐โฆ๐ต โ โค) |
66 | 61 | ralrimiva 3140 |
. . . . . . 7
โข (๐ โ โ๐ โ ๐ด ๐ถ โ โค) |
67 | | rspcsbela 4396 |
. . . . . . 7
โข ((๐ โ ๐ด โง โ๐ โ ๐ด ๐ถ โ โค) โ โฆ๐ / ๐โฆ๐ถ โ โค) |
68 | 51, 66, 67 | syl2anr 598 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โฆ๐ / ๐โฆ๐ถ โ โค) |
69 | 68 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ โฆ๐ / ๐โฆ๐ถ โ โค) |
70 | | fprodmodd.m |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
71 | 70 | nnrpd 12960 |
. . . . . . 7
โข (๐ โ ๐ โ
โ+) |
72 | 71 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ ๐ โ
โ+) |
73 | 72 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ ๐ โ
โ+) |
74 | | simpr 486 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) |
75 | | fprodmodd.p |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (๐ต mod ๐) = (๐ถ mod ๐)) |
76 | 75 | ralrimiva 3140 |
. . . . . . . . 9
โข (๐ โ โ๐ โ ๐ด (๐ต mod ๐) = (๐ถ mod ๐)) |
77 | | rspsbca 3837 |
. . . . . . . . 9
โข ((๐ โ ๐ด โง โ๐ โ ๐ด (๐ต mod ๐) = (๐ถ mod ๐)) โ [๐ / ๐](๐ต mod ๐) = (๐ถ mod ๐)) |
78 | 51, 76, 77 | syl2anr 598 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ [๐ / ๐](๐ต mod ๐) = (๐ถ mod ๐)) |
79 | | vex 3448 |
. . . . . . . . 9
โข ๐ โ V |
80 | | sbceqg 4370 |
. . . . . . . . 9
โข (๐ โ V โ ([๐ / ๐](๐ต mod ๐) = (๐ถ mod ๐) โ โฆ๐ / ๐โฆ(๐ต mod ๐) = โฆ๐ / ๐โฆ(๐ถ mod ๐))) |
81 | 79, 80 | mp1i 13 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ ([๐ / ๐](๐ต mod ๐) = (๐ถ mod ๐) โ โฆ๐ / ๐โฆ(๐ต mod ๐) = โฆ๐ / ๐โฆ(๐ถ mod ๐))) |
82 | 78, 81 | mpbid 231 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โฆ๐ / ๐โฆ(๐ต mod ๐) = โฆ๐ / ๐โฆ(๐ถ mod ๐)) |
83 | | csbov1g 7403 |
. . . . . . . 8
โข (๐ โ V โ
โฆ๐ / ๐โฆ(๐ต mod ๐) = (โฆ๐ / ๐โฆ๐ต mod ๐)) |
84 | 83 | elv 3450 |
. . . . . . 7
โข
โฆ๐ /
๐โฆ(๐ต mod ๐) = (โฆ๐ / ๐โฆ๐ต mod ๐) |
85 | | csbov1g 7403 |
. . . . . . . 8
โข (๐ โ V โ
โฆ๐ / ๐โฆ(๐ถ mod ๐) = (โฆ๐ / ๐โฆ๐ถ mod ๐)) |
86 | 85 | elv 3450 |
. . . . . . 7
โข
โฆ๐ /
๐โฆ(๐ถ mod ๐) = (โฆ๐ / ๐โฆ๐ถ mod ๐) |
87 | 82, 84, 86 | 3eqtr3g 2796 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ (โฆ๐ / ๐โฆ๐ต mod ๐) = (โฆ๐ / ๐โฆ๐ถ mod ๐)) |
88 | 87 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ (โฆ๐ / ๐โฆ๐ต mod ๐) = (โฆ๐ / ๐โฆ๐ถ mod ๐)) |
89 | 60, 64, 65, 69, 73, 74, 88 | modmul12d 13836 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ ((โ๐ โ ๐ฆ ๐ต ยท โฆ๐ / ๐โฆ๐ต) mod ๐) = ((โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ / ๐โฆ๐ถ) mod ๐)) |
90 | | nfcsb1v 3881 |
. . . . . . . 8
โข
โฒ๐โฆ๐ / ๐โฆ๐ถ |
91 | 62 | zcnd 12613 |
. . . . . . . 8
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ถ โ โ) |
92 | | csbeq1a 3870 |
. . . . . . . 8
โข (๐ = ๐ โ ๐ถ = โฆ๐ / ๐โฆ๐ถ) |
93 | 68 | zcnd 12613 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โฆ๐ / ๐โฆ๐ถ โ โ) |
94 | 28, 90, 35, 37, 40, 91, 92, 93 | fprodsplitsn 15877 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐})๐ถ = (โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ / ๐โฆ๐ถ)) |
95 | 94 | oveq1d 7373 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ (โ๐ โ (๐ฆ โช {๐})๐ถ mod ๐) = ((โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ / ๐โฆ๐ถ) mod ๐)) |
96 | 95 | eqcomd 2739 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ ((โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ / ๐โฆ๐ถ) mod ๐) = (โ๐ โ (๐ฆ โช {๐})๐ถ mod ๐)) |
97 | 96 | adantr 482 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ ((โ๐ โ ๐ฆ ๐ถ ยท โฆ๐ / ๐โฆ๐ถ) mod ๐) = (โ๐ โ (๐ฆ โช {๐})๐ถ mod ๐)) |
98 | 58, 89, 97 | 3eqtrd 2777 |
. . 3
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โง (โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐)) โ (โ๐ โ (๐ฆ โช {๐})๐ต mod ๐) = (โ๐ โ (๐ฆ โช {๐})๐ถ mod ๐)) |
99 | 98 | ex 414 |
. 2
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ โ (๐ด โ ๐ฆ))) โ ((โ๐ โ ๐ฆ ๐ต mod ๐) = (โ๐ โ ๐ฆ ๐ถ mod ๐) โ (โ๐ โ (๐ฆ โช {๐})๐ต mod ๐) = (โ๐ โ (๐ฆ โช {๐})๐ถ mod ๐))) |
100 | 5, 10, 15, 20, 27, 99, 32 | findcard2d 9113 |
1
โข (๐ โ (โ๐ โ ๐ด ๐ต mod ๐) = (โ๐ โ ๐ด ๐ถ mod ๐)) |