Proof of Theorem eqrabdioph
Step | Hyp | Ref
| Expression |
1 | | nfmpt1 5025 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴) |
2 | 1 | nfel1 2947 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) |
3 | | nfmpt1 5025 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) |
4 | 3 | nfel1 2947 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁)) |
5 | 2, 4 | nfan 1862 |
. . . . 5
⊢
Ⅎ𝑡((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁))) |
6 | | mzpf 38725 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴):(ℤ
↑𝑚 (1...𝑁))⟶ℤ) |
7 | 6 | ad2antrr 713 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴):(ℤ
↑𝑚 (1...𝑁))⟶ℤ) |
8 | | zex 11802 |
. . . . . . . . . . . . 13
⊢ ℤ
∈ V |
9 | | nn0ssz 11816 |
. . . . . . . . . . . . 13
⊢
ℕ0 ⊆ ℤ |
10 | | mapss 8251 |
. . . . . . . . . . . . 13
⊢ ((ℤ
∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0
↑𝑚 (1...𝑁)) ⊆ (ℤ
↑𝑚 (1...𝑁))) |
11 | 8, 9, 10 | mp2an 679 |
. . . . . . . . . . . 12
⊢
(ℕ0 ↑𝑚 (1...𝑁)) ⊆ (ℤ
↑𝑚 (1...𝑁)) |
12 | 11 | sseli 3855 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) → 𝑡 ∈ (ℤ ↑𝑚
(1...𝑁))) |
13 | 12 | adantl 474 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → 𝑡 ∈ (ℤ ↑𝑚
(1...𝑁))) |
14 | | mptfcl 38709 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴):(ℤ ↑𝑚
(1...𝑁))⟶ℤ
→ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) → 𝐴 ∈ ℤ)) |
15 | 7, 13, 14 | sylc 65 |
. . . . . . . . 9
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → 𝐴 ∈ ℤ) |
16 | 15 | zcnd 11901 |
. . . . . . . 8
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → 𝐴 ∈ ℂ) |
17 | | mzpf 38725 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁)) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵):(ℤ
↑𝑚 (1...𝑁))⟶ℤ) |
18 | 17 | ad2antlr 714 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵):(ℤ
↑𝑚 (1...𝑁))⟶ℤ) |
19 | | mptfcl 38709 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐵):(ℤ ↑𝑚
(1...𝑁))⟶ℤ
→ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) → 𝐵 ∈ ℤ)) |
20 | 18, 13, 19 | sylc 65 |
. . . . . . . . 9
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → 𝐵 ∈ ℤ) |
21 | 20 | zcnd 11901 |
. . . . . . . 8
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → 𝐵 ∈ ℂ) |
22 | 16, 21 | subeq0ad 10808 |
. . . . . . 7
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) |
23 | 22 | bicomd 215 |
. . . . . 6
⊢ ((((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))) → (𝐴 = 𝐵 ↔ (𝐴 − 𝐵) = 0)) |
24 | 23 | ex 405 |
. . . . 5
⊢ (((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) → (𝐴 = 𝐵 ↔ (𝐴 − 𝐵) = 0))) |
25 | 5, 24 | ralrimi 3167 |
. . . 4
⊢ (((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ ∀𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝐴 = 𝐵 ↔ (𝐴 − 𝐵) = 0)) |
26 | | rabbi 3323 |
. . . 4
⊢
(∀𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝐴 = 𝐵 ↔ (𝐴 − 𝐵) = 0) ↔ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 = 𝐵} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ (𝐴 − 𝐵) = 0}) |
27 | 25, 26 | sylib 210 |
. . 3
⊢ (((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 = 𝐵} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ (𝐴 − 𝐵) = 0}) |
28 | 27 | 3adant1 1110 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 = 𝐵} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ (𝐴 − 𝐵) = 0}) |
29 | | simp1 1116 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ 𝑁 ∈
ℕ0) |
30 | | mzpsubmpt 38732 |
. . . 4
⊢ (((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘(1...𝑁))) |
31 | 30 | 3adant1 1110 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘(1...𝑁))) |
32 | | eq0rabdioph 38766 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ (𝐴 − 𝐵) = 0} ∈ (Dioph‘𝑁)) |
33 | 29, 31, 32 | syl2anc 576 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ (𝐴 − 𝐵) = 0} ∈ (Dioph‘𝑁)) |
34 | 28, 33 | eqeltrd 2867 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 = 𝐵} ∈ (Dioph‘𝑁)) |