Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑚𝐴 |
2 | | nfcsb1v 3836 |
. . . 4
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐴 |
3 | | csbeq1a 3825 |
. . . 4
⊢ (𝑘 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑘⦌𝐴) |
4 | 1, 2, 3 | cbvprodi 15479 |
. . 3
⊢
∏𝑘 ∈
{𝑀}𝐴 = ∏𝑚 ∈ {𝑀}⦋𝑚 / 𝑘⦌𝐴 |
5 | | csbeq1 3814 |
. . . 4
⊢ (𝑚 = ({〈1, 𝑀〉}‘𝑛) → ⦋𝑚 / 𝑘⦌𝐴 = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
6 | | 1nn 11841 |
. . . . 5
⊢ 1 ∈
ℕ |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 1 ∈
ℕ) |
8 | | 1z 12207 |
. . . . . 6
⊢ 1 ∈
ℤ |
9 | | f1osng 6701 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → {〈1,
𝑀〉}:{1}–1-1-onto→{𝑀}) |
10 | | fzsn 13154 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → (1...1) = {1}) |
11 | 8, 10 | ax-mp 5 |
. . . . . . . 8
⊢ (1...1) =
{1} |
12 | | f1oeq2 6650 |
. . . . . . . 8
⊢ ((1...1)
= {1} → ({〈1, 𝑀〉}:(1...1)–1-1-onto→{𝑀} ↔ {〈1, 𝑀〉}:{1}–1-1-onto→{𝑀})) |
13 | 11, 12 | ax-mp 5 |
. . . . . . 7
⊢
({〈1, 𝑀〉}:(1...1)–1-1-onto→{𝑀} ↔ {〈1, 𝑀〉}:{1}–1-1-onto→{𝑀}) |
14 | 9, 13 | sylibr 237 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → {〈1,
𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
15 | 8, 14 | mpan 690 |
. . . . 5
⊢ (𝑀 ∈ 𝑉 → {〈1, 𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
16 | 15 | adantr 484 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → {〈1, 𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
17 | | velsn 4557 |
. . . . . 6
⊢ (𝑚 ∈ {𝑀} ↔ 𝑚 = 𝑀) |
18 | | csbeq1 3814 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ⦋𝑚 / 𝑘⦌𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
19 | | prodsnf.1 |
. . . . . . . . . 10
⊢
Ⅎ𝑘𝐵 |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑘𝐵) |
21 | | prodsnf.2 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) |
22 | 20, 21 | csbiegf 3845 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑘⦌𝐴 = 𝐵) |
23 | 22 | adantr 484 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ⦋𝑀 / 𝑘⦌𝐴 = 𝐵) |
24 | 18, 23 | sylan9eqr 2800 |
. . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 = 𝑀) → ⦋𝑚 / 𝑘⦌𝐴 = 𝐵) |
25 | 17, 24 | sylan2b 597 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → ⦋𝑚 / 𝑘⦌𝐴 = 𝐵) |
26 | | simplr 769 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → 𝐵 ∈ ℂ) |
27 | 25, 26 | eqeltrd 2838 |
. . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → ⦋𝑚 / 𝑘⦌𝐴 ∈ ℂ) |
28 | 11 | eleq2i 2829 |
. . . . . 6
⊢ (𝑛 ∈ (1...1) ↔ 𝑛 ∈ {1}) |
29 | | velsn 4557 |
. . . . . 6
⊢ (𝑛 ∈ {1} ↔ 𝑛 = 1) |
30 | 28, 29 | bitri 278 |
. . . . 5
⊢ (𝑛 ∈ (1...1) ↔ 𝑛 = 1) |
31 | | fvsng 6995 |
. . . . . . . . . . 11
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → ({〈1,
𝑀〉}‘1) = 𝑀) |
32 | 8, 31 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝑉 → ({〈1, 𝑀〉}‘1) = 𝑀) |
33 | 32 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝑀〉}‘1) = 𝑀) |
34 | 33 | csbeq1d 3815 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) →
⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
35 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) |
36 | | fvsng 6995 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ 𝐵
∈ ℂ) → ({〈1, 𝐵〉}‘1) = 𝐵) |
37 | 8, 35, 36 | sylancr 590 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝐵〉}‘1) = 𝐵) |
38 | 23, 34, 37 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝐵〉}‘1) =
⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴) |
39 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑛 = 1 → ({〈1, 𝐵〉}‘𝑛) = ({〈1, 𝐵〉}‘1)) |
40 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑛 = 1 → ({〈1, 𝑀〉}‘𝑛) = ({〈1, 𝑀〉}‘1)) |
41 | 40 | csbeq1d 3815 |
. . . . . . . 8
⊢ (𝑛 = 1 →
⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴 = ⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴) |
42 | 39, 41 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑛 = 1 → (({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴 ↔ ({〈1, 𝐵〉}‘1) = ⦋({〈1,
𝑀〉}‘1) / 𝑘⦌𝐴)) |
43 | 38, 42 | syl5ibrcom 250 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (𝑛 = 1 → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴)) |
44 | 43 | imp 410 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑛 = 1) → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
45 | 30, 44 | sylan2b 597 |
. . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (1...1)) → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
46 | 5, 7, 16, 27, 45 | fprod 15503 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑚 ∈ {𝑀}⦋𝑚 / 𝑘⦌𝐴 = (seq1( · , {〈1, 𝐵〉})‘1)) |
47 | 4, 46 | syl5eq 2790 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = (seq1( · , {〈1, 𝐵〉})‘1)) |
48 | 8, 37 | seq1i 13588 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (seq1( · ,
{〈1, 𝐵〉})‘1) = 𝐵) |
49 | 47, 48 | eqtrd 2777 |
1
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = 𝐵) |