Step | Hyp | Ref
| Expression |
1 | | prodeq1 14478 |
. . . 4
⊢ (𝑥 = ∅ → ∏𝑘 ∈ 𝑥 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
2 | 1 | oveq1d 6564 |
. . 3
⊢ (𝑥 = ∅ → (∏𝑘 ∈ 𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐵 mod 𝑀)) |
3 | | prodeq1 14478 |
. . . 4
⊢ (𝑥 = ∅ → ∏𝑘 ∈ 𝑥 𝐶 = ∏𝑘 ∈ ∅ 𝐶) |
4 | 3 | oveq1d 6564 |
. . 3
⊢ (𝑥 = ∅ → (∏𝑘 ∈ 𝑥 𝐶 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐶 mod 𝑀)) |
5 | 2, 4 | eqeq12d 2625 |
. 2
⊢ (𝑥 = ∅ → ((∏𝑘 ∈ 𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑥 𝐶 mod 𝑀) ↔ (∏𝑘 ∈ ∅ 𝐵 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐶 mod 𝑀))) |
6 | | prodeq1 14478 |
. . . 4
⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 𝐵 = ∏𝑘 ∈ 𝑦 𝐵) |
7 | 6 | oveq1d 6564 |
. . 3
⊢ (𝑥 = 𝑦 → (∏𝑘 ∈ 𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀)) |
8 | | prodeq1 14478 |
. . . 4
⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 𝐶 = ∏𝑘 ∈ 𝑦 𝐶) |
9 | 8 | oveq1d 6564 |
. . 3
⊢ (𝑥 = 𝑦 → (∏𝑘 ∈ 𝑥 𝐶 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) |
10 | 7, 9 | eqeq12d 2625 |
. 2
⊢ (𝑥 = 𝑦 → ((∏𝑘 ∈ 𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑥 𝐶 mod 𝑀) ↔ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀))) |
11 | | prodeq1 14478 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑖}) → ∏𝑘 ∈ 𝑥 𝐵 = ∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵) |
12 | 11 | oveq1d 6564 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑖}) → (∏𝑘 ∈ 𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀)) |
13 | | prodeq1 14478 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑖}) → ∏𝑘 ∈ 𝑥 𝐶 = ∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶) |
14 | 13 | oveq1d 6564 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑖}) → (∏𝑘 ∈ 𝑥 𝐶 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀)) |
15 | 12, 14 | eqeq12d 2625 |
. 2
⊢ (𝑥 = (𝑦 ∪ {𝑖}) → ((∏𝑘 ∈ 𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑥 𝐶 mod 𝑀) ↔ (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀))) |
16 | | prodeq1 14478 |
. . . 4
⊢ (𝑥 = 𝐴 → ∏𝑘 ∈ 𝑥 𝐵 = ∏𝑘 ∈ 𝐴 𝐵) |
17 | 16 | oveq1d 6564 |
. . 3
⊢ (𝑥 = 𝐴 → (∏𝑘 ∈ 𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝐴 𝐵 mod 𝑀)) |
18 | | prodeq1 14478 |
. . . 4
⊢ (𝑥 = 𝐴 → ∏𝑘 ∈ 𝑥 𝐶 = ∏𝑘 ∈ 𝐴 𝐶) |
19 | 18 | oveq1d 6564 |
. . 3
⊢ (𝑥 = 𝐴 → (∏𝑘 ∈ 𝑥 𝐶 mod 𝑀) = (∏𝑘 ∈ 𝐴 𝐶 mod 𝑀)) |
20 | 17, 19 | eqeq12d 2625 |
. 2
⊢ (𝑥 = 𝐴 → ((∏𝑘 ∈ 𝑥 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑥 𝐶 mod 𝑀) ↔ (∏𝑘 ∈ 𝐴 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝐴 𝐶 mod 𝑀))) |
21 | | prod0 14512 |
. . . . 5
⊢
∏𝑘 ∈
∅ 𝐵 =
1 |
22 | 21 | a1i 11 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ ∅ 𝐵 = 1) |
23 | 22 | oveq1d 6564 |
. . 3
⊢ (𝜑 → (∏𝑘 ∈ ∅ 𝐵 mod 𝑀) = (1 mod 𝑀)) |
24 | | prod0 14512 |
. . . . 5
⊢
∏𝑘 ∈
∅ 𝐶 =
1 |
25 | 24 | eqcomi 2619 |
. . . 4
⊢ 1 =
∏𝑘 ∈ ∅
𝐶 |
26 | 25 | oveq1i 6559 |
. . 3
⊢ (1 mod
𝑀) = (∏𝑘 ∈ ∅ 𝐶 mod 𝑀) |
27 | 23, 26 | syl6eq 2660 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ ∅ 𝐵 mod 𝑀) = (∏𝑘 ∈ ∅ 𝐶 mod 𝑀)) |
28 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) |
29 | | nfcsb1v 3515 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 |
30 | | fprodmodd.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ Fin) |
31 | | ssfi 8065 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴) → 𝑦 ∈ Fin) |
32 | 31 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin → (𝑦 ⊆ 𝐴 → 𝑦 ∈ Fin)) |
33 | 30, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ⊆ 𝐴 → 𝑦 ∈ Fin)) |
34 | 33 | com12 32 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝐴 → (𝜑 → 𝑦 ∈ Fin)) |
35 | 34 | adantr 480 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦)) → (𝜑 → 𝑦 ∈ Fin)) |
36 | 35 | impcom 445 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
37 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦)) → 𝑖 ∈ (𝐴 ∖ 𝑦)) |
38 | 37 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → 𝑖 ∈ (𝐴 ∖ 𝑦)) |
39 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑖 ∈ (𝐴 ∖ 𝑦) → ¬ 𝑖 ∈ 𝑦) |
40 | 39 | adantl 481 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦)) → ¬ 𝑖 ∈ 𝑦) |
41 | 40 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑖 ∈ 𝑦) |
42 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝜑) |
43 | | ssel 3562 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ 𝐴 → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
44 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
45 | 44 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
46 | 45 | imp 444 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝐴) |
47 | | fprodmodd.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) |
48 | 42, 46, 47 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℤ) |
49 | 48 | zcnd 11359 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ) |
50 | | csbeq1a 3508 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
51 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (𝐴 ∖ 𝑦) → 𝑖 ∈ 𝐴) |
52 | 51 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦)) → 𝑖 ∈ 𝐴) |
53 | 47 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) |
54 | | rspcsbela 3958 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℤ) |
55 | 52, 53, 54 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℤ) |
56 | 55 | zcnd 11359 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ) |
57 | 28, 29, 36, 38, 41, 49, 50, 56 | fprodsplitsn 14559 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 = (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑖 / 𝑘⦌𝐵)) |
58 | 57 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = ((∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑖 / 𝑘⦌𝐵) mod 𝑀)) |
59 | 58 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = ((∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑖 / 𝑘⦌𝐵) mod 𝑀)) |
60 | 36, 48 | fprodzcl 14523 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ∏𝑘 ∈ 𝑦 𝐵 ∈ ℤ) |
61 | 60 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → ∏𝑘 ∈ 𝑦 𝐵 ∈ ℤ) |
62 | | fprodmodd.c |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℤ) |
63 | 42, 46, 62 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐶 ∈ ℤ) |
64 | 36, 63 | fprodzcl 14523 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ∏𝑘 ∈ 𝑦 𝐶 ∈ ℤ) |
65 | 64 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → ∏𝑘 ∈ 𝑦 𝐶 ∈ ℤ) |
66 | 55 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℤ) |
67 | 62 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℤ) |
68 | | rspcsbela 3958 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ∈ ℤ) → ⦋𝑖 / 𝑘⦌𝐶 ∈ ℤ) |
69 | 52, 67, 68 | syl2anr 494 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑖 / 𝑘⦌𝐶 ∈ ℤ) |
70 | 69 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → ⦋𝑖 / 𝑘⦌𝐶 ∈ ℤ) |
71 | | fprodmodd.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
72 | 71 | nnrpd 11746 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
73 | 72 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → 𝑀 ∈
ℝ+) |
74 | 73 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → 𝑀 ∈
ℝ+) |
75 | | simpr 476 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) |
76 | | fprodmodd.p |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 mod 𝑀) = (𝐶 mod 𝑀)) |
77 | 76 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 (𝐵 mod 𝑀) = (𝐶 mod 𝑀)) |
78 | | rspsbca 3485 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝐵 mod 𝑀) = (𝐶 mod 𝑀)) → [𝑖 / 𝑘](𝐵 mod 𝑀) = (𝐶 mod 𝑀)) |
79 | 52, 77, 78 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → [𝑖 / 𝑘](𝐵 mod 𝑀) = (𝐶 mod 𝑀)) |
80 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑖 ∈ V |
81 | | sbceqg 3936 |
. . . . . . . . 9
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘](𝐵 mod 𝑀) = (𝐶 mod 𝑀) ↔ ⦋𝑖 / 𝑘⦌(𝐵 mod 𝑀) = ⦋𝑖 / 𝑘⦌(𝐶 mod 𝑀))) |
82 | 80, 81 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ([𝑖 / 𝑘](𝐵 mod 𝑀) = (𝐶 mod 𝑀) ↔ ⦋𝑖 / 𝑘⦌(𝐵 mod 𝑀) = ⦋𝑖 / 𝑘⦌(𝐶 mod 𝑀))) |
83 | 79, 82 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑖 / 𝑘⦌(𝐵 mod 𝑀) = ⦋𝑖 / 𝑘⦌(𝐶 mod 𝑀)) |
84 | | csbov1g 6588 |
. . . . . . . 8
⊢ (𝑖 ∈ V →
⦋𝑖 / 𝑘⦌(𝐵 mod 𝑀) = (⦋𝑖 / 𝑘⦌𝐵 mod 𝑀)) |
85 | 80, 84 | ax-mp 5 |
. . . . . . 7
⊢
⦋𝑖 /
𝑘⦌(𝐵 mod 𝑀) = (⦋𝑖 / 𝑘⦌𝐵 mod 𝑀) |
86 | | csbov1g 6588 |
. . . . . . . 8
⊢ (𝑖 ∈ V →
⦋𝑖 / 𝑘⦌(𝐶 mod 𝑀) = (⦋𝑖 / 𝑘⦌𝐶 mod 𝑀)) |
87 | 80, 86 | ax-mp 5 |
. . . . . . 7
⊢
⦋𝑖 /
𝑘⦌(𝐶 mod 𝑀) = (⦋𝑖 / 𝑘⦌𝐶 mod 𝑀) |
88 | 83, 85, 87 | 3eqtr3g 2667 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → (⦋𝑖 / 𝑘⦌𝐵 mod 𝑀) = (⦋𝑖 / 𝑘⦌𝐶 mod 𝑀)) |
89 | 88 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → (⦋𝑖 / 𝑘⦌𝐵 mod 𝑀) = (⦋𝑖 / 𝑘⦌𝐶 mod 𝑀)) |
90 | 61, 65, 66, 70, 74, 75, 89 | modmul12d 12586 |
. . . 4
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → ((∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑖 / 𝑘⦌𝐵) mod 𝑀) = ((∏𝑘 ∈ 𝑦 𝐶 · ⦋𝑖 / 𝑘⦌𝐶) mod 𝑀)) |
91 | | nfcsb1v 3515 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐶 |
92 | 63 | zcnd 11359 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐶 ∈ ℂ) |
93 | | csbeq1a 3508 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → 𝐶 = ⦋𝑖 / 𝑘⦌𝐶) |
94 | 69 | zcnd 11359 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑖 / 𝑘⦌𝐶 ∈ ℂ) |
95 | 28, 91, 36, 38, 41, 92, 93, 94 | fprodsplitsn 14559 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 = (∏𝑘 ∈ 𝑦 𝐶 · ⦋𝑖 / 𝑘⦌𝐶)) |
96 | 95 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀) = ((∏𝑘 ∈ 𝑦 𝐶 · ⦋𝑖 / 𝑘⦌𝐶) mod 𝑀)) |
97 | 96 | eqcomd 2616 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ((∏𝑘 ∈ 𝑦 𝐶 · ⦋𝑖 / 𝑘⦌𝐶) mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀)) |
98 | 97 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → ((∏𝑘 ∈ 𝑦 𝐶 · ⦋𝑖 / 𝑘⦌𝐶) mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀)) |
99 | 59, 90, 98 | 3eqtrd 2648 |
. . 3
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) ∧ (∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀)) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀)) |
100 | 99 | ex 449 |
. 2
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ (𝐴 ∖ 𝑦))) → ((∏𝑘 ∈ 𝑦 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝑦 𝐶 mod 𝑀) → (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐵 mod 𝑀) = (∏𝑘 ∈ (𝑦 ∪ {𝑖})𝐶 mod 𝑀))) |
101 | 5, 10, 15, 20, 27, 100, 30 | findcard2d 8087 |
1
⊢ (𝜑 → (∏𝑘 ∈ 𝐴 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝐴 𝐶 mod 𝑀)) |