Metamath Proof Explorer


Theorem nerabdioph

Description: Diophantine set builder for inequality. This not quite trivial theorem touches on something important; Diophantine sets are not closed under negation, but they contain an important subclass that is, namely the recursive sets. With this theorem and De Morgan's laws, all quantifier-free formulas can be negated. (Contributed by Stefan O'Rear, 11-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 rabdiophlem1 ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )
2 rabdiophlem1 ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ )
3 zre ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
4 zre ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
5 lttri2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴𝐵 ↔ ( 𝐴 < 𝐵𝐵 < 𝐴 ) ) )
6 3 4 5 syl2an ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴𝐵 ↔ ( 𝐴 < 𝐵𝐵 < 𝐴 ) ) )
7 6 ralimi ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ( 𝐴𝐵 ↔ ( 𝐴 < 𝐵𝐵 < 𝐴 ) ) )
8 r19.26 ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ↔ ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) )
9 rabbi ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ( 𝐴𝐵 ↔ ( 𝐴 < 𝐵𝐵 < 𝐴 ) ) ↔ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵𝐵 < 𝐴 ) } )
10 7 8 9 3imtr3i ( ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵𝐵 < 𝐴 ) } )
11 1 2 10 syl2an ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵𝐵 < 𝐴 ) } )
12 11 3adant1 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵𝐵 < 𝐴 ) } )
13 ltrabdioph ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } ∈ ( Dioph ‘ 𝑁 ) )
14 ltrabdioph ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐵 < 𝐴 } ∈ ( Dioph ‘ 𝑁 ) )
15 14 3com23 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐵 < 𝐴 } ∈ ( Dioph ‘ 𝑁 ) )
16 orrabdioph ( ( { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐵 < 𝐴 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵𝐵 < 𝐴 ) } ∈ ( Dioph ‘ 𝑁 ) )
17 13 15 16 syl2anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵𝐵 < 𝐴 ) } ∈ ( Dioph ‘ 𝑁 ) )
18 12 17 eqeltrd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } ∈ ( Dioph ‘ 𝑁 ) )