Proof of Theorem seqz
Step | Hyp | Ref
| Expression |
1 | | seqz.5 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) |
2 | | elfzuz 12209 |
. . . 4
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
4 | | eluzelz 11573 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ ℤ) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
6 | | seq1 12676 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → (seq𝐾( + , 𝐹)‘𝐾) = (𝐹‘𝐾)) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝐾) = (𝐹‘𝐾)) |
8 | | seqz.7 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐾) = 𝑍) |
9 | 7, 8 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝐾) = 𝑍) |
10 | | seqeq1 12666 |
. . . . . . . 8
⊢ (𝐾 = 𝑀 → seq𝐾( + , 𝐹) = seq𝑀( + , 𝐹)) |
11 | 10 | fveq1d 6105 |
. . . . . . 7
⊢ (𝐾 = 𝑀 → (seq𝐾( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝐾)) |
12 | 11 | eqeq1d 2612 |
. . . . . 6
⊢ (𝐾 = 𝑀 → ((seq𝐾( + , 𝐹)‘𝐾) = 𝑍 ↔ (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)) |
13 | 9, 12 | syl5ibcom 234 |
. . . . 5
⊢ (𝜑 → (𝐾 = 𝑀 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)) |
14 | | eluzel2 11568 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
15 | 3, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
16 | | seqm1 12680 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹‘𝐾))) |
17 | 15, 16 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹‘𝐾))) |
18 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝐾) = 𝑍) |
19 | 18 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹‘𝐾)) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍)) |
20 | | eluzp1m1 11587 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘(𝑀 + 1))) → (𝐾 − 1) ∈
(ℤ≥‘𝑀)) |
21 | 15, 20 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐾 − 1) ∈
(ℤ≥‘𝑀)) |
22 | | fzssp1 12255 |
. . . . . . . . . . . . . . 15
⊢ (𝑀...(𝐾 − 1)) ⊆ (𝑀...((𝐾 − 1) + 1)) |
23 | 5 | zcnd 11359 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ ℂ) |
24 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
25 | | npcan 10169 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
26 | 23, 24, 25 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾) |
27 | 26 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀...((𝐾 − 1) + 1)) = (𝑀...𝐾)) |
28 | 22, 27 | syl5sseq 3616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝐾)) |
29 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
30 | 1, 29 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) |
31 | | fzss2 12252 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀...𝐾) ⊆ (𝑀...𝑁)) |
33 | 28, 32 | sstrd 3578 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁)) |
34 | 33 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁)) |
35 | 34 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...𝑁)) |
36 | | seqhomo.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
37 | 36 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
38 | 35, 37 | syldan 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐹‘𝑥) ∈ 𝑆) |
39 | | seqhomo.1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
40 | 39 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
41 | 21, 38, 40 | seqcl 12683 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐾 − 1)) ∈ 𝑆) |
42 | | seqz.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑍) |
43 | 42 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝑥 + 𝑍) = 𝑍) |
44 | 43 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → ∀𝑥 ∈ 𝑆 (𝑥 + 𝑍) = 𝑍) |
45 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘(𝐾 − 1)) → (𝑥 + 𝑍) = ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍)) |
46 | 45 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘(𝐾 − 1)) → ((𝑥 + 𝑍) = 𝑍 ↔ ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍)) |
47 | 46 | rspcv 3278 |
. . . . . . . . 9
⊢
((seq𝑀( + , 𝐹)‘(𝐾 − 1)) ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝑥 + 𝑍) = 𝑍 → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍)) |
48 | 41, 44, 47 | sylc 63 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + 𝑍) = 𝑍) |
49 | 19, 48 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → ((seq𝑀( + , 𝐹)‘(𝐾 − 1)) + (𝐹‘𝐾)) = 𝑍) |
50 | 17, 49 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍) |
51 | 50 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍)) |
52 | | uzp1 11597 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾 = 𝑀 ∨ 𝐾 ∈ (ℤ≥‘(𝑀 + 1)))) |
53 | 3, 52 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾 = 𝑀 ∨ 𝐾 ∈ (ℤ≥‘(𝑀 + 1)))) |
54 | 13, 51, 53 | mpjaod 395 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = 𝑍) |
55 | 54, 8 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐹‘𝐾)) |
56 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
57 | 3, 55, 30, 56 | seqfveq2 12685 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐹)‘𝑁)) |
58 | | fvex 6113 |
. . . . . 6
⊢ (𝐹‘𝐾) ∈ V |
59 | 58 | elsn 4140 |
. . . . 5
⊢ ((𝐹‘𝐾) ∈ {𝑍} ↔ (𝐹‘𝐾) = 𝑍) |
60 | 8, 59 | sylibr 223 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐾) ∈ {𝑍}) |
61 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ {𝑍}) |
62 | | velsn 4141 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑍} ↔ 𝑥 = 𝑍) |
63 | 61, 62 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦 ∈ 𝑆)) → 𝑥 = 𝑍) |
64 | 63 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑍 + 𝑦)) |
65 | | simprr 792 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
66 | | seqz.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑍) |
67 | 66 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑍) |
68 | 67 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦 ∈ 𝑆)) → ∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑍) |
69 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑍 + 𝑥) = (𝑍 + 𝑦)) |
70 | 69 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑍 + 𝑥) = 𝑍 ↔ (𝑍 + 𝑦) = 𝑍)) |
71 | 70 | rspcv 3278 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝑍 + 𝑥) = 𝑍 → (𝑍 + 𝑦) = 𝑍)) |
72 | 65, 68, 71 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦 ∈ 𝑆)) → (𝑍 + 𝑦) = 𝑍) |
73 | 64, 72 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = 𝑍) |
74 | | ovex 6577 |
. . . . . 6
⊢ (𝑥 + 𝑦) ∈ V |
75 | 74 | elsn 4140 |
. . . . 5
⊢ ((𝑥 + 𝑦) ∈ {𝑍} ↔ (𝑥 + 𝑦) = 𝑍) |
76 | 73, 75 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑍} ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ {𝑍}) |
77 | | peano2uz 11617 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾 + 1) ∈
(ℤ≥‘𝑀)) |
78 | 3, 77 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐾 + 1) ∈
(ℤ≥‘𝑀)) |
79 | | fzss1 12251 |
. . . . . . 7
⊢ ((𝐾 + 1) ∈
(ℤ≥‘𝑀) → ((𝐾 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
80 | 78, 79 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
81 | 80 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 𝑥 ∈ (𝑀...𝑁)) |
82 | 81, 36 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
83 | 60, 76, 30, 82 | seqcl2 12681 |
. . 3
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) ∈ {𝑍}) |
84 | | elsni 4142 |
. . 3
⊢
((seq𝐾( + , 𝐹)‘𝑁) ∈ {𝑍} → (seq𝐾( + , 𝐹)‘𝑁) = 𝑍) |
85 | 83, 84 | syl 17 |
. 2
⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = 𝑍) |
86 | 57, 85 | eqtrd 2644 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍) |