Step | Hyp | Ref
| Expression |
1 | | nfcv 2312 |
. . . 4
⊢
Ⅎ𝑚𝐴 |
2 | | nfcsb1v 3082 |
. . . 4
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐴 |
3 | | csbeq1a 3058 |
. . . 4
⊢ (𝑘 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑘⦌𝐴) |
4 | 1, 2, 3 | cbvprodi 11523 |
. . 3
⊢
∏𝑘 ∈
{𝑀}𝐴 = ∏𝑚 ∈ {𝑀}⦋𝑚 / 𝑘⦌𝐴 |
5 | | csbeq1 3052 |
. . . 4
⊢ (𝑚 = ({〈1, 𝑀〉}‘𝑛) → ⦋𝑚 / 𝑘⦌𝐴 = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
6 | | 1nn 8889 |
. . . . 5
⊢ 1 ∈
ℕ |
7 | 6 | a1i 9 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 1 ∈
ℕ) |
8 | | 1z 9238 |
. . . . . 6
⊢ 1 ∈
ℤ |
9 | | f1osng 5483 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → {〈1,
𝑀〉}:{1}–1-1-onto→{𝑀}) |
10 | | fzsn 10022 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → (1...1) = {1}) |
11 | 8, 10 | ax-mp 5 |
. . . . . . . 8
⊢ (1...1) =
{1} |
12 | | f1oeq2 5432 |
. . . . . . . 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 133 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → {〈1,
𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
15 | 8, 14 | mpan 422 |
. . . . 5
⊢ (𝑀 ∈ 𝑉 → {〈1, 𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
16 | 15 | adantr 274 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → {〈1, 𝑀〉}:(1...1)–1-1-onto→{𝑀}) |
17 | | velsn 3600 |
. . . . . 6
⊢ (𝑚 ∈ {𝑀} ↔ 𝑚 = 𝑀) |
18 | | csbeq1 3052 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ⦋𝑚 / 𝑘⦌𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
19 | | prodsnf.1 |
. . . . . . . . . 10
⊢
Ⅎ𝑘𝐵 |
20 | 19 | a1i 9 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑘𝐵) |
21 | | prodsnf.2 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) |
22 | 20, 21 | csbiegf 3092 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑘⦌𝐴 = 𝐵) |
23 | 22 | adantr 274 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ⦋𝑀 / 𝑘⦌𝐴 = 𝐵) |
24 | 18, 23 | sylan9eqr 2225 |
. . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 = 𝑀) → ⦋𝑚 / 𝑘⦌𝐴 = 𝐵) |
25 | 17, 24 | sylan2b 285 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → ⦋𝑚 / 𝑘⦌𝐴 = 𝐵) |
26 | | simplr 525 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → 𝐵 ∈ ℂ) |
27 | 25, 26 | eqeltrd 2247 |
. . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑚 ∈ {𝑀}) → ⦋𝑚 / 𝑘⦌𝐴 ∈ ℂ) |
28 | 11 | eleq2i 2237 |
. . . . . 6
⊢ (𝑛 ∈ (1...1) ↔ 𝑛 ∈ {1}) |
29 | | velsn 3600 |
. . . . . 6
⊢ (𝑛 ∈ {1} ↔ 𝑛 = 1) |
30 | 28, 29 | bitri 183 |
. . . . 5
⊢ (𝑛 ∈ (1...1) ↔ 𝑛 = 1) |
31 | | fvsng 5692 |
. . . . . . . . . . 11
⊢ ((1
∈ ℤ ∧ 𝑀
∈ 𝑉) → ({〈1,
𝑀〉}‘1) = 𝑀) |
32 | 8, 31 | mpan 422 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝑉 → ({〈1, 𝑀〉}‘1) = 𝑀) |
33 | 32 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝑀〉}‘1) = 𝑀) |
34 | 33 | csbeq1d 3056 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) →
⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
35 | | simpr 109 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) |
36 | | fvsng 5692 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ 𝐵
∈ ℂ) → ({〈1, 𝐵〉}‘1) = 𝐵) |
37 | 8, 35, 36 | sylancr 412 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝐵〉}‘1) = 𝐵) |
38 | 23, 34, 37 | 3eqtr4rd 2214 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ({〈1, 𝐵〉}‘1) =
⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴) |
39 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑛 = 1 → ({〈1, 𝐵〉}‘𝑛) = ({〈1, 𝐵〉}‘1)) |
40 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑛 = 1 → ({〈1, 𝑀〉}‘𝑛) = ({〈1, 𝑀〉}‘1)) |
41 | 40 | csbeq1d 3056 |
. . . . . . . 8
⊢ (𝑛 = 1 →
⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴 = ⦋({〈1, 𝑀〉}‘1) / 𝑘⦌𝐴) |
42 | 39, 41 | eqeq12d 2185 |
. . . . . . 7
⊢ (𝑛 = 1 → (({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴 ↔ ({〈1, 𝐵〉}‘1) = ⦋({〈1,
𝑀〉}‘1) / 𝑘⦌𝐴)) |
43 | 38, 42 | syl5ibrcom 156 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (𝑛 = 1 → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴)) |
44 | 43 | imp 123 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑛 = 1) → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
45 | 30, 44 | sylan2b 285 |
. . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑛 ∈ (1...1)) → ({〈1, 𝐵〉}‘𝑛) = ⦋({〈1, 𝑀〉}‘𝑛) / 𝑘⦌𝐴) |
46 | 5, 7, 16, 27, 45 | fprodseq 11546 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑚 ∈ {𝑀}⦋𝑚 / 𝑘⦌𝐴 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1)))‘1)) |
47 | 4, 46 | eqtrid 2215 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1)))‘1)) |
48 | | 1zzd 9239 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → 1 ∈
ℤ) |
49 | | eqid 2170 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1)) |
50 | | breq1 3992 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → (𝑛 ≤ 1 ↔ 𝑗 ≤ 1)) |
51 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → ({〈1, 𝐵〉}‘𝑛) = ({〈1, 𝐵〉}‘𝑗)) |
52 | 50, 51 | ifbieq1d 3548 |
. . . . . 6
⊢ (𝑛 = 𝑗 → if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1) = if(𝑗 ≤ 1, ({〈1, 𝐵〉}‘𝑗), 1)) |
53 | | elnnuz 9523 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ ↔ 𝑗 ∈
(ℤ≥‘1)) |
54 | 53 | biimpri 132 |
. . . . . . 7
⊢ (𝑗 ∈
(ℤ≥‘1) → 𝑗 ∈ ℕ) |
55 | 54 | adantl 275 |
. . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
→ 𝑗 ∈
ℕ) |
56 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
𝑗 ≤ 1) |
57 | | eluzle 9499 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘1) → 1 ≤ 𝑗) |
58 | 57 | ad2antlr 486 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) → 1
≤ 𝑗) |
59 | 54 | nnzd 9333 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘1) → 𝑗 ∈ ℤ) |
60 | 59 | ad2antlr 486 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
𝑗 ∈
ℤ) |
61 | 60 | zred 9334 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
𝑗 ∈
ℝ) |
62 | | 1red 7935 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) → 1
∈ ℝ) |
63 | 61, 62 | letri3d 8035 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
(𝑗 = 1 ↔ (𝑗 ≤ 1 ∧ 1 ≤ 𝑗))) |
64 | 56, 58, 63 | mpbir2and 939 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
𝑗 = 1) |
65 | 64 | fveq2d 5500 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
({〈1, 𝐵〉}‘𝑗) = ({〈1, 𝐵〉}‘1)) |
66 | 37 | ad2antrr 485 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
({〈1, 𝐵〉}‘1) = 𝐵) |
67 | 65, 66 | eqtrd 2203 |
. . . . . . . 8
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
({〈1, 𝐵〉}‘𝑗) = 𝐵) |
68 | 35 | ad2antrr 485 |
. . . . . . . 8
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
𝐵 ∈
ℂ) |
69 | 67, 68 | eqeltrd 2247 |
. . . . . . 7
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ 𝑗 ≤ 1) →
({〈1, 𝐵〉}‘𝑗) ∈ ℂ) |
70 | | 1cnd 7936 |
. . . . . . 7
⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
∧ ¬ 𝑗 ≤ 1)
→ 1 ∈ ℂ) |
71 | 55 | nnzd 9333 |
. . . . . . . 8
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
→ 𝑗 ∈
ℤ) |
72 | | 1zzd 9239 |
. . . . . . . 8
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
→ 1 ∈ ℤ) |
73 | | zdcle 9288 |
. . . . . . . 8
⊢ ((𝑗 ∈ ℤ ∧ 1 ∈
ℤ) → DECID 𝑗 ≤ 1) |
74 | 71, 72, 73 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
→ DECID 𝑗 ≤ 1) |
75 | 69, 70, 74 | ifcldadc 3555 |
. . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
→ if(𝑗 ≤ 1,
({〈1, 𝐵〉}‘𝑗), 1) ∈ ℂ) |
76 | 49, 52, 55, 75 | fvmptd3 5589 |
. . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
→ ((𝑛 ∈ ℕ
↦ if(𝑛 ≤ 1,
({〈1, 𝐵〉}‘𝑛), 1))‘𝑗) = if(𝑗 ≤ 1, ({〈1, 𝐵〉}‘𝑗), 1)) |
77 | 76, 75 | eqeltrd 2247 |
. . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ (ℤ≥‘1))
→ ((𝑛 ∈ ℕ
↦ if(𝑛 ≤ 1,
({〈1, 𝐵〉}‘𝑛), 1))‘𝑗) ∈ ℂ) |
78 | | mulcl 7901 |
. . . . 5
⊢ ((𝑗 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (𝑗 · 𝑞) ∈ ℂ) |
79 | 78 | adantl 275 |
. . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) ∧ (𝑗 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑗 · 𝑞) ∈ ℂ) |
80 | 48, 77, 79 | seq3-1 10416 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ≤ 1, ({〈1,
𝐵〉}‘𝑛), 1)))‘1) = ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1))‘1)) |
81 | | breq1 3992 |
. . . . . 6
⊢ (𝑛 = 1 → (𝑛 ≤ 1 ↔ 1 ≤ 1)) |
82 | 81, 39 | ifbieq1d 3548 |
. . . . 5
⊢ (𝑛 = 1 → if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1) = if(1 ≤ 1, ({〈1, 𝐵〉}‘1),
1)) |
83 | | 1le1 8491 |
. . . . . . . 8
⊢ 1 ≤
1 |
84 | 83 | iftruei 3532 |
. . . . . . 7
⊢ if(1 ≤
1, ({〈1, 𝐵〉}‘1), 1) = ({〈1, 𝐵〉}‘1) |
85 | 84, 37 | eqtrid 2215 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → if(1 ≤ 1,
({〈1, 𝐵〉}‘1), 1) = 𝐵) |
86 | 85, 35 | eqeltrd 2247 |
. . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → if(1 ≤ 1,
({〈1, 𝐵〉}‘1), 1) ∈
ℂ) |
87 | 49, 82, 7, 86 | fvmptd3 5589 |
. . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1))‘1) = if(1 ≤ 1, ({〈1,
𝐵〉}‘1),
1)) |
88 | 87, 85 | eqtrd 2203 |
. . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 1, ({〈1, 𝐵〉}‘𝑛), 1))‘1) = 𝐵) |
89 | 80, 88 | eqtrd 2203 |
. 2
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ≤ 1, ({〈1,
𝐵〉}‘𝑛), 1)))‘1) = 𝐵) |
90 | 47, 89 | eqtrd 2203 |
1
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = 𝐵) |