Step | Hyp | Ref
| Expression |
1 | | prodfap0.1 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz2 9940 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
4 | | fveq2 5470 |
. . . . 5
⊢ (𝑚 = 𝑀 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑀)) |
5 | 4 | breq1d 3977 |
. . . 4
⊢ (𝑚 = 𝑀 → ((seq𝑀( · , 𝐹)‘𝑚) # 0 ↔ (seq𝑀( · , 𝐹)‘𝑀) # 0)) |
6 | 5 | imbi2d 229 |
. . 3
⊢ (𝑚 = 𝑀 → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑚) # 0) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘𝑀) # 0))) |
7 | | fveq2 5470 |
. . . . 5
⊢ (𝑚 = 𝑛 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑛)) |
8 | 7 | breq1d 3977 |
. . . 4
⊢ (𝑚 = 𝑛 → ((seq𝑀( · , 𝐹)‘𝑚) # 0 ↔ (seq𝑀( · , 𝐹)‘𝑛) # 0)) |
9 | 8 | imbi2d 229 |
. . 3
⊢ (𝑚 = 𝑛 → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑚) # 0) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘𝑛) # 0))) |
10 | | fveq2 5470 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘(𝑛 + 1))) |
11 | 10 | breq1d 3977 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → ((seq𝑀( · , 𝐹)‘𝑚) # 0 ↔ (seq𝑀( · , 𝐹)‘(𝑛 + 1)) # 0)) |
12 | 11 | imbi2d 229 |
. . 3
⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑚) # 0) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) # 0))) |
13 | | fveq2 5470 |
. . . . 5
⊢ (𝑚 = 𝑁 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑁)) |
14 | 13 | breq1d 3977 |
. . . 4
⊢ (𝑚 = 𝑁 → ((seq𝑀( · , 𝐹)‘𝑚) # 0 ↔ (seq𝑀( · , 𝐹)‘𝑁) # 0)) |
15 | 14 | imbi2d 229 |
. . 3
⊢ (𝑚 = 𝑁 → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑚) # 0) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0))) |
16 | | eluzfz1 9939 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
17 | | elfzelz 9934 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) |
18 | 17 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ) |
19 | | prodfap0.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
20 | 19 | adantlr 469 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
21 | | mulcl 7861 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑘 · 𝑣) ∈ ℂ) |
22 | 21 | adantl 275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) ∧ (𝑘 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑘 · 𝑣) ∈ ℂ) |
23 | 18, 20, 22 | seq3-1 10368 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (seq𝑀( · , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
24 | | fveq2 5470 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
25 | 24 | breq1d 3977 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) # 0 ↔ (𝐹‘𝑀) # 0)) |
26 | 25 | imbi2d 229 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → ((𝜑 → (𝐹‘𝑘) # 0) ↔ (𝜑 → (𝐹‘𝑀) # 0))) |
27 | | prodfap0.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) # 0) |
28 | 27 | expcom 115 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘𝑘) # 0)) |
29 | 26, 28 | vtoclga 2778 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘𝑀) # 0)) |
30 | 29 | impcom 124 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (𝐹‘𝑀) # 0) |
31 | 23, 30 | eqbrtrd 3988 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (seq𝑀( · , 𝐹)‘𝑀) # 0) |
32 | 31 | expcom 115 |
. . . 4
⊢ (𝑀 ∈ (𝑀...𝑁) → (𝜑 → (seq𝑀( · , 𝐹)‘𝑀) # 0)) |
33 | 16, 32 | syl 14 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (seq𝑀( · , 𝐹)‘𝑀) # 0)) |
34 | | elfzouz 10059 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
35 | 34 | 3ad2ant2 1004 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) → 𝑛 ∈ (ℤ≥‘𝑀)) |
36 | 19 | 3ad2antl1 1144 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
37 | 21 | adantl 275 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) ∧ (𝑘 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑘 · 𝑣) ∈ ℂ) |
38 | 35, 36, 37 | seq3p1 10370 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) |
39 | | elfzofz 10070 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑛 ∈ (𝑀...𝑁)) |
40 | | elfzuz 9930 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
41 | | eqid 2157 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
42 | 1, 16, 17 | 3syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℤ) |
43 | 41, 42, 19 | prodf 11446 |
. . . . . . . . . . . 12
⊢ (𝜑 → seq𝑀( · , 𝐹):(ℤ≥‘𝑀)⟶ℂ) |
44 | 43 | ffvelrnda 5604 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (seq𝑀( · , 𝐹)‘𝑛) ∈ ℂ) |
45 | 40, 44 | sylan2 284 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → (seq𝑀( · , 𝐹)‘𝑛) ∈ ℂ) |
46 | 39, 45 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( · , 𝐹)‘𝑛) ∈ ℂ) |
47 | 46 | 3adant3 1002 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) → (seq𝑀( · , 𝐹)‘𝑛) ∈ ℂ) |
48 | | fzofzp1 10135 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
49 | | fveq2 5470 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
50 | 49 | eleq1d 2226 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘(𝑛 + 1)) ∈ ℂ)) |
51 | 50 | imbi2d 229 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → ((𝜑 → (𝐹‘𝑘) ∈ ℂ) ↔ (𝜑 → (𝐹‘(𝑛 + 1)) ∈ ℂ))) |
52 | | elfzuz 9930 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) |
53 | 19 | expcom 115 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝜑 → (𝐹‘𝑘) ∈ ℂ)) |
54 | 52, 53 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘𝑘) ∈ ℂ)) |
55 | 51, 54 | vtoclga 2778 |
. . . . . . . . . . 11
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘(𝑛 + 1)) ∈ ℂ)) |
56 | 48, 55 | syl 14 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → (𝐹‘(𝑛 + 1)) ∈ ℂ)) |
57 | 56 | impcom 124 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑛 + 1)) ∈ ℂ) |
58 | 57 | 3adant3 1002 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) → (𝐹‘(𝑛 + 1)) ∈ ℂ) |
59 | | simp3 984 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) → (seq𝑀( · , 𝐹)‘𝑛) # 0) |
60 | 49 | breq1d 3977 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) # 0 ↔ (𝐹‘(𝑛 + 1)) # 0)) |
61 | 60 | imbi2d 229 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 + 1) → ((𝜑 → (𝐹‘𝑘) # 0) ↔ (𝜑 → (𝐹‘(𝑛 + 1)) # 0))) |
62 | 61, 28 | vtoclga 2778 |
. . . . . . . . . . 11
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘(𝑛 + 1)) # 0)) |
63 | 62 | impcom 124 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑛 + 1)) # 0) |
64 | 48, 63 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑛 + 1)) # 0) |
65 | 64 | 3adant3 1002 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) → (𝐹‘(𝑛 + 1)) # 0) |
66 | 47, 58, 59, 65 | mulap0d 8536 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) # 0) |
67 | 38, 66 | eqbrtrd 3988 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐹)‘𝑛) # 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) # 0) |
68 | 67 | 3exp 1184 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (𝑀..^𝑁) → ((seq𝑀( · , 𝐹)‘𝑛) # 0 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) # 0))) |
69 | 68 | com12 30 |
. . . 4
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → ((seq𝑀( · , 𝐹)‘𝑛) # 0 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) # 0))) |
70 | 69 | a2d 26 |
. . 3
⊢ (𝑛 ∈ (𝑀..^𝑁) → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑛) # 0) → (𝜑 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) # 0))) |
71 | 6, 9, 12, 15, 33, 70 | fzind2 10147 |
. 2
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0)) |
72 | 3, 71 | mpcom 36 |
1
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0) |