Metamath Proof Explorer

Theorem eq0rabdioph

Description: This is the first of a number of theorems which allow sets to be proven Diophantine by syntactic induction, and models the correspondence between Diophantine sets and monotone existential first-order logic. This first theorem shows that the zero set of an implicit polynomial is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑡 𝑁 ∈ ℕ0
2 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 )
3 2 nfel1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) )
4 1 3 nfan ⊢ Ⅎ 𝑡 ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
5 zex ⊢ ℤ ∈ V
6 nn0ssz ⊢ ℕ0 ⊆ ℤ
7 mapss ⊢ ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
8 5 6 7 mp2an ⊢ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℤ ↑m ( 1 ... 𝑁 ) )
9 8 sseli ⊢ ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
10 9 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
11 mzpf ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
12 mptfcl ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) → 𝐴 ∈ ℤ ) )
13 12 imp ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ ∧ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ) → 𝐴 ∈ ℤ )
14 11 9 13 syl2an ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝐴 ∈ ℤ )
15 14 adantll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝐴 ∈ ℤ )
16 eqid ⊢ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 )
17 16 fvmpt2 ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 𝐴 )
18 10 15 17 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 𝐴 )
19 18 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → 𝐴 = ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) )
20 19 eqeq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( 𝐴 = 0 ↔ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0 ) )
21 20 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( 𝐴 = 0 ↔ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0 ) ) )
22 4 21 ralrimi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 = 0 ↔ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0 ) )
23 rabbi ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 = 0 ↔ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0 ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 0 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0 } )
24 22 23 sylib ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 0 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0 } )
25 nfcv ⊢ Ⅎ 𝑡 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
26 nfcv ⊢ Ⅎ 𝑎 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
27 nfv ⊢ Ⅎ 𝑎 ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0
28 nffvmpt1 ⊢ Ⅎ 𝑡 ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 )
29 28 nfeq1 ⊢ Ⅎ 𝑡 ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0
30 fveqeq2 ⊢ ( 𝑡 = 𝑎 → ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0 ↔ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 ) )
31 25 26 27 29 30 cbvrabw ⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑡 ) = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 }
32 24 31 eqtrdi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 } )
33 df-rab ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 } = { 𝑎 ∣ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 ) }
34 32 33 eqtrdi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 0 } = { 𝑎 ∣ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 ) } )
35 elmapi ⊢ ( 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → 𝑏 : ( 1 ... 𝑁 ) ⟶ ℕ0 )
36 ffn ⊢ ( 𝑏 : ( 1 ... 𝑁 ) ⟶ ℕ0 → 𝑏 Fn ( 1 ... 𝑁 ) )
37 fnresdm ⊢ ( 𝑏 Fn ( 1 ... 𝑁 ) → ( 𝑏 ↾ ( 1 ... 𝑁 ) ) = 𝑏 )
38 35 36 37 3syl ⊢ ( 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( 𝑏 ↾ ( 1 ... 𝑁 ) ) = 𝑏 )
39 38 eqeq2d ⊢ ( 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑎 = 𝑏 ) )
40 equcom ⊢ ( 𝑎 = 𝑏 ↔ 𝑏 = 𝑎 )
41 39 40 bitrdi ⊢ ( 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑏 = 𝑎 ) )
42 41 anbi1d ⊢ ( 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) ↔ ( 𝑏 = 𝑎 ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) ) )
43 42 rexbiia ⊢ ( ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝑏 = 𝑎 ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) )
44 fveqeq2 ⊢ ( 𝑏 = 𝑎 → ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ↔ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 ) )
45 44 ceqsrexbv ⊢ ( ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝑏 = 𝑎 ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) ↔ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 ) )
46 43 45 bitr2i ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) )
47 46 abbii ⊢ { 𝑎 ∣ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑎 ) = 0 ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) }
48 34 47 eqtrdi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 0 } = { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) } )
49 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
50 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
51 uzid ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
52 50 51 syl ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
53 52 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
54 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
55 eldioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
56 49 53 54 55 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ 𝑏 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
57 48 56 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 = 0 } ∈ ( Dioph ‘ 𝑁 ) )