Metamath Proof Explorer

Theorem eluzrabdioph

Description: Diophantine set builder for membership in a fixed upper set of integers. (Contributed by Stefan O'Rear, 11-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 rabdiophlem1 ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )
2 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝐴 ) )
3 2 ex ⊢ ( 𝑀 ∈ ℤ → ( 𝐴 ∈ ℤ → ( 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝐴 ) ) )
4 3 ralimdv ⊢ ( 𝑀 ∈ ℤ → ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝐴 ) ) )
5 4 imp ⊢ ( ( 𝑀 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝐴 ) )
6 1 5 sylan2 ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝐴 ) )
7 rabbi ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝐴 ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝑀 ≤ 𝐴 } )
8 6 7 sylib ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝑀 ≤ 𝐴 } )
9 8 3adant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝑀 ≤ 𝐴 } )
10 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
11 mzpconstmpt ⊢ ( ( ( 1 ... 𝑁 ) ∈ V ∧ 𝑀 ∈ ℤ ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝑀 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
12 10 11 mpan ⊢ ( 𝑀 ∈ ℤ → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝑀 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
13 lerabdioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝑀 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝑀 ≤ 𝐴 } ∈ ( Dioph ‘ 𝑁 ) )
14 12 13 syl3an2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝑀 ≤ 𝐴 } ∈ ( Dioph ‘ 𝑁 ) )
15 9 14 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) } ∈ ( Dioph ‘ 𝑁 ) )