Step | Hyp | Ref
| Expression |
1 | | algcvga.5 |
. . . 4
⊢ 𝑁 = (𝐶‘𝐴) |
2 | | algcvga.3 |
. . . . 5
⊢ 𝐶:𝑆⟶ℕ0 |
3 | 2 | ffvelrni 5301 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → (𝐶‘𝐴) ∈
ℕ0) |
4 | 1, 3 | syl5eqel 2124 |
. . 3
⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈
ℕ0) |
5 | 4 | nn0zd 8358 |
. 2
⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈ ℤ) |
6 | | uzval 8475 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) |
7 | 6 | eleq2d 2107 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝐾 ∈
(ℤ≥‘𝑁) ↔ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
8 | 7 | pm5.32i 427 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘𝑁)) ↔ (𝑁 ∈ ℤ ∧ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
9 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → (𝑅‘𝑚) = (𝑅‘𝑁)) |
10 | 9 | eqeq1d 2048 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝑁) = (𝑅‘𝑁))) |
11 | 10 | imbi2d 219 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁)))) |
12 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (𝑅‘𝑚) = (𝑅‘𝑘)) |
13 | 12 | eqeq1d 2048 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝑘) = (𝑅‘𝑁))) |
14 | 13 | imbi2d 219 |
. . . . . 6
⊢ (𝑚 = 𝑘 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝑘) = (𝑅‘𝑁)))) |
15 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 + 1) → (𝑅‘𝑚) = (𝑅‘(𝑘 + 1))) |
16 | 15 | eqeq1d 2048 |
. . . . . . 7
⊢ (𝑚 = (𝑘 + 1) → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁))) |
17 | 16 | imbi2d 219 |
. . . . . 6
⊢ (𝑚 = (𝑘 + 1) → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
18 | | fveq2 5178 |
. . . . . . . 8
⊢ (𝑚 = 𝐾 → (𝑅‘𝑚) = (𝑅‘𝐾)) |
19 | 18 | eqeq1d 2048 |
. . . . . . 7
⊢ (𝑚 = 𝐾 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝐾) = (𝑅‘𝑁))) |
20 | 19 | imbi2d 219 |
. . . . . 6
⊢ (𝑚 = 𝐾 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
21 | | eqidd 2041 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁)) |
22 | 21 | a1i 9 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁))) |
23 | 6 | eleq2d 2107 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑘 ∈
(ℤ≥‘𝑁) ↔ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
24 | 23 | pm5.32i 427 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘𝑁)) ↔ (𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
25 | | eluznn0 8537 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑁)) → 𝑘 ∈ ℕ0) |
26 | 4, 25 | sylan 267 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → 𝑘 ∈ ℕ0) |
27 | | nn0uz 8507 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
28 | | algcvga.2 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 = seq0((𝐹 ∘ 1st ),
(ℕ0 × {𝐴}), 𝑆) |
29 | | 0zd 8257 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 0 ∈ ℤ) |
30 | | id 19 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆) |
31 | | algcvga.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹:𝑆⟶𝑆 |
32 | 31 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 𝐹:𝑆⟶𝑆) |
33 | | ialgcvga.s |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 ∈ 𝑉 |
34 | 33 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 𝑆 ∈ 𝑉) |
35 | 27, 28, 29, 30, 32, 34 | ialgrp1 9885 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
36 | 26, 35 | syldan 266 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
37 | 27, 28, 29, 30, 32, 34 | ialgrf 9884 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑆 → 𝑅:ℕ0⟶𝑆) |
38 | 37 | ffvelrnda 5302 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘𝑘) ∈ 𝑆) |
39 | 26, 38 | syldan 266 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘𝑘) ∈ 𝑆) |
40 | | algcvga.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧))) |
41 | 31, 28, 2, 40, 1, 33 | ialgcvga 9890 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → (𝑘 ∈ (ℤ≥‘𝑁) → (𝐶‘(𝑅‘𝑘)) = 0)) |
42 | 41 | imp 115 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐶‘(𝑅‘𝑘)) = 0) |
43 | | fveq2 5178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → (𝐶‘𝑧) = (𝐶‘(𝑅‘𝑘))) |
44 | 43 | eqeq1d 2048 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑅‘𝑘) → ((𝐶‘𝑧) = 0 ↔ (𝐶‘(𝑅‘𝑘)) = 0)) |
45 | | fveq2 5178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → (𝐹‘𝑧) = (𝐹‘(𝑅‘𝑘))) |
46 | | id 19 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → 𝑧 = (𝑅‘𝑘)) |
47 | 45, 46 | eqeq12d 2054 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑅‘𝑘) → ((𝐹‘𝑧) = 𝑧 ↔ (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘))) |
48 | 44, 47 | imbi12d 223 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑅‘𝑘) → (((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧) ↔ ((𝐶‘(𝑅‘𝑘)) = 0 → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘)))) |
49 | | algfx.6 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → ((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧)) |
50 | 48, 49 | vtoclga 2619 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑘) ∈ 𝑆 → ((𝐶‘(𝑅‘𝑘)) = 0 → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘))) |
51 | 39, 42, 50 | sylc 56 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘)) |
52 | 36, 51 | eqtrd 2072 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑘)) |
53 | 52 | eqeq1d 2048 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → ((𝑅‘(𝑘 + 1)) = (𝑅‘𝑁) ↔ (𝑅‘𝑘) = (𝑅‘𝑁))) |
54 | 53 | biimprd 147 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁))) |
55 | 54 | expcom 109 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
56 | 55 | adantl 262 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘𝑁)) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
57 | 24, 56 | sylbir 125 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
58 | 57 | a2d 23 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → ((𝐴 ∈ 𝑆 → (𝑅‘𝑘) = (𝑅‘𝑁)) → (𝐴 ∈ 𝑆 → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
59 | 11, 14, 17, 20, 22, 58 | uzind3 8351 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁))) |
60 | 8, 59 | sylbi 114 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁))) |
61 | 60 | ex 108 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝐾 ∈
(ℤ≥‘𝑁) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
62 | 61 | com3r 73 |
. 2
⊢ (𝐴 ∈ 𝑆 → (𝑁 ∈ ℤ → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
63 | 5, 62 | mpd 13 |
1
⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁))) |