Metamath Proof Explorer

Theorem rexzrexnn0

Description: Rewrite an existential quantification restricted to integers into an existential quantification restricted to naturals. (Contributed by Stefan O'Rear, 11-Oct-2014)

Ref Expression
Hypotheses rexzrexnn0.1 
|- ( x = y -> ( ph <-> ps ) )
rexzrexnn0.2 
|- ( x = -u y -> ( ph <-> ch ) )
Assertion rexzrexnn0 
|- ( E. x e. ZZ ph <-> E. y e. NN0 ( ps \/ ch ) )

Proof

Step Hyp Ref Expression
1 rexzrexnn0.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 rexzrexnn0.2 
 |-  ( x = -u y -> ( ph <-> ch ) )
3 elznn0 
 |-  ( x e. ZZ <-> ( x e. RR /\ ( x e. NN0 \/ -u x e. NN0 ) ) )
4 3 simprbi 
 |-  ( x e. ZZ -> ( x e. NN0 \/ -u x e. NN0 ) )
5 4 adantr 
 |-  ( ( x e. ZZ /\ ph ) -> ( x e. NN0 \/ -u x e. NN0 ) )
6 simpr 
 |-  ( ( ( x e. ZZ /\ ph ) /\ x e. NN0 ) -> x e. NN0 )
7 simplr 
 |-  ( ( ( x e. ZZ /\ ph ) /\ x e. NN0 ) -> ph )
8 1 equcoms 
 |-  ( y = x -> ( ph <-> ps ) )
9 8 bicomd 
 |-  ( y = x -> ( ps <-> ph ) )
10 9 rspcev 
 |-  ( ( x e. NN0 /\ ph ) -> E. y e. NN0 ps )
11 6 7 10 syl2anc 
 |-  ( ( ( x e. ZZ /\ ph ) /\ x e. NN0 ) -> E. y e. NN0 ps )
12 11 ex 
 |-  ( ( x e. ZZ /\ ph ) -> ( x e. NN0 -> E. y e. NN0 ps ) )
13 simpr 
 |-  ( ( x e. ZZ /\ -u x e. NN0 ) -> -u x e. NN0 )
14 zcn 
 |-  ( x e. ZZ -> x e. CC )
15 14 negnegd 
 |-  ( x e. ZZ -> -u -u x = x )
16 15 eqcomd 
 |-  ( x e. ZZ -> x = -u -u x )
17 negeq 
 |-  ( y = -u x -> -u y = -u -u x )
18 17 eqeq2d 
 |-  ( y = -u x -> ( x = -u y <-> x = -u -u x ) )
19 16 18 syl5ibrcom 
 |-  ( x e. ZZ -> ( y = -u x -> x = -u y ) )
20 19 imp 
 |-  ( ( x e. ZZ /\ y = -u x ) -> x = -u y )
21 20 2 syl 
 |-  ( ( x e. ZZ /\ y = -u x ) -> ( ph <-> ch ) )
22 21 bicomd 
 |-  ( ( x e. ZZ /\ y = -u x ) -> ( ch <-> ph ) )
23 22 adantlr 
 |-  ( ( ( x e. ZZ /\ -u x e. NN0 ) /\ y = -u x ) -> ( ch <-> ph ) )
24 13 23 rspcedv 
 |-  ( ( x e. ZZ /\ -u x e. NN0 ) -> ( ph -> E. y e. NN0 ch ) )
25 24 impancom 
 |-  ( ( x e. ZZ /\ ph ) -> ( -u x e. NN0 -> E. y e. NN0 ch ) )
26 12 25 orim12d 
 |-  ( ( x e. ZZ /\ ph ) -> ( ( x e. NN0 \/ -u x e. NN0 ) -> ( E. y e. NN0 ps \/ E. y e. NN0 ch ) ) )
27 5 26 mpd 
 |-  ( ( x e. ZZ /\ ph ) -> ( E. y e. NN0 ps \/ E. y e. NN0 ch ) )
28 r19.43 
 |-  ( E. y e. NN0 ( ps \/ ch ) <-> ( E. y e. NN0 ps \/ E. y e. NN0 ch ) )
29 27 28 sylibr 
 |-  ( ( x e. ZZ /\ ph ) -> E. y e. NN0 ( ps \/ ch ) )
30 29 rexlimiva 
 |-  ( E. x e. ZZ ph -> E. y e. NN0 ( ps \/ ch ) )
31 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
32 1 rspcev 
 |-  ( ( y e. ZZ /\ ps ) -> E. x e. ZZ ph )
33 31 32 sylan 
 |-  ( ( y e. NN0 /\ ps ) -> E. x e. ZZ ph )
34 nn0negz 
 |-  ( y e. NN0 -> -u y e. ZZ )
35 2 rspcev 
 |-  ( ( -u y e. ZZ /\ ch ) -> E. x e. ZZ ph )
36 34 35 sylan 
 |-  ( ( y e. NN0 /\ ch ) -> E. x e. ZZ ph )
37 33 36 jaodan 
 |-  ( ( y e. NN0 /\ ( ps \/ ch ) ) -> E. x e. ZZ ph )
38 37 rexlimiva 
 |-  ( E. y e. NN0 ( ps \/ ch ) -> E. x e. ZZ ph )
39 30 38 impbii 
 |-  ( E. x e. ZZ ph <-> E. y e. NN0 ( ps \/ ch ) )