Step | Hyp | Ref
| Expression |
1 | | algcvga.5 |
. . . 4
⊢ 𝑁 = (𝐶‘𝐴) |
2 | | algcvga.3 |
. . . . 5
⊢ 𝐶:𝑆⟶ℕ0 |
3 | 2 | ffvelrni 6962 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → (𝐶‘𝐴) ∈
ℕ0) |
4 | 1, 3 | eqeltrid 2843 |
. . 3
⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈
ℕ0) |
5 | 4 | nn0zd 12422 |
. 2
⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈ ℤ) |
6 | | uzval 12582 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) |
7 | 6 | eleq2d 2824 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝐾 ∈
(ℤ≥‘𝑁) ↔ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
8 | 7 | pm5.32i 575 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘𝑁)) ↔ (𝑁 ∈ ℤ ∧ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
9 | | fveqeq2 6785 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝑁) = (𝑅‘𝑁))) |
10 | 9 | imbi2d 341 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁)))) |
11 | | fveqeq2 6785 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝑘) = (𝑅‘𝑁))) |
12 | 11 | imbi2d 341 |
. . . . . 6
⊢ (𝑚 = 𝑘 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝑘) = (𝑅‘𝑁)))) |
13 | | fveqeq2 6785 |
. . . . . . 7
⊢ (𝑚 = (𝑘 + 1) → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁))) |
14 | 13 | imbi2d 341 |
. . . . . 6
⊢ (𝑚 = (𝑘 + 1) → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
15 | | fveqeq2 6785 |
. . . . . . 7
⊢ (𝑚 = 𝐾 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝐾) = (𝑅‘𝑁))) |
16 | 15 | imbi2d 341 |
. . . . . 6
⊢ (𝑚 = 𝐾 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
17 | | eqidd 2739 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁)) |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁))) |
19 | 6 | eleq2d 2824 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑘 ∈
(ℤ≥‘𝑁) ↔ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
20 | 19 | pm5.32i 575 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘𝑁)) ↔ (𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
21 | | eluznn0 12655 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑁)) → 𝑘 ∈ ℕ0) |
22 | 4, 21 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → 𝑘 ∈ ℕ0) |
23 | | nn0uz 12618 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
24 | | algcvga.2 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 = seq0((𝐹 ∘ 1st ),
(ℕ0 × {𝐴})) |
25 | | 0zd 12329 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 0 ∈ ℤ) |
26 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆) |
27 | | algcvga.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹:𝑆⟶𝑆 |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 𝐹:𝑆⟶𝑆) |
29 | 23, 24, 25, 26, 28 | algrp1 16277 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
30 | 22, 29 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
31 | 23, 24, 25, 26, 28 | algrf 16276 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑆 → 𝑅:ℕ0⟶𝑆) |
32 | 31 | ffvelrnda 6963 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘𝑘) ∈ 𝑆) |
33 | 22, 32 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘𝑘) ∈ 𝑆) |
34 | | algcvga.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧))) |
35 | 27, 24, 2, 34, 1 | algcvga 16282 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → (𝑘 ∈ (ℤ≥‘𝑁) → (𝐶‘(𝑅‘𝑘)) = 0)) |
36 | 35 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐶‘(𝑅‘𝑘)) = 0) |
37 | | fveqeq2 6785 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑅‘𝑘) → ((𝐶‘𝑧) = 0 ↔ (𝐶‘(𝑅‘𝑘)) = 0)) |
38 | | fveq2 6776 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → (𝐹‘𝑧) = (𝐹‘(𝑅‘𝑘))) |
39 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → 𝑧 = (𝑅‘𝑘)) |
40 | 38, 39 | eqeq12d 2754 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑅‘𝑘) → ((𝐹‘𝑧) = 𝑧 ↔ (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘))) |
41 | 37, 40 | imbi12d 345 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑅‘𝑘) → (((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧) ↔ ((𝐶‘(𝑅‘𝑘)) = 0 → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘)))) |
42 | | algfx.6 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → ((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧)) |
43 | 41, 42 | vtoclga 3512 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑘) ∈ 𝑆 → ((𝐶‘(𝑅‘𝑘)) = 0 → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘))) |
44 | 33, 36, 43 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘)) |
45 | 30, 44 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑘)) |
46 | 45 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → ((𝑅‘(𝑘 + 1)) = (𝑅‘𝑁) ↔ (𝑅‘𝑘) = (𝑅‘𝑁))) |
47 | 46 | biimprd 247 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁))) |
48 | 47 | expcom 414 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
49 | 48 | adantl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘𝑁)) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
50 | 20, 49 | sylbir 234 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
51 | 50 | a2d 29 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → ((𝐴 ∈ 𝑆 → (𝑅‘𝑘) = (𝑅‘𝑁)) → (𝐴 ∈ 𝑆 → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
52 | 10, 12, 14, 16, 18, 51 | uzind3 12412 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁))) |
53 | 8, 52 | sylbi 216 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁))) |
54 | 53 | ex 413 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝐾 ∈
(ℤ≥‘𝑁) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
55 | 54 | com3r 87 |
. 2
⊢ (𝐴 ∈ 𝑆 → (𝑁 ∈ ℤ → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
56 | 5, 55 | mpd 15 |
1
⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁))) |