Metamath Proof Explorer

Theorem eqrabdioph

Description: Diophantine set builder for equality of polynomial expressions. Note that the two expressions need not be nonnegative; only variables are so constrained. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion eqrabdioph ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 𝐵 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 )
2 1 nfel1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) )
3 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 )
4 3 nfel1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) )
5 2 4 nfan ⊢ Ⅎ 𝑡 ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
6 mzpf ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
7 6 ad2antrr ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
8 zex ⊢ ℤ ∈ V
9 nn0ssz ⊢ ℕ0 ⊆ ℤ
10 mapss ⊢ ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
11 8 9 10 mp2an ⊢ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℤ ↑m ( 1 ... 𝑁 ) )
12 11 sseli ⊢ ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
13 12 adantl ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
14 mptfcl ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) → 𝐴 ∈ ℤ ) )
15 7 13 14 sylc ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝐴 ∈ ℤ )
16 15 zcnd ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝐴 ∈ ℂ )
17 mzpf ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
18 17 ad2antlr ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
19 mptfcl ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) → 𝐵 ∈ ℤ ) )
20 18 13 19 sylc ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝐵 ∈ ℤ )
21 20 zcnd ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝐵 ∈ ℂ )
22 16 21 subeq0ad ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( ( 𝐴 − 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) )
23 22 bicomd ⊢ ( ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 − 𝐵 ) = 0 ) )
24 23 ex ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 − 𝐵 ) = 0 ) ) )
25 5 24 ralrimi ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 = 𝐵 ↔ ( 𝐴 − 𝐵 ) = 0 ) )
26 rabbi ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 = 𝐵 ↔ ( 𝐴 − 𝐵 ) = 0 ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 − 𝐵 ) = 0 } )
27 25 26 sylib ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 − 𝐵 ) = 0 } )
28 27 3adant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 − 𝐵 ) = 0 } )
29 simp1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
30 mzpsubmpt ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝐴 − 𝐵 ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
31 30 3adant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝐴 − 𝐵 ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
32 eq0rabdioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝐴 − 𝐵 ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 − 𝐵 ) = 0 } ∈ ( Dioph ‘ 𝑁 ) )
33 29 31 32 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 − 𝐵 ) = 0 } ∈ ( Dioph ‘ 𝑁 ) )
34 28 33 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 𝐵 } ∈ ( Dioph ‘ 𝑁 ) )