Step | Hyp | Ref
| Expression |
1 | | algcvga.5 |
. . . 4
⊢ 𝑁 = (𝐶‘𝐴) |
2 | | algcvga.3 |
. . . . 5
⊢ 𝐶:𝑆⟶ℕ0 |
3 | 2 | ffvelrni 5322 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → (𝐶‘𝐴) ∈
ℕ0) |
4 | 1, 3 | syl5eqel 2165 |
. . 3
⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈
ℕ0) |
5 | 4 | nn0zd 8467 |
. 2
⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈ ℤ) |
6 | | uzval 8621 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) |
7 | 6 | eleq2d 2148 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝐾 ∈
(ℤ≥‘𝑁) ↔ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
8 | 7 | pm5.32i 441 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘𝑁)) ↔ (𝑁 ∈ ℤ ∧ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
9 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → (𝑅‘𝑚) = (𝑅‘𝑁)) |
10 | 9 | eqeq1d 2089 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝑁) = (𝑅‘𝑁))) |
11 | 10 | imbi2d 228 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁)))) |
12 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (𝑅‘𝑚) = (𝑅‘𝑘)) |
13 | 12 | eqeq1d 2089 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝑘) = (𝑅‘𝑁))) |
14 | 13 | imbi2d 228 |
. . . . . 6
⊢ (𝑚 = 𝑘 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝑘) = (𝑅‘𝑁)))) |
15 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 + 1) → (𝑅‘𝑚) = (𝑅‘(𝑘 + 1))) |
16 | 15 | eqeq1d 2089 |
. . . . . . 7
⊢ (𝑚 = (𝑘 + 1) → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁))) |
17 | 16 | imbi2d 228 |
. . . . . 6
⊢ (𝑚 = (𝑘 + 1) → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
18 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑚 = 𝐾 → (𝑅‘𝑚) = (𝑅‘𝐾)) |
19 | 18 | eqeq1d 2089 |
. . . . . . 7
⊢ (𝑚 = 𝐾 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝐾) = (𝑅‘𝑁))) |
20 | 19 | imbi2d 228 |
. . . . . 6
⊢ (𝑚 = 𝐾 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
21 | | eqidd 2082 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁)) |
22 | 21 | a1i 9 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁))) |
23 | 6 | eleq2d 2148 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑘 ∈
(ℤ≥‘𝑁) ↔ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
24 | 23 | pm5.32i 441 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘𝑁)) ↔ (𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
25 | | eluznn0 8686 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑁)) → 𝑘 ∈ ℕ0) |
26 | 4, 25 | sylan 277 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → 𝑘 ∈ ℕ0) |
27 | | nn0uz 8653 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
28 | | algcvga.2 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 = seq0((𝐹 ∘ 1st ),
(ℕ0 × {𝐴}), 𝑆) |
29 | | 0zd 8363 |
. . . . . . . . . . . . . . 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 10428 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
36 | 26, 35 | syldan 276 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
37 | 27, 28, 29, 30, 32, 34 | ialgrf 10427 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑆 → 𝑅:ℕ0⟶𝑆) |
38 | 37 | ffvelrnda 5323 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘𝑘) ∈ 𝑆) |
39 | 26, 38 | syldan 276 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘𝑘) ∈ 𝑆) |
40 | | algcvga.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧))) |
41 | 31, 28, 2, 40, 1, 33 | ialgcvga 10433 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → (𝑘 ∈ (ℤ≥‘𝑁) → (𝐶‘(𝑅‘𝑘)) = 0)) |
42 | 41 | imp 122 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐶‘(𝑅‘𝑘)) = 0) |
43 | | fveq2 5198 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → (𝐶‘𝑧) = (𝐶‘(𝑅‘𝑘))) |
44 | 43 | eqeq1d 2089 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑅‘𝑘) → ((𝐶‘𝑧) = 0 ↔ (𝐶‘(𝑅‘𝑘)) = 0)) |
45 | | fveq2 5198 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → (𝐹‘𝑧) = (𝐹‘(𝑅‘𝑘))) |
46 | | id 19 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → 𝑧 = (𝑅‘𝑘)) |
47 | 45, 46 | eqeq12d 2095 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑅‘𝑘) → ((𝐹‘𝑧) = 𝑧 ↔ (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘))) |
48 | 44, 47 | imbi12d 232 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑅‘𝑘) → (((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧) ↔ ((𝐶‘(𝑅‘𝑘)) = 0 → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘)))) |
49 | | algfx.6 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → ((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧)) |
50 | 48, 49 | vtoclga 2664 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑘) ∈ 𝑆 → ((𝐶‘(𝑅‘𝑘)) = 0 → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘))) |
51 | 39, 42, 50 | sylc 61 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘)) |
52 | 36, 51 | eqtrd 2113 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑘)) |
53 | 52 | eqeq1d 2089 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → ((𝑅‘(𝑘 + 1)) = (𝑅‘𝑁) ↔ (𝑅‘𝑘) = (𝑅‘𝑁))) |
54 | 53 | biimprd 156 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁))) |
55 | 54 | expcom 114 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
56 | 55 | adantl 271 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘𝑁)) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
57 | 24, 56 | sylbir 133 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
58 | 57 | a2d 26 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → ((𝐴 ∈ 𝑆 → (𝑅‘𝑘) = (𝑅‘𝑁)) → (𝐴 ∈ 𝑆 → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
59 | 11, 14, 17, 20, 22, 58 | uzind3 8460 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁))) |
60 | 8, 59 | sylbi 119 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁))) |
61 | 60 | ex 113 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝐾 ∈
(ℤ≥‘𝑁) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
62 | 61 | com3r 78 |
. 2
⊢ (𝐴 ∈ 𝑆 → (𝑁 ∈ ℤ → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
63 | 5, 62 | mpd 13 |
1
⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁))) |