Step | Hyp | Ref
| Expression |
1 | | mulid2 9917 |
. . 3
⊢ (𝑛 ∈ ℂ → (1
· 𝑛) = 𝑛) |
2 | 1 | adantl 481 |
. 2
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ ℂ) → (1 · 𝑛) = 𝑛) |
3 | | 1cnd 9935 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → 1 ∈
ℂ) |
4 | | prodrb.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
5 | 4 | adantr 480 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
6 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
7 | 6 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
8 | | prodmo.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
9 | 8 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
10 | 7, 9 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
11 | 10 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)) |
12 | | iffalse 4045 |
. . . . . . 7
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
13 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
14 | 12, 13 | syl6eqel 2696 |
. . . . . 6
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
15 | 11, 14 | pm2.61d1 170 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
16 | | prodmo.1 |
. . . . 5
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) |
17 | 15, 16 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐹:ℤ⟶ℂ) |
18 | | uzssz 11583 |
. . . . 5
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
19 | 18, 4 | sseldi 3566 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
20 | 17, 19 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℂ) |
21 | 20 | adantr 480 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (𝐹‘𝑁) ∈ ℂ) |
22 | | elfzelz 12213 |
. . . . 5
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → 𝑛 ∈ ℤ) |
23 | 22 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝑛 ∈ ℤ) |
24 | | simplr 788 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ⊆ (ℤ≥‘𝑁)) |
25 | 19 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
26 | 25 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → 𝑁 ∈ ℂ) |
27 | 26 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝑁 ∈ ℂ) |
28 | | 1cnd 9935 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 1 ∈
ℂ) |
29 | 27, 28 | npcand 10275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
30 | 29 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) →
(ℤ≥‘((𝑁 − 1) + 1)) =
(ℤ≥‘𝑁)) |
31 | 24, 30 | sseqtr4d 3605 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ⊆
(ℤ≥‘((𝑁 − 1) + 1))) |
32 | | fznuz 12291 |
. . . . . 6
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → ¬ 𝑛 ∈ (ℤ≥‘((𝑁 − 1) +
1))) |
33 | 32 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ¬ 𝑛 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
34 | 31, 33 | ssneldd 3571 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ¬ 𝑛 ∈ 𝐴) |
35 | 23, 34 | eldifd 3551 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝑛 ∈ (ℤ ∖ 𝐴)) |
36 | | fveq2 6103 |
. . . . 5
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
37 | 36 | eqeq1d 2612 |
. . . 4
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) = 1 ↔ (𝐹‘𝑛) = 1)) |
38 | | eldifi 3694 |
. . . . . 6
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → 𝑘 ∈ ℤ) |
39 | | eldifn 3695 |
. . . . . . . 8
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
40 | 39, 12 | syl 17 |
. . . . . . 7
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
41 | 40, 13 | syl6eqel 2696 |
. . . . . 6
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
42 | 16 | fvmpt2 6200 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
43 | 38, 41, 42 | syl2anc 691 |
. . . . 5
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
44 | 43, 40 | eqtrd 2644 |
. . . 4
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑘) = 1) |
45 | 37, 44 | vtoclga 3245 |
. . 3
⊢ (𝑛 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑛) = 1) |
46 | 35, 45 | syl 17 |
. 2
⊢ (((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑛) = 1) |
47 | 2, 3, 5, 21, 46 | seqid 12708 |
1
⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾
(ℤ≥‘𝑁)) = seq𝑁( · , 𝐹)) |