Step | Hyp | Ref
| Expression |
1 | | algcvga.5 |
. . . 4
⊢ 𝑁 = (𝐶‘𝐴) |
2 | | algcvga.3 |
. . . . 5
⊢ 𝐶:𝑆⟶ℕ0 |
3 | 2 | ffvelrni 6266 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → (𝐶‘𝐴) ∈
ℕ0) |
4 | 1, 3 | syl5eqel 2692 |
. . 3
⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈
ℕ0) |
5 | 4 | nn0zd 11356 |
. 2
⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈ ℤ) |
6 | | uzval 11565 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) |
7 | 6 | eleq2d 2673 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝐾 ∈
(ℤ≥‘𝑁) ↔ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
8 | 7 | pm5.32i 667 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘𝑁)) ↔ (𝑁 ∈ ℤ ∧ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
9 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → (𝑅‘𝑚) = (𝑅‘𝑁)) |
10 | 9 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝑁) = (𝑅‘𝑁))) |
11 | 10 | imbi2d 329 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁)))) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (𝑅‘𝑚) = (𝑅‘𝑘)) |
13 | 12 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝑘) = (𝑅‘𝑁))) |
14 | 13 | imbi2d 329 |
. . . . . 6
⊢ (𝑚 = 𝑘 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝑘) = (𝑅‘𝑁)))) |
15 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 + 1) → (𝑅‘𝑚) = (𝑅‘(𝑘 + 1))) |
16 | 15 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑚 = (𝑘 + 1) → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁))) |
17 | 16 | imbi2d 329 |
. . . . . 6
⊢ (𝑚 = (𝑘 + 1) → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
18 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = 𝐾 → (𝑅‘𝑚) = (𝑅‘𝐾)) |
19 | 18 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑚 = 𝐾 → ((𝑅‘𝑚) = (𝑅‘𝑁) ↔ (𝑅‘𝐾) = (𝑅‘𝑁))) |
20 | 19 | imbi2d 329 |
. . . . . 6
⊢ (𝑚 = 𝐾 → ((𝐴 ∈ 𝑆 → (𝑅‘𝑚) = (𝑅‘𝑁)) ↔ (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
21 | | eqidd 2611 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁)) |
22 | 21 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝐴 ∈ 𝑆 → (𝑅‘𝑁) = (𝑅‘𝑁))) |
23 | 6 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑘 ∈
(ℤ≥‘𝑁) ↔ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
24 | 23 | pm5.32i 667 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘𝑁)) ↔ (𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧})) |
25 | | eluznn0 11633 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑁)) → 𝑘 ∈ ℕ0) |
26 | 4, 25 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → 𝑘 ∈ ℕ0) |
27 | | nn0uz 11598 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
28 | | algcvga.2 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 = seq0((𝐹 ∘ 1st ),
(ℕ0 × {𝐴})) |
29 | | 0zd 11266 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 0 ∈ ℤ) |
30 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆) |
31 | | algcvga.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹:𝑆⟶𝑆 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → 𝐹:𝑆⟶𝑆) |
33 | 27, 28, 29, 30, 32 | algrp1 15125 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
34 | 26, 33 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘))) |
35 | 27, 28, 29, 30, 32 | algrf 15124 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑆 → 𝑅:ℕ0⟶𝑆) |
36 | 35 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝑅‘𝑘) ∈ 𝑆) |
37 | 26, 36 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘𝑘) ∈ 𝑆) |
38 | | algcvga.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧))) |
39 | 31, 28, 2, 38, 1 | algcvga 15130 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑆 → (𝑘 ∈ (ℤ≥‘𝑁) → (𝐶‘(𝑅‘𝑘)) = 0)) |
40 | 39 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐶‘(𝑅‘𝑘)) = 0) |
41 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → (𝐶‘𝑧) = (𝐶‘(𝑅‘𝑘))) |
42 | 41 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑅‘𝑘) → ((𝐶‘𝑧) = 0 ↔ (𝐶‘(𝑅‘𝑘)) = 0)) |
43 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → (𝐹‘𝑧) = (𝐹‘(𝑅‘𝑘))) |
44 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑅‘𝑘) → 𝑧 = (𝑅‘𝑘)) |
45 | 43, 44 | eqeq12d 2625 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑅‘𝑘) → ((𝐹‘𝑧) = 𝑧 ↔ (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘))) |
46 | 42, 45 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑅‘𝑘) → (((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧) ↔ ((𝐶‘(𝑅‘𝑘)) = 0 → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘)))) |
47 | | algfx.6 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → ((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧)) |
48 | 46, 47 | vtoclga 3245 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑘) ∈ 𝑆 → ((𝐶‘(𝑅‘𝑘)) = 0 → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘))) |
49 | 37, 40, 48 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘(𝑅‘𝑘)) = (𝑅‘𝑘)) |
50 | 34, 49 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑘)) |
51 | 50 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → ((𝑅‘(𝑘 + 1)) = (𝑅‘𝑁) ↔ (𝑅‘𝑘) = (𝑅‘𝑁))) |
52 | 51 | biimprd 237 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁))) |
53 | 52 | expcom 450 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
54 | 53 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘𝑁)) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
55 | 24, 54 | sylbir 224 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → (𝐴 ∈ 𝑆 → ((𝑅‘𝑘) = (𝑅‘𝑁) → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
56 | 55 | a2d 29 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → ((𝐴 ∈ 𝑆 → (𝑅‘𝑘) = (𝑅‘𝑁)) → (𝐴 ∈ 𝑆 → (𝑅‘(𝑘 + 1)) = (𝑅‘𝑁)))) |
57 | 11, 14, 17, 20, 22, 56 | uzind3 11347 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧}) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁))) |
58 | 8, 57 | sylbi 206 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈
(ℤ≥‘𝑁)) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁))) |
59 | 58 | ex 449 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝐾 ∈
(ℤ≥‘𝑁) → (𝐴 ∈ 𝑆 → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
60 | 59 | com3r 85 |
. 2
⊢ (𝐴 ∈ 𝑆 → (𝑁 ∈ ℤ → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁)))) |
61 | 5, 60 | mpd 15 |
1
⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁))) |