Step | Hyp | Ref
| Expression |
1 | | seq3clss.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz2 9961 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
4 | | fveq2 5483 |
. . . . 5
⊢ (𝑤 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑤) = (seq𝑀( + , 𝐹)‘𝑀)) |
5 | 4 | eleq1d 2233 |
. . . 4
⊢ (𝑤 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑤) ∈ 𝑆 ↔ (seq𝑀( + , 𝐹)‘𝑀) ∈ 𝑆)) |
6 | 5 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑀 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) ∈ 𝑆) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) ∈ 𝑆))) |
7 | | fveq2 5483 |
. . . . 5
⊢ (𝑤 = 𝑘 → (seq𝑀( + , 𝐹)‘𝑤) = (seq𝑀( + , 𝐹)‘𝑘)) |
8 | 7 | eleq1d 2233 |
. . . 4
⊢ (𝑤 = 𝑘 → ((seq𝑀( + , 𝐹)‘𝑤) ∈ 𝑆 ↔ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆)) |
9 | 8 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑘 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) ∈ 𝑆) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆))) |
10 | | fveq2 5483 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → (seq𝑀( + , 𝐹)‘𝑤) = (seq𝑀( + , 𝐹)‘(𝑘 + 1))) |
11 | 10 | eleq1d 2233 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → ((seq𝑀( + , 𝐹)‘𝑤) ∈ 𝑆 ↔ (seq𝑀( + , 𝐹)‘(𝑘 + 1)) ∈ 𝑆)) |
12 | 11 | imbi2d 229 |
. . 3
⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) ∈ 𝑆) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) ∈ 𝑆))) |
13 | | fveq2 5483 |
. . . . 5
⊢ (𝑤 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑤) = (seq𝑀( + , 𝐹)‘𝑁)) |
14 | 13 | eleq1d 2233 |
. . . 4
⊢ (𝑤 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝑤) ∈ 𝑆 ↔ (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆)) |
15 | 14 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑁 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) ∈ 𝑆) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆))) |
16 | | eluzel2 9465 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
17 | 1, 16 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
18 | | seq3clss.ft |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑇) |
19 | | seq3clss.tcl |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥 + 𝑦) ∈ 𝑇) |
20 | 17, 18, 19 | seq3-1 10389 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
21 | | fveq2 5483 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
22 | 21 | eleq1d 2233 |
. . . . . 6
⊢ (𝑥 = 𝑀 → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘𝑀) ∈ 𝑆)) |
23 | | seq3clss.fs |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
24 | 23 | ralrimiva 2537 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ 𝑆) |
25 | | eluzfz1 9960 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
26 | 1, 25 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
27 | 22, 24, 26 | rspcdva 2833 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝑆) |
28 | 20, 27 | eqeltrd 2241 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) ∈ 𝑆) |
29 | 28 | a1i 9 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) ∈ 𝑆)) |
30 | | elfzouz 10080 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) |
31 | 30 | ad2antlr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → 𝑘 ∈ (ℤ≥‘𝑀)) |
32 | 18 | adantlr 469 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑇) |
33 | 32 | adantlr 469 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑇) |
34 | 19 | adantlr 469 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥 + 𝑦) ∈ 𝑇) |
35 | 34 | adantlr 469 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥 + 𝑦) ∈ 𝑇) |
36 | 31, 33, 35 | seq3p1 10391 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
37 | | seq3clss.scl |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
38 | 37 | adantlr 469 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
39 | 38 | adantlr 469 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
40 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) |
41 | | fveq2 5483 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1))) |
42 | 41 | eleq1d 2233 |
. . . . . . . . 9
⊢ (𝑥 = (𝑘 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑘 + 1)) ∈ 𝑆)) |
43 | 24 | ad2antrr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ 𝑆) |
44 | | fzofzp1 10156 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
45 | 44 | ad2antlr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
46 | 42, 43, 45 | rspcdva 2833 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → (𝐹‘(𝑘 + 1)) ∈ 𝑆) |
47 | 39, 40, 46 | caovcld 5989 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))) ∈ 𝑆) |
48 | 36, 47 | eqeltrd 2241 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) ∈ 𝑆) |
49 | 48 | ex 114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) ∈ 𝑆)) |
50 | 49 | expcom 115 |
. . . 4
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝜑 → ((seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) ∈ 𝑆))) |
51 | 50 | a2d 26 |
. . 3
⊢ (𝑘 ∈ (𝑀..^𝑁) → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑘) ∈ 𝑆) → (𝜑 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) ∈ 𝑆))) |
52 | 6, 9, 12, 15, 29, 51 | fzind2 10168 |
. 2
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆)) |
53 | 3, 52 | mpcom 36 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆) |