Step | Hyp | Ref
| Expression |
1 | | seqz.5 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) |
2 | | elfzuz3 9965 |
. . 3
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) |
4 | | fveqeq2 5503 |
. . . 4
⊢ (𝑤 = 𝐾 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)) |
5 | 4 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝐾 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍))) |
6 | | fveqeq2 5503 |
. . . 4
⊢ (𝑤 = 𝑘 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍)) |
7 | 6 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑘 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑘) = 𝑍))) |
8 | | fveqeq2 5503 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍)) |
9 | 8 | imbi2d 229 |
. . 3
⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍))) |
10 | | fveqeq2 5503 |
. . . 4
⊢ (𝑤 = 𝑁 → ((seq𝑀( + , 𝐹)‘𝑤) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)) |
11 | 10 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑁 → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑤) = 𝑍) ↔ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍))) |
12 | | elfzuz 9964 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
13 | 1, 12 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
14 | | eluzelz 9483 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ ℤ) |
15 | 13, 14 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
16 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → 𝑥 ∈ (ℤ≥‘𝐾)) |
17 | 13 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (ℤ≥‘𝑀)) |
18 | | uztrn 9490 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
19 | 16, 17, 18 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
20 | | seq3homo.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
21 | 19, 20 | syldan 280 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆) |
22 | | seq3homo.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
23 | 15, 21, 22 | seq3-1 10403 |
. . . . . . 7
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝐾) = (𝐹‘𝐾)) |
24 | | seqz.7 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐾) = 𝑍) |
25 | 23, 24 | eqtrd 2203 |
. . . . . 6
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝐾) = 𝑍) |
26 | | seqeq1 10391 |
. . . . . . . 8
⊢ (𝐾 = 𝑀 → seq𝐾( + , 𝐹) = seq𝑀( + , 𝐹)) |
27 | 26 | fveq1d 5496 |
. . . . . . 7
⊢ (𝐾 = 𝑀 → (seq𝐾( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾)) |
28 | 27 | eqeq1d 2179 |
. . . . . 6
⊢ (𝐾 = 𝑀 → ((seq𝐾( + , 𝐹)‘𝐾) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)) |
29 | 25, 28 | syl5ibcom 154 |
. . . . 5
⊢ (𝜑 → (𝐾 = 𝑀 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)) |
30 | | eluzel2 9479 |
. . . . . . . . . 10
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
31 | 13, 30 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
32 | 31 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ) |
33 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) |
34 | 20 | adantlr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
35 | 22 | adantlr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
36 | 32, 33, 34, 35 | seq3m1 10411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹‘𝐾))) |
37 | 24 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝐾) = 𝑍) |
38 | 37 | oveq2d 5866 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹‘𝐾)) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍)) |
39 | | oveq1 5857 |
. . . . . . . . 9
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘(𝐾 − 1)) → (𝑥 + 𝑍) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍)) |
40 | 39 | eqeq1d 2179 |
. . . . . . . 8
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘(𝐾 − 1)) → ((𝑥 + 𝑍) = 𝑍 ↔ ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍)) |
41 | | seqz.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑍) |
42 | 41 | ralrimiva 2543 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝑥 + 𝑍) = 𝑍) |
43 | 42 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → ∀𝑥 ∈ 𝑆 (𝑥 + 𝑍) = 𝑍) |
44 | | eqid 2170 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
45 | 44, 32, 34, 35 | seqf 10404 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → seq𝑀( + , 𝐹):(ℤ≥‘𝑀)⟶𝑆) |
46 | | eluzp1m1 9497 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘(𝑀 + 1))) → (𝐾 − 1) ∈
(ℤ≥‘𝑀)) |
47 | 31, 46 | sylan 281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐾 − 1) ∈
(ℤ≥‘𝑀)) |
48 | 45, 47 | ffvelrnd 5629 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐾 − 1)) ∈ 𝑆) |
49 | 40, 43, 48 | rspcdva 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍) |
50 | 36, 38, 49 | 3eqtrd 2207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍) |
51 | 50 | ex 114 |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)) |
52 | | uzp1 9507 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾 = 𝑀 ∨ 𝐾 ∈ (ℤ≥‘(𝑀 + 1)))) |
53 | 13, 52 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝐾 = 𝑀 ∨ 𝐾 ∈ (ℤ≥‘(𝑀 + 1)))) |
54 | 29, 51, 53 | mpjaod 713 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍) |
55 | 54 | a1i 9 |
. . 3
⊢ (𝐾 ∈ ℤ → (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)) |
56 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → 𝑘 ∈ (ℤ≥‘𝐾)) |
57 | 13 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (ℤ≥‘𝑀)) |
58 | | uztrn 9490 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
59 | 56, 57, 58 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
60 | 20 | adantlr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
61 | 22 | adantlr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
62 | 59, 60, 61 | seq3p1 10405 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
63 | 62 | adantr 274 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
64 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) |
65 | 64 | oveq1d 5865 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))) = (𝑍 + (𝐹‘(𝑘 + 1)))) |
66 | | oveq2 5858 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑍 + 𝑥) = (𝑍 + (𝐹‘(𝑘 + 1)))) |
67 | 66 | eqeq1d 2179 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘(𝑘 + 1)) → ((𝑍 + 𝑥) = 𝑍 ↔ (𝑍 + (𝐹‘(𝑘 + 1))) = 𝑍)) |
68 | | seqz.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑍) |
69 | 68 | ralrimiva 2543 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑍) |
70 | 69 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → ∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑍) |
71 | | fveq2 5494 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1))) |
72 | 71 | eleq1d 2239 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑘 + 1)) ∈ 𝑆)) |
73 | 20 | ralrimiva 2543 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆) |
74 | 73 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → ∀𝑥 ∈
(ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆) |
75 | | peano2uz 9529 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝑘 + 1) ∈
(ℤ≥‘𝑀)) |
76 | 59, 75 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → (𝑘 + 1) ∈
(ℤ≥‘𝑀)) |
77 | 72, 74, 76 | rspcdva 2839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → (𝐹‘(𝑘 + 1)) ∈ 𝑆) |
78 | 67, 70, 77 | rspcdva 2839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → (𝑍 + (𝐹‘(𝑘 + 1))) = 𝑍) |
79 | 78 | adantr 274 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (𝑍 + (𝐹‘(𝑘 + 1))) = 𝑍) |
80 | 63, 65, 79 | 3eqtrd 2207 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) ∧ (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍) |
81 | 80 | ex 114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → ((seq𝑀( + , 𝐹)‘𝑘) = 𝑍 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍)) |
82 | 81 | expcom 115 |
. . . 4
⊢ (𝑘 ∈
(ℤ≥‘𝐾) → (𝜑 → ((seq𝑀( + , 𝐹)‘𝑘) = 𝑍 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍))) |
83 | 82 | a2d 26 |
. . 3
⊢ (𝑘 ∈
(ℤ≥‘𝐾) → ((𝜑 → (seq𝑀( + , 𝐹)‘𝑘) = 𝑍) → (𝜑 → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = 𝑍))) |
84 | 5, 7, 9, 11, 55, 83 | uzind4 9534 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)) |
85 | 3, 84 | mpcom 36 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍) |