Proof of Theorem eqrabdioph
| Step | Hyp | Ref
| Expression |
| 1 | | nfmpt1 5250 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴) |
| 2 | 1 | nfel1 2922 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)) |
| 3 | | nfmpt1 5250 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐵) |
| 4 | 3 | nfel1 2922 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)) |
| 5 | 2, 4 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑡((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁))) |
| 6 | | mzpf 42747 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
→ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴):(ℤ
↑m (1...𝑁))⟶ℤ) |
| 7 | 6 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → (𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴):(ℤ ↑m
(1...𝑁))⟶ℤ) |
| 8 | | zex 12622 |
. . . . . . . . . . . . 13
⊢ ℤ
∈ V |
| 9 | | nn0ssz 12636 |
. . . . . . . . . . . . 13
⊢
ℕ0 ⊆ ℤ |
| 10 | | mapss 8929 |
. . . . . . . . . . . . 13
⊢ ((ℤ
∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0
↑m (1...𝑁))
⊆ (ℤ ↑m (1...𝑁))) |
| 11 | 8, 9, 10 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(ℕ0 ↑m (1...𝑁)) ⊆ (ℤ ↑m
(1...𝑁)) |
| 12 | 11 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (ℕ0
↑m (1...𝑁))
→ 𝑡 ∈ (ℤ
↑m (1...𝑁))) |
| 13 | 12 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝑡 ∈ (ℤ ↑m
(1...𝑁))) |
| 14 | | mptfcl 42731 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴):(ℤ
↑m (1...𝑁))⟶ℤ → (𝑡 ∈ (ℤ ↑m
(1...𝑁)) → 𝐴 ∈
ℤ)) |
| 15 | 7, 13, 14 | sylc 65 |
. . . . . . . . 9
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝐴 ∈ ℤ) |
| 16 | 15 | zcnd 12723 |
. . . . . . . 8
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝐴 ∈ ℂ) |
| 17 | | mzpf 42747 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁))
→ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵):(ℤ
↑m (1...𝑁))⟶ℤ) |
| 18 | 17 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → (𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐵):(ℤ ↑m
(1...𝑁))⟶ℤ) |
| 19 | | mptfcl 42731 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵):(ℤ
↑m (1...𝑁))⟶ℤ → (𝑡 ∈ (ℤ ↑m
(1...𝑁)) → 𝐵 ∈
ℤ)) |
| 20 | 18, 13, 19 | sylc 65 |
. . . . . . . . 9
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝐵 ∈ ℤ) |
| 21 | 20 | zcnd 12723 |
. . . . . . . 8
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝐵 ∈ ℂ) |
| 22 | 16, 21 | subeq0ad 11630 |
. . . . . . 7
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) |
| 23 | 22 | bicomd 223 |
. . . . . 6
⊢ ((((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → (𝐴 = 𝐵 ↔ (𝐴 − 𝐵) = 0)) |
| 24 | 23 | ex 412 |
. . . . 5
⊢ (((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑡 ∈
(ℕ0 ↑m (1...𝑁)) → (𝐴 = 𝐵 ↔ (𝐴 − 𝐵) = 0))) |
| 25 | 5, 24 | ralrimi 3257 |
. . . 4
⊢ (((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ ∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))(𝐴 = 𝐵 ↔ (𝐴 − 𝐵) = 0)) |
| 26 | | rabbi 3467 |
. . . 4
⊢
(∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))(𝐴 = 𝐵 ↔ (𝐴 − 𝐵) = 0) ↔ {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ 𝐴 = 𝐵} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ (𝐴 − 𝐵) = 0}) |
| 27 | 25, 26 | sylib 218 |
. . 3
⊢ (((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 𝐵} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ (𝐴 − 𝐵) = 0}) |
| 28 | 27 | 3adant1 1131 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 𝐵} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ (𝐴 − 𝐵) = 0}) |
| 29 | | simp1 1137 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ 𝑁 ∈
ℕ0) |
| 30 | | mzpsubmpt 42754 |
. . . 4
⊢ (((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ (𝐴 − 𝐵)) ∈
(mzPoly‘(1...𝑁))) |
| 31 | 30 | 3adant1 1131 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ (𝐴 − 𝐵)) ∈
(mzPoly‘(1...𝑁))) |
| 32 | | eq0rabdioph 42787 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ (𝐴 − 𝐵)) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ (𝐴 − 𝐵) = 0} ∈ (Dioph‘𝑁)) |
| 33 | 29, 31, 32 | syl2anc 584 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ (𝐴 − 𝐵) = 0} ∈ (Dioph‘𝑁)) |
| 34 | 28, 33 | eqeltrd 2841 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 𝐵} ∈ (Dioph‘𝑁)) |