Step | Hyp | Ref
| Expression |
1 | | eqid 2157 |
. 2
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
2 | | prodrb.3 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
3 | | eluzelz 9448 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
4 | 2, 3 | syl 14 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℤ) |
5 | | seqex 10346 |
. . 3
⊢ seq𝑀( · , 𝐹) ∈ V |
6 | 5 | a1i 9 |
. 2
⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ V) |
7 | | eqid 2157 |
. . . 4
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
8 | | eluzel2 9444 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
9 | 2, 8 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
10 | | eluzelz 9448 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
11 | 10 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℤ) |
12 | | iftrue 3510 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
13 | 12 | adantl 275 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
14 | | prodmo.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
15 | 14 | adantlr 469 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
16 | 13, 15 | eqeltrd 2234 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
17 | | iffalse 3513 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
18 | | ax-1cn 7825 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
19 | 17, 18 | eqeltrdi 2248 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
20 | 19 | adantl 275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
21 | | prodrbdc.dc |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴) |
22 | | exmiddc 822 |
. . . . . . . 8
⊢
(DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴)) |
23 | 21, 22 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴)) |
24 | 16, 20, 23 | mpjaodan 788 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
25 | | prodmo.1 |
. . . . . . 7
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) |
26 | 25 | fvmpt2 5551 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
27 | 11, 24, 26 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
28 | 27, 24 | eqeltrd 2234 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
29 | 7, 9, 28 | prodf 11435 |
. . 3
⊢ (𝜑 → seq𝑀( · , 𝐹):(ℤ≥‘𝑀)⟶ℂ) |
30 | 29, 2 | ffvelrnd 5603 |
. 2
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) |
31 | | mulid1 7875 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚) |
32 | 31 | adantl 275 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚) |
33 | 2 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
34 | | simpr 109 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ (ℤ≥‘𝑁)) |
35 | 9 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℤ) |
36 | 28 | adantlr 469 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
37 | 7, 35, 36 | prodf 11435 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → seq𝑀( · , 𝐹):(ℤ≥‘𝑀)⟶ℂ) |
38 | 37, 33 | ffvelrnd 5603 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) |
39 | | elfzuz 9924 |
. . . . . 6
⊢ (𝑚 ∈ ((𝑁 + 1)...𝑛) → 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) |
40 | | eluzelz 9448 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘(𝑁 + 1)) → 𝑚 ∈ ℤ) |
41 | 40 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑚 ∈
ℤ) |
42 | | fprodcvg.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) |
43 | 42 | sseld 3127 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑚 ∈ 𝐴 → 𝑚 ∈ (𝑀...𝑁))) |
44 | | fznuz 10004 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (𝑀...𝑁) → ¬ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) |
45 | 43, 44 | syl6 33 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ 𝐴 → ¬ 𝑚 ∈ (ℤ≥‘(𝑁 + 1)))) |
46 | 45 | con2d 614 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ (ℤ≥‘(𝑁 + 1)) → ¬ 𝑚 ∈ 𝐴)) |
47 | 46 | imp 123 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → ¬ 𝑚 ∈ 𝐴) |
48 | 41, 47 | eldifd 3112 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑚 ∈ (ℤ ∖ 𝐴)) |
49 | | fveqeq2 5477 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 1 ↔ (𝐹‘𝑚) = 1)) |
50 | | eldifi 3229 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → 𝑘 ∈ ℤ) |
51 | | eldifn 3230 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
52 | 51, 17 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
53 | 52, 18 | eqeltrdi 2248 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
54 | 50, 53, 26 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
55 | 54, 52 | eqtrd 2190 |
. . . . . . . 8
⊢ (𝑘 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑘) = 1) |
56 | 49, 55 | vtoclga 2778 |
. . . . . . 7
⊢ (𝑚 ∈ (ℤ ∖ 𝐴) → (𝐹‘𝑚) = 1) |
57 | 48, 56 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑚) = 1) |
58 | 39, 57 | sylan2 284 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝐹‘𝑚) = 1) |
59 | 58 | adantlr 469 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ ((𝑁 + 1)...𝑛)) → (𝐹‘𝑚) = 1) |
60 | | fveq2 5468 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) |
61 | 60 | eleq1d 2226 |
. . . . 5
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑚) ∈ ℂ)) |
62 | 28 | ralrimiva 2530 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) |
63 | 62 | ad2antrr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ∀𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) |
64 | | simpr 109 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ (ℤ≥‘𝑀)) |
65 | 61, 63, 64 | rspcdva 2821 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ) |
66 | | mulcl 7859 |
. . . . 5
⊢ ((𝑚 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑚 · 𝑣) ∈ ℂ) |
67 | 66 | adantl 275 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ (𝑚 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑚 · 𝑣) ∈ ℂ) |
68 | 32, 33, 34, 38, 59, 65, 67 | seq3id2 10408 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹)‘𝑁) = (seq𝑀( · , 𝐹)‘𝑛)) |
69 | 68 | eqcomd 2163 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹)‘𝑛) = (seq𝑀( · , 𝐹)‘𝑁)) |
70 | 1, 4, 6, 30, 69 | climconst 11187 |
1
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘𝑁)) |