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 
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A =/= B } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 rabdiophlem1 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ )
2 rabdiophlem1 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ )
3 zre 
 |-  ( A e. ZZ -> A e. RR )
4 zre 
 |-  ( B e. ZZ -> B e. RR )
5 lttri2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )
6 3 4 5 syl2an 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )
7 6 ralimi 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ZZ /\ B e. ZZ ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) ( A =/= B <-> ( A < B \/ B < A ) ) )
8 r19.26 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ZZ /\ B e. ZZ ) <-> ( A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ /\ A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ ) )
9 rabbi 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A =/= B <-> ( A < B \/ B < A ) ) <-> { t e. ( NN0 ^m ( 1 ... N ) ) | A =/= B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( A < B \/ B < A ) } )
10 7 8 9 3imtr3i 
 |-  ( ( A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ /\ A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A =/= B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( A < B \/ B < A ) } )
11 1 2 10 syl2an 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A =/= B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( A < B \/ B < A ) } )
12 11 3adant1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A =/= B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( A < B \/ B < A ) } )
13 ltrabdioph 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A < B } e. ( Dioph ` N ) )
14 ltrabdioph 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | B < A } e. ( Dioph ` N ) )
15 14 3com23 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | B < A } e. ( Dioph ` N ) )
16 orrabdioph 
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | A < B } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | B < A } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( A < B \/ B < A ) } e. ( Dioph ` N ) )
17 13 15 16 syl2anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( A < B \/ B < A ) } e. ( Dioph ` N ) )
18 12 17 eqeltrd 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A =/= B } e. ( Dioph ` N ) )