Step | Hyp | Ref
| Expression |
1 | | mulid2 7911 |
. . 3
⊢ (𝑛 ∈ ℂ → (1
· 𝑛) = 𝑛) |
2 | 1 | adantl 275 |
. 2
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ ℂ) → (1 · 𝑛) = 𝑛) |
3 | | 1cnd 7929 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → 1 ∈
ℂ) |
4 | | prodrb.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
5 | 4 | adantr 274 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
6 | | eluzelz 9489 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
7 | 5, 6 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → 𝑁 ∈ ℤ) |
8 | | prodrbdc.dc |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴) |
9 | | exmiddc 831 |
. . . . . . . . 9
⊢
(DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴)) |
10 | 8, 9 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴)) |
11 | | iftrue 3530 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
12 | 11 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
13 | | prodmo.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
14 | 12, 13 | eqeltrd 2247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
15 | 14 | ex 114 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)) |
16 | | iffalse 3533 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
17 | | ax-1cn 7860 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
18 | 16, 17 | eqeltrdi 2261 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
19 | 18 | a1i 9 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)) |
20 | 15, 19 | jaod 712 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)) |
21 | 20 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)) |
22 | 10, 21 | mpd 13 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
23 | 22 | ralrimiva 2543 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
24 | | nfcv 2312 |
. . . . . . . . . 10
⊢
Ⅎ𝑘𝑁 |
25 | 24 | nfel1 2323 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑁 ∈ 𝐴 |
26 | | nfcsb1v 3082 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑁 / 𝑘⦌𝐵 |
27 | | nfcv 2312 |
. . . . . . . . 9
⊢
Ⅎ𝑘1 |
28 | 25, 26, 27 | nfif 3553 |
. . . . . . . 8
⊢
Ⅎ𝑘if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1) |
29 | 28 | nfel1 2323 |
. . . . . . 7
⊢
Ⅎ𝑘if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1) ∈ ℂ |
30 | | eleq1 2233 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → (𝑘 ∈ 𝐴 ↔ 𝑁 ∈ 𝐴)) |
31 | | csbeq1a 3058 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → 𝐵 = ⦋𝑁 / 𝑘⦌𝐵) |
32 | 30, 31 | ifbieq1d 3547 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1)) |
33 | 32 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ ↔ if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1) ∈ ℂ)) |
34 | 29, 33 | rspc 2828 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ → if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1) ∈ ℂ)) |
35 | 4, 23, 34 | sylc 62 |
. . . . 5
⊢ (𝜑 → if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1) ∈ ℂ) |
36 | 35 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1) ∈ ℂ) |
37 | | prodmo.1 |
. . . . 5
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) |
38 | 24, 28, 32, 37 | fvmptf 5586 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘𝑁) = if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1)) |
39 | 7, 36, 38 | syl2anc 409 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (𝐹‘𝑁) = if(𝑁 ∈ 𝐴, ⦋𝑁 / 𝑘⦌𝐵, 1)) |
40 | 39, 36 | eqeltrd 2247 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (𝐹‘𝑁) ∈ ℂ) |
41 | | elfzelz 9974 |
. . . 4
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → 𝑛 ∈ ℤ) |
42 | | elfzuz 9970 |
. . . . . 6
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
43 | 42 | adantl 275 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
44 | 23 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ∀𝑘 ∈
(ℤ≥‘𝑀)if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
45 | | nfv 1521 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑛 ∈ 𝐴 |
46 | | nfcsb1v 3082 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵 |
47 | 45, 46, 27 | nfif 3553 |
. . . . . . 7
⊢
Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) |
48 | 47 | nfel1 2323 |
. . . . . 6
⊢
Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) ∈ ℂ |
49 | | eleq1w 2231 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴)) |
50 | | csbeq1a 3058 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵) |
51 | 49, 50 | ifbieq1d 3547 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
52 | 51 | eleq1d 2239 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ ↔ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) ∈ ℂ)) |
53 | 48, 52 | rspc 2828 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) ∈ ℂ)) |
54 | 43, 44, 53 | sylc 62 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) ∈ ℂ) |
55 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑘𝑛 |
56 | 55, 47, 51, 37 | fvmptf 5586 |
. . . 4
⊢ ((𝑛 ∈ ℤ ∧ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘𝑛) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
57 | 41, 54, 56 | syl2an2 589 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑛) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
58 | | uznfz 10052 |
. . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → ¬ 𝑛 ∈ (𝑀...(𝑁 − 1))) |
59 | 58 | con2i 622 |
. . . . . 6
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → ¬ 𝑛 ∈ (ℤ≥‘𝑁)) |
60 | 59 | adantl 275 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ¬ 𝑛 ∈
(ℤ≥‘𝑁)) |
61 | | ssel 3141 |
. . . . . 6
⊢ (𝐴 ⊆
(ℤ≥‘𝑁) → (𝑛 ∈ 𝐴 → 𝑛 ∈ (ℤ≥‘𝑁))) |
62 | 61 | ad2antlr 486 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑛 ∈ 𝐴 → 𝑛 ∈ (ℤ≥‘𝑁))) |
63 | 60, 62 | mtod 658 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ¬ 𝑛 ∈ 𝐴) |
64 | 63 | iffalsed 3535 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) = 1) |
65 | 57, 64 | eqtrd 2203 |
. 2
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑛) = 1) |
66 | | eluzelz 9489 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) |
67 | | simpr 109 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
68 | 23 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ∀𝑘 ∈
(ℤ≥‘𝑀)if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
69 | 67, 68, 53 | sylc 62 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) ∈ ℂ) |
70 | 66, 69, 56 | syl2an2 589 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑛) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
71 | 70, 69 | eqeltrd 2247 |
. 2
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑛) ∈ ℂ) |
72 | | mulcl 7894 |
. . 3
⊢ ((𝑛 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑛 · 𝑧) ∈ ℂ) |
73 | 72 | adantl 275 |
. 2
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ (𝑛 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑛 · 𝑧) ∈ ℂ) |
74 | 2, 3, 5, 40, 65, 71, 73 | seq3id 10457 |
1
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾
(ℤ≥‘𝑁)) = seq𝑁( · , 𝐹)) |