Step | Hyp | Ref
| Expression |
1 | | isercoll.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | uzssz 12345 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
3 | 1, 2 | eqsstri 3911 |
. . . . . . . . 9
⊢ 𝑍 ⊆
ℤ |
4 | | isercoll.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶𝑍) |
5 | 4 | ffvelrnda 6861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ 𝑍) |
6 | 3, 5 | sseldi 3875 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℤ) |
7 | | nnz 12085 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
8 | 7 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℤ) |
9 | | fzfid 13432 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (𝑀...𝑚) ∈ Fin) |
10 | | ffun 6507 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺) |
11 | | funimacnv 6420 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝐺 → (𝐺 “ (◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺)) |
12 | 4, 10, 11 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 “ (◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺)) |
13 | | inss1 4119 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀...𝑚) ∩ ran 𝐺) ⊆ (𝑀...𝑚) |
14 | 12, 13 | eqsstrdi 3931 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺 “ (◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚)) |
15 | 14 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚)) |
16 | 9, 15 | ssfid 8819 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑚))) ∈ Fin) |
17 | | hashcl 13809 |
. . . . . . . . . . . 12
⊢ ((𝐺 “ (◡𝐺 “ (𝑀...𝑚))) ∈ Fin → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) ∈
ℕ0) |
18 | | nn0z 12086 |
. . . . . . . . . . . 12
⊢
((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ0 →
(♯‘(𝐺 “
(◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ) |
20 | | ssid 3899 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℕ
⊆ ℕ |
21 | | isercoll.m |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ ℤ) |
22 | | isercoll.i |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
23 | 1, 21, 4, 22 | isercolllem1 15114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℕ ⊆ ℕ)
→ (𝐺 ↾ ℕ)
Isom < , < (ℕ, (𝐺 “ ℕ))) |
24 | 20, 23 | mpan2 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “
ℕ))) |
25 | | ffn 6504 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ) |
26 | | fnresdm 6455 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺) |
27 | | isoeq1 7083 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “ ℕ)) ↔
𝐺 Isom < , <
(ℕ, (𝐺 “
ℕ)))) |
28 | 4, 25, 26, 27 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ,
(𝐺 “ ℕ)) ↔
𝐺 Isom < , <
(ℕ, (𝐺 “
ℕ)))) |
29 | 24, 28 | mpbid 235 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺 Isom < , < (ℕ, (𝐺 “
ℕ))) |
30 | | isof1o 7089 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 Isom < , < (ℕ,
(𝐺 “ ℕ)) →
𝐺:ℕ–1-1-onto→(𝐺 “ ℕ)) |
31 | | f1ocnv 6630 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → ◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ) |
32 | | f1ofun 6620 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun ◡𝐺) |
33 | 29, 30, 31, 32 | 4syl 19 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Fun ◡𝐺) |
34 | | df-f1 6344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:ℕ–1-1→𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun ◡𝐺)) |
35 | 4, 33, 34 | sylanbrc 586 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:ℕ–1-1→𝑍) |
36 | 35 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → 𝐺:ℕ–1-1→𝑍) |
37 | | fz1ssnn 13029 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑛) ⊆
ℕ |
38 | | ovex 7203 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑛) ∈
V |
39 | 38 | f1imaen 8617 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑛) ⊆ ℕ) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) |
40 | 36, 37, 39 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) |
41 | | fzfid 13432 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (1...𝑛) ∈ Fin) |
42 | | enfii 8784 |
. . . . . . . . . . . . . . . 16
⊢
(((1...𝑛) ∈ Fin
∧ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) → (𝐺 “ (1...𝑛)) ∈ Fin) |
43 | 41, 40, 42 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ∈ Fin) |
44 | | hashen 13799 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (1...𝑛) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛))) |
45 | 43, 41, 44 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → ((♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛))) |
46 | 40, 45 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛))) |
47 | | nnnn0 11983 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
48 | 47 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℕ0) |
49 | | hashfz1 13798 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ (♯‘(1...𝑛)) = 𝑛) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (♯‘(1...𝑛)) = 𝑛) |
51 | 46, 50 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = 𝑛) |
52 | | elfznn 13027 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ∈ ℕ) |
53 | 52 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℕ) |
54 | | zssre 12069 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℤ
⊆ ℝ |
55 | 3, 54 | sstri 3886 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑍 ⊆
ℝ |
56 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → 𝐺:ℕ⟶𝑍) |
57 | | ffvelrn 6859 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺:ℕ⟶𝑍 ∧ 𝑦 ∈ ℕ) → (𝐺‘𝑦) ∈ 𝑍) |
58 | 56, 52, 57 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ 𝑍) |
59 | 55, 58 | sseldi 3875 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ ℝ) |
60 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ 𝑍) |
61 | 55, 60 | sseldi 3875 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ ℝ) |
62 | | eluzelz 12334 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈
(ℤ≥‘(𝐺‘𝑛)) → 𝑚 ∈ ℤ) |
63 | 62 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℤ) |
64 | 63 | zred 12168 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℝ) |
65 | | elfzle2 13002 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ≤ 𝑛) |
66 | 65 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ≤ 𝑛) |
67 | 29 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Isom < , < (ℕ, (𝐺 “
ℕ))) |
68 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℕ) |
69 | | isorel 7092 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 Isom < , < (ℕ,
(𝐺 “ ℕ)) ∧
(𝑛 ∈ ℕ ∧
𝑦 ∈ ℕ)) →
(𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦))) |
70 | 67, 68, 53, 69 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦))) |
71 | 70 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (¬ 𝑛 < 𝑦 ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦))) |
72 | 53 | nnred 11731 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℝ) |
73 | 68 | nnred 11731 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℝ) |
74 | 72, 73 | lenltd 10864 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑦)) |
75 | 59, 61 | lenltd 10864 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ≤ (𝐺‘𝑛) ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦))) |
76 | 71, 74, 75 | 3bitr4d 314 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ (𝐺‘𝑦) ≤ (𝐺‘𝑛))) |
77 | 66, 76 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ (𝐺‘𝑛)) |
78 | | eluzle 12337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈
(ℤ≥‘(𝐺‘𝑛)) → (𝐺‘𝑛) ≤ 𝑚) |
79 | 78 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ≤ 𝑚) |
80 | 59, 61, 64, 77, 79 | letrd 10875 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ 𝑚) |
81 | 58, 1 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (ℤ≥‘𝑀)) |
82 | | elfz5 12990 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺‘𝑦) ∈ (ℤ≥‘𝑀) ∧ 𝑚 ∈ ℤ) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚)) |
83 | 81, 63, 82 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚)) |
84 | 80, 83 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (𝑀...𝑚)) |
85 | 56 | ffnd 6505 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → 𝐺 Fn ℕ) |
86 | 85 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Fn ℕ) |
87 | | elpreima 6835 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 Fn ℕ → (𝑦 ∈ (◡𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺‘𝑦) ∈ (𝑀...𝑚)))) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ∈ (◡𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺‘𝑦) ∈ (𝑀...𝑚)))) |
89 | 53, 84, 88 | mpbir2and 713 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ (◡𝐺 “ (𝑀...𝑚))) |
90 | 89 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (𝑦 ∈ (1...𝑛) → 𝑦 ∈ (◡𝐺 “ (𝑀...𝑚)))) |
91 | 90 | ssrdv 3883 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (1...𝑛) ⊆ (◡𝐺 “ (𝑀...𝑚))) |
92 | | imass2 5939 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑛) ⊆
(◡𝐺 “ (𝑀...𝑚)) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) |
94 | | ssdomg 8601 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 “ (◡𝐺 “ (𝑀...𝑚))) ∈ Fin → ((𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑚))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) |
95 | 16, 93, 94 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) |
96 | | hashdom 13832 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (𝐺 “ (◡𝐺 “ (𝑀...𝑚))) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) |
97 | 43, 16, 96 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → ((♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) |
98 | 95, 97 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) |
99 | 51, 98 | eqbrtrrd 5054 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → 𝑛 ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) |
100 | | eluz2 12330 |
. . . . . . . . . . 11
⊢
((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑚)))) ∈
(ℤ≥‘𝑛) ↔ (𝑛 ∈ ℤ ∧ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ ∧ 𝑛 ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))))) |
101 | 8, 19, 99, 100 | syl3anbrc 1344 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) ∈
(ℤ≥‘𝑛)) |
102 | | fveq2 6674 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))))) |
103 | 102 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ (𝑘 = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ)) |
104 | 102 | fvoveq1d 7192 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) → (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴))) |
105 | 104 | breq1d 5040 |
. . . . . . . . . . . 12
⊢ (𝑘 = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) → ((abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) |
106 | 103, 105 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑘 = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) → (((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
107 | 106 | rspcv 3521 |
. . . . . . . . . 10
⊢
((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑚)))) ∈
(ℤ≥‘𝑛) → (∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
108 | 101, 107 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))) → (∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
109 | 108 | ralrimdva 3101 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∀𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
110 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑗 = (𝐺‘𝑛) → (ℤ≥‘𝑗) =
(ℤ≥‘(𝐺‘𝑛))) |
111 | 110 | raleqdv 3316 |
. . . . . . . . 9
⊢ (𝑗 = (𝐺‘𝑛) → (∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
112 | 111 | rspcev 3526 |
. . . . . . . 8
⊢ (((𝐺‘𝑛) ∈ ℤ ∧ ∀𝑚 ∈
(ℤ≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) |
113 | 6, 109, 112 | syl6an 684 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
114 | 113 | rexlimdva 3194 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
115 | | 1nn 11727 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
116 | | ffvelrn 6859 |
. . . . . . . . 9
⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) →
(𝐺‘1) ∈ 𝑍) |
117 | 4, 115, 116 | sylancl 589 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘1) ∈ 𝑍) |
118 | 117, 1 | eleqtrdi 2843 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘1) ∈
(ℤ≥‘𝑀)) |
119 | | eluzelz 12334 |
. . . . . . 7
⊢ ((𝐺‘1) ∈
(ℤ≥‘𝑀) → (𝐺‘1) ∈ ℤ) |
120 | | eqid 2738 |
. . . . . . . 8
⊢
(ℤ≥‘(𝐺‘1)) =
(ℤ≥‘(𝐺‘1)) |
121 | 120 | rexuz3 14798 |
. . . . . . 7
⊢ ((𝐺‘1) ∈ ℤ →
(∃𝑗 ∈
(ℤ≥‘(𝐺‘1))∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
122 | 118, 119,
121 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (∃𝑗 ∈ (ℤ≥‘(𝐺‘1))∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
123 | 114, 122 | sylibrd 262 |
. . . . 5
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ (ℤ≥‘(𝐺‘1))∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
124 | | fzfid 13432 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) → (𝑀...𝑗) ∈ Fin) |
125 | | funimacnv 6420 |
. . . . . . . . . . . 12
⊢ (Fun
𝐺 → (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺)) |
126 | 4, 10, 125 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺)) |
127 | | inss1 4119 |
. . . . . . . . . . 11
⊢ ((𝑀...𝑗) ∩ ran 𝐺) ⊆ (𝑀...𝑗) |
128 | 126, 127 | eqsstrdi 3931 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗)) |
129 | 128 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗)) |
130 | 124, 129 | ssfid 8819 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) ∈ Fin) |
131 | | hashcl 13809 |
. . . . . . . 8
⊢ ((𝐺 “ (◡𝐺 “ (𝑀...𝑗))) ∈ Fin → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) ∈
ℕ0) |
132 | | nn0p1nn 12015 |
. . . . . . . 8
⊢
((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ0 →
((♯‘(𝐺 “
(◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ) |
133 | 130, 131,
132 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) →
((♯‘(𝐺 “
(◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ) |
134 | | eluzle 12337 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1)) → ((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘) |
135 | 134 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘) |
136 | 130 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) ∈ Fin) |
137 | | nn0z 12086 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ0 →
(♯‘(𝐺 “
(◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ) |
138 | 136, 131,
137 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ) |
139 | | eluzelz 12334 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1)) → 𝑘 ∈ ℤ) |
140 | 139 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℤ) |
141 | | zltp1le 12113 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ ∧ 𝑘 ∈ ℤ) →
((♯‘(𝐺 “
(◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)) |
142 | 138, 140,
141 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)) |
143 | 135, 142 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) < 𝑘) |
144 | | nn0re 11985 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ0 →
(♯‘(𝐺 “
(◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ) |
145 | 130, 131,
144 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) →
(♯‘(𝐺 “
(◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ) |
146 | 145 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ) |
147 | | eluznn 12400 |
. . . . . . . . . . . . . . . 16
⊢
((((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ) |
148 | 133, 147 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ) |
149 | 148 | nnred 11731 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℝ) |
150 | 146, 149 | ltnled 10865 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ¬ 𝑘 ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))))) |
151 | 143, 150 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑘 ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗))))) |
152 | | fzss2 13038 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘(𝐺‘𝑘)) → (𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗)) |
153 | | imass2 5939 |
. . . . . . . . . . . . . 14
⊢ ((𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗) → (◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (◡𝐺 “ (𝑀...𝑗))) |
154 | | imass2 5939 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (◡𝐺 “ (𝑀...𝑗)) → (𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) |
155 | 152, 153,
154 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘(𝐺‘𝑘)) → (𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) |
156 | | ssdomg 8601 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 “ (◡𝐺 “ (𝑀...𝑗))) ∈ Fin → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))))) |
157 | 136, 156 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))))) |
158 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ⟶𝑍) |
159 | 158 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ 𝑍) |
160 | 159, 1 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ (ℤ≥‘𝑀)) |
161 | 158, 148 | ffvelrnd 6862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ 𝑍) |
162 | 3, 161 | sseldi 3875 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ ℤ) |
163 | 162 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑘) ∈ ℤ) |
164 | | elfz5 12990 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺‘𝑥) ∈ (ℤ≥‘𝑀) ∧ (𝐺‘𝑘) ∈ ℤ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘))) |
165 | 160, 163,
164 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘))) |
166 | 29 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ, (𝐺 “
ℕ))) |
167 | | nnssre 11720 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℕ
⊆ ℝ |
168 | | ressxr 10763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℝ
⊆ ℝ* |
169 | 167, 168 | sstri 3886 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ
⊆ ℝ* |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆
ℝ*) |
171 | | imassrn 5914 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 “ ℕ) ⊆ ran
𝐺 |
172 | 158 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍) |
173 | 172 | frnd 6512 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ 𝑍) |
174 | 173, 55 | sstrdi 3889 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ ℝ) |
175 | 171, 174 | sstrid 3888 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆
ℝ) |
176 | 175, 168 | sstrdi 3889 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆
ℝ*) |
177 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ) |
178 | 148 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑘 ∈ ℕ) |
179 | | leisorel 13912 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 Isom < , < (ℕ,
(𝐺 “ ℕ)) ∧
(ℕ ⊆ ℝ* ∧ (𝐺 “ ℕ) ⊆
ℝ*) ∧ (𝑥 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘))) |
180 | 166, 170,
176, 177, 178, 179 | syl122anc 1380 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘))) |
181 | 165, 180 | bitr4d 285 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ 𝑥 ≤ 𝑘)) |
182 | 181 | pm5.32da 582 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘))) |
183 | | elpreima 6835 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 Fn ℕ → (𝑥 ∈ (◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘))))) |
184 | 158, 25, 183 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘))))) |
185 | | fznn 13066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℤ → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘))) |
186 | 140, 185 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘))) |
187 | 182, 184,
186 | 3bitr4d 314 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ 𝑥 ∈ (1...𝑘))) |
188 | 187 | eqrdv 2736 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (◡𝐺 “ (𝑀...(𝐺‘𝑘))) = (1...𝑘)) |
189 | 188 | imaeq2d 5903 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))) = (𝐺 “ (1...𝑘))) |
190 | 189 | sseq1d 3908 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) ↔ (𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))))) |
191 | 35 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ–1-1→𝑍) |
192 | | fz1ssnn 13029 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1...𝑘) ⊆
ℕ |
193 | | ovex 7203 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑘) ∈
V |
194 | 193 | f1imaen 8617 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑘) ⊆ ℕ) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) |
195 | 191, 192,
194 | sylancl 589 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) |
196 | | fzfid 13432 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (1...𝑘) ∈ Fin) |
197 | | enfii 8784 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1...𝑘) ∈ Fin
∧ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) → (𝐺 “ (1...𝑘)) ∈ Fin) |
198 | 196, 195,
197 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ∈ Fin) |
199 | | hashen 13799 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (1...𝑘) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘))) |
200 | 198, 196,
199 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘))) |
201 | 195, 200 | mpbird 260 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘))) |
202 | | nnnn0 11983 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
203 | | hashfz1 13798 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ (♯‘(1...𝑘)) = 𝑘) |
204 | 148, 202,
203 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(1...𝑘)) = 𝑘) |
205 | 201, 204 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = 𝑘) |
206 | 205 | breq1d 5040 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) ↔ 𝑘 ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))))) |
207 | | hashdom 13832 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))))) |
208 | 198, 136,
207 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))))) |
209 | 206, 208 | bitr3d 284 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑘 ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))))) |
210 | 157, 190,
209 | 3imtr4d 297 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (◡𝐺 “ (𝑀...𝑗))) → 𝑘 ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))))) |
211 | 155, 210 | syl5 34 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ≥‘(𝐺‘𝑘)) → 𝑘 ≤ (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))))) |
212 | 151, 211 | mtod 201 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑗 ∈ (ℤ≥‘(𝐺‘𝑘))) |
213 | | eluzelz 12334 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘(𝐺‘1)) → 𝑗 ∈ ℤ) |
214 | 213 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑗 ∈ ℤ) |
215 | | uztric 12348 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑘) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ≥‘𝑗))) |
216 | 162, 214,
215 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ≥‘𝑗))) |
217 | 216 | ord 863 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (¬ 𝑗 ∈ (ℤ≥‘(𝐺‘𝑘)) → (𝐺‘𝑘) ∈ (ℤ≥‘𝑗))) |
218 | 212, 217 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ (ℤ≥‘𝑗)) |
219 | | oveq2 7178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝐺‘𝑘) → (𝑀...𝑚) = (𝑀...(𝐺‘𝑘))) |
220 | 219 | imaeq2d 5903 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝐺‘𝑘) → (◡𝐺 “ (𝑀...𝑚)) = (◡𝐺 “ (𝑀...(𝐺‘𝑘)))) |
221 | 220 | imaeq2d 5903 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝐺‘𝑘) → (𝐺 “ (◡𝐺 “ (𝑀...𝑚))) = (𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘))))) |
222 | 221 | fveq2d 6678 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝐺‘𝑘) → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))) = (♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) |
223 | 222 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝐺‘𝑘) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘))))))) |
224 | 223 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝐺‘𝑘) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ)) |
225 | 223 | fvoveq1d 7192 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝐺‘𝑘) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴))) |
226 | 225 | breq1d 5040 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝐺‘𝑘) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)) |
227 | 224, 226 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝐺‘𝑘) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧
(abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥))) |
228 | 227 | rspcv 3521 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑘) ∈ (ℤ≥‘𝑗) → (∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧
(abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥))) |
229 | 218, 228 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧
(abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥))) |
230 | 189 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = (♯‘(𝐺 “ (1...𝑘)))) |
231 | 230, 205 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = 𝑘) |
232 | 231 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) = (seq1( + , 𝐻)‘𝑘)) |
233 | 232 | eleq1d 2817 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘𝑘) ∈ ℂ)) |
234 | 232 | fvoveq1d 7192 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (abs‘((seq1( + ,
𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴))) |
235 | 234 | breq1d 5040 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((abs‘((seq1( + ,
𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) |
236 | 233, 235 | anbi12d 634 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧
(abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥))) |
237 | 229, 236 | sylibd 242 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) ∧ 𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥))) |
238 | 237 | ralrimdva 3101 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) →
(∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∀𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥))) |
239 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑛 = ((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1) →
(ℤ≥‘𝑛) =
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))) |
240 | 239 | raleqdv 3316 |
. . . . . . . 8
⊢ (𝑛 = ((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1) → (∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥))) |
241 | 240 | rspcev 3526 |
. . . . . . 7
⊢
((((♯‘(𝐺
“ (◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘((♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥)) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥)) |
242 | 133, 238,
241 | syl6an 684 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝐺‘1))) →
(∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥))) |
243 | 242 | rexlimdva 3194 |
. . . . 5
⊢ (𝜑 → (∃𝑗 ∈ (ℤ≥‘(𝐺‘1))∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥))) |
244 | 123, 243 | impbid 215 |
. . . 4
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ (ℤ≥‘(𝐺‘1))∀𝑚 ∈
(ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
245 | 244 | ralbidv 3109 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑛 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘(𝐺‘1))∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))) |
246 | 245 | anbi2d 632 |
. 2
⊢ (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑛 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥)) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘(𝐺‘1))∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))) |
247 | | nnuz 12363 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
248 | | 1zzd 12094 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
249 | | seqex 13462 |
. . . 4
⊢ seq1( + ,
𝐻) ∈
V |
250 | 249 | a1i 11 |
. . 3
⊢ (𝜑 → seq1( + , 𝐻) ∈ V) |
251 | | eqidd 2739 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘𝑘)) |
252 | 247, 248,
250, 251 | clim2 14951 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑛 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + ,
𝐻)‘𝑘) − 𝐴)) < 𝑥)))) |
253 | 118, 119 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺‘1) ∈ ℤ) |
254 | | seqex 13462 |
. . . 4
⊢ seq𝑀( + , 𝐹) ∈ V |
255 | 254 | a1i 11 |
. . 3
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ V) |
256 | | isercoll.0 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0) |
257 | | isercoll.f |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℂ) |
258 | | isercoll.h |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
259 | 1, 21, 4, 22, 256, 257, 258 | isercolllem3 15116 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑚) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚)))))) |
260 | 120, 253,
255, 259 | clim2 14951 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘(𝐺‘1))∀𝑚 ∈ (ℤ≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1(
+ , 𝐻)‘(♯‘(𝐺 “ (◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))) |
261 | 246, 252,
260 | 3bitr4d 314 |
1
⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ seq𝑀( + , 𝐹) ⇝ 𝐴)) |