Metamath Proof Explorer

Theorem ltrabdioph

Description: Diophantine set builder for the strict less than relation. (Contributed by Stefan O'Rear, 11-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 rabdiophlem1 ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )
2 rabdiophlem1 ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ )
3 znnsub ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℕ ) )
4 3 ralimi ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℕ ) )
5 r19.26 ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ↔ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) )
6 rabbi ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℕ ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐵 − 𝐴 ) ∈ ℕ } )
7 4 5 6 3imtr3i ⊢ ( ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐵 − 𝐴 ) ∈ ℕ } )
8 1 2 7 syl2an ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐵 − 𝐴 ) ∈ ℕ } )
9 8 3adant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐵 − 𝐴 ) ∈ ℕ } )
10 simp1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
11 mzpsubmpt ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝐵 − 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
12 11 ancoms ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝐵 − 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
13 12 3adant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝐵 − 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
14 elnnrabdioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ( 𝐵 − 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐵 − 𝐴 ) ∈ ℕ } ∈ ( Dioph ‘ 𝑁 ) )
15 10 13 14 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐵 − 𝐴 ) ∈ ℕ } ∈ ( Dioph ‘ 𝑁 ) )
16 9 15 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } ∈ ( Dioph ‘ 𝑁 ) )