Step | Hyp | Ref
| Expression |
1 | | nfcv 2907 |
. . . 4
⊢
Ⅎ𝑚𝐴 |
2 | | nfcsb1v 3858 |
. . . 4
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐴 |
3 | | csbeq1a 3847 |
. . . 4
⊢ (𝑘 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑘⦌𝐴) |
4 | 1, 2, 3 | cbvprodi 15625 |
. . 3
⊢
∏𝑘 ∈
{𝑀}𝐴 = ∏𝑚 ∈ {𝑀}⦋𝑚 / 𝑘⦌𝐴 |
5 | | csbeq1 3836 |
. . . 4
⊢ (𝑚 = ({〈1, 𝑀〉}‘𝑛) → ⦋𝑚 / 𝑘⦌𝐴 = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
6 | | 1nn 11982 |
. . . . 5
⊢ 1 ∈
ℕ |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 1 ∈
ℕ) |
8 | | 1z 12348 |
. . . . . 6
⊢ 1 ∈
ℤ |
9 | | f1osng 6759 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → {〈1,
𝑀〉}:{1}–1-1-onto→{𝑀}) |
10 | | fzsn 13296 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → (1...1) = {1}) |
11 | 8, 10 | ax-mp 5 |
. . . . . . . 8
⊢ (1...1) =
{1} |
12 | | f1oeq2 6707 |
. . . . . . . 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 233 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → {〈1,
𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
15 | 8, 14 | mpan 687 |
. . . . 5
⊢ (𝑀 ∈ 𝑉 → {〈1, 𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
16 | 15 | adantr 481 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → {〈1, 𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
17 | | velsn 4579 |
. . . . . 6
⊢ (𝑚 ∈ {𝑀} ↔ 𝑚 = 𝑀) |
18 | | csbeq1 3836 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ⦋𝑚 / 𝑘⦌𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
19 | | nfcvd 2908 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑘𝐵) |
20 | | prodsn.1 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) |
21 | 19, 20 | csbiegf 3867 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑘⦌𝐴 = 𝐵) |
22 | 21 | adantr 481 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ⦋𝑀 / 𝑘⦌𝐴 = 𝐵) |
23 | 18, 22 | sylan9eqr 2800 |
. . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 = 𝑀) → ⦋𝑚 / 𝑘⦌𝐴 = 𝐵) |
24 | 17, 23 | sylan2b 594 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → ⦋𝑚 / 𝑘⦌𝐴 = 𝐵) |
25 | | simplr 766 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → 𝐵 ∈ ℂ) |
26 | 24, 25 | eqeltrd 2839 |
. . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → ⦋𝑚 / 𝑘⦌𝐴 ∈ ℂ) |
27 | 11 | eleq2i 2830 |
. . . . . 6
⊢ (𝑛 ∈ (1...1) ↔ 𝑛 ∈ {1}) |
28 | | velsn 4579 |
. . . . . 6
⊢ (𝑛 ∈ {1} ↔ 𝑛 = 1) |
29 | 27, 28 | bitri 274 |
. . . . 5
⊢ (𝑛 ∈ (1...1) ↔ 𝑛 = 1) |
30 | | fvsng 7054 |
. . . . . . . . . . 11
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → ({〈1,
𝑀〉}‘1) = 𝑀) |
31 | 8, 30 | mpan 687 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝑉 → ({〈1, 𝑀〉}‘1) = 𝑀) |
32 | 31 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝑀〉}‘1) = 𝑀) |
33 | 32 | csbeq1d 3837 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) →
⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
34 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) |
35 | | fvsng 7054 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ 𝐵
∈ ℂ) → ({〈1, 𝐵〉}‘1) = 𝐵) |
36 | 8, 34, 35 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝐵〉}‘1) = 𝐵) |
37 | 22, 33, 36 | 3eqtr4rd 2789 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝐵〉}‘1) =
⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴) |
38 | | fveq2 6776 |
. . . . . . . 8
⊢ (𝑛 = 1 → ({〈1, 𝐵〉}‘𝑛) = ({〈1, 𝐵〉}‘1)) |
39 | | fveq2 6776 |
. . . . . . . . 9
⊢ (𝑛 = 1 → ({〈1, 𝑀〉}‘𝑛) = ({〈1, 𝑀〉}‘1)) |
40 | 39 | csbeq1d 3837 |
. . . . . . . 8
⊢ (𝑛 = 1 →
⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴 = ⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴) |
41 | 38, 40 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑛 = 1 → (({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴 ↔ ({〈1, 𝐵〉}‘1) = ⦋({〈1,
𝑀〉}‘1) / 𝑘⦌𝐴)) |
42 | 37, 41 | syl5ibrcom 246 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (𝑛 = 1 → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴)) |
43 | 42 | imp 407 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑛 = 1) → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
44 | 29, 43 | sylan2b 594 |
. . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (1...1)) → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
45 | 5, 7, 16, 26, 44 | fprod 15649 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑚 ∈ {𝑀}⦋𝑚 / 𝑘⦌𝐴 = (seq1( · , {〈1, 𝐵〉})‘1)) |
46 | 4, 45 | eqtrid 2790 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = (seq1( · , {〈1, 𝐵〉})‘1)) |
47 | 8, 36 | seq1i 13733 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (seq1( · ,
{〈1, 𝐵〉})‘1) = 𝐵) |
48 | 46, 47 | eqtrd 2778 |
1
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = 𝐵) |