| Step | Hyp | Ref
| Expression |
| 1 | | risset 3233 |
. . . . 5
⊢ (𝐴 ∈ ℕ0
↔ ∃𝑏 ∈
ℕ0 𝑏 =
𝐴) |
| 2 | 1 | rabbii 3442 |
. . . 4
⊢ {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ 𝐴 ∈
ℕ0} = {𝑡
∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 𝑏 = 𝐴} |
| 3 | 2 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∈ ℕ0} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 𝑏 =
𝐴}) |
| 4 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑡(ℕ0 ↑m
(1...𝑁)) |
| 5 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑎(ℕ0 ↑m
(1...𝑁)) |
| 6 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑎∃𝑏 ∈ ℕ0
𝑏 = 𝐴 |
| 7 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑡ℕ0 |
| 8 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑡⦋𝑎 / 𝑡⦌𝐴 |
| 9 | 8 | nfeq2 2923 |
. . . . 5
⊢
Ⅎ𝑡 𝑏 = ⦋𝑎 / 𝑡⦌𝐴 |
| 10 | 7, 9 | nfrexw 3313 |
. . . 4
⊢
Ⅎ𝑡∃𝑏 ∈ ℕ0
𝑏 = ⦋𝑎 / 𝑡⦌𝐴 |
| 11 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑡 = 𝑎 → 𝐴 = ⦋𝑎 / 𝑡⦌𝐴) |
| 12 | 11 | eqeq2d 2748 |
. . . . 5
⊢ (𝑡 = 𝑎 → (𝑏 = 𝐴 ↔ 𝑏 = ⦋𝑎 / 𝑡⦌𝐴)) |
| 13 | 12 | rexbidv 3179 |
. . . 4
⊢ (𝑡 = 𝑎 → (∃𝑏 ∈ ℕ0 𝑏 = 𝐴 ↔ ∃𝑏 ∈ ℕ0 𝑏 = ⦋𝑎 / 𝑡⦌𝐴)) |
| 14 | 4, 5, 6, 10, 13 | cbvrabw 3473 |
. . 3
⊢ {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 𝑏 =
𝐴} = {𝑎 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 𝑏 =
⦋𝑎 / 𝑡⦌𝐴} |
| 15 | 3, 14 | eqtrdi 2793 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∈ ℕ0} = {𝑎 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 𝑏 =
⦋𝑎 / 𝑡⦌𝐴}) |
| 16 | | peano2nn0 12566 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
| 17 | 16 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑁 + 1) ∈
ℕ0) |
| 18 | | ovex 7464 |
. . . . 5
⊢
(1...(𝑁 + 1)) ∈
V |
| 19 | | nn0p1nn 12565 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
| 20 | | elfz1end 13594 |
. . . . . . 7
⊢ ((𝑁 + 1) ∈ ℕ ↔
(𝑁 + 1) ∈ (1...(𝑁 + 1))) |
| 21 | 19, 20 | sylib 218 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(1...(𝑁 +
1))) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑁 + 1) ∈
(1...(𝑁 +
1))) |
| 23 | | mzpproj 42748 |
. . . . 5
⊢
(((1...(𝑁 + 1))
∈ V ∧ (𝑁 + 1)
∈ (1...(𝑁 + 1)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 24 | 18, 22, 23 | sylancr 587 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 25 | | eqid 2737 |
. . . . 5
⊢ (𝑁 + 1) = (𝑁 + 1) |
| 26 | 25 | rabdiophlem2 42813 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 27 | | eqrabdioph 42788 |
. . . 4
⊢ (((𝑁 + 1) ∈ ℕ0
∧ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) ∈ (mzPoly‘(1...(𝑁 + 1)))) → {𝑐 ∈ (ℕ0
↑m (1...(𝑁
+ 1))) ∣ (𝑐‘(𝑁 + 1)) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴} ∈ (Dioph‘(𝑁 + 1))) |
| 28 | 17, 24, 26, 27 | syl3anc 1373 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑐 ∈
(ℕ0 ↑m (1...(𝑁 + 1))) ∣ (𝑐‘(𝑁 + 1)) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴} ∈ (Dioph‘(𝑁 + 1))) |
| 29 | | eqeq1 2741 |
. . . 4
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → (𝑏 = ⦋𝑎 / 𝑡⦌𝐴 ↔ (𝑐‘(𝑁 + 1)) = ⦋𝑎 / 𝑡⦌𝐴)) |
| 30 | | csbeq1 3902 |
. . . . 5
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ⦋𝑎 / 𝑡⦌𝐴 = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) |
| 31 | 30 | eqeq2d 2748 |
. . . 4
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ((𝑐‘(𝑁 + 1)) = ⦋𝑎 / 𝑡⦌𝐴 ↔ (𝑐‘(𝑁 + 1)) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) |
| 32 | 25, 29, 31 | rexrabdioph 42805 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ {𝑐 ∈
(ℕ0 ↑m (1...(𝑁 + 1))) ∣ (𝑐‘(𝑁 + 1)) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴} ∈ (Dioph‘(𝑁 + 1))) → {𝑎 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 𝑏 =
⦋𝑎 / 𝑡⦌𝐴} ∈ (Dioph‘𝑁)) |
| 33 | 28, 32 | syldan 591 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑎 ∈
(ℕ0 ↑m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 𝑏 = ⦋𝑎 / 𝑡⦌𝐴} ∈ (Dioph‘𝑁)) |
| 34 | 15, 33 | eqeltrd 2841 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∈ ℕ0} ∈
(Dioph‘𝑁)) |