This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elq

Description: Membership in the set of rationals. (Contributed by NM, 8-Jan-2002) (Revised by Mario Carneiro, 28-Jan-2014)

Ref Expression
Assertion elq 
|- ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )

Proof

Step Hyp Ref Expression
1 df-q 
 |-  QQ = ( / " ( ZZ X. NN ) )
2 1 eleq2i 
 |-  ( A e. QQ <-> A e. ( / " ( ZZ X. NN ) ) )
3 df-div 
 |-  / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
4 riotaex 
 |-  ( iota_ z e. CC ( y x. z ) = x ) e. _V
5 3 4 fnmpoi 
 |-  / Fn ( CC X. ( CC \ { 0 } ) )
6 zsscn 
 |-  ZZ C_ CC
7 nncn 
 |-  ( x e. NN -> x e. CC )
8 nnne0 
 |-  ( x e. NN -> x =/= 0 )
9 eldifsn 
 |-  ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) )
10 7 8 9 sylanbrc 
 |-  ( x e. NN -> x e. ( CC \ { 0 } ) )
11 10 ssriv 
 |-  NN C_ ( CC \ { 0 } )
12 xpss12 
 |-  ( ( ZZ C_ CC /\ NN C_ ( CC \ { 0 } ) ) -> ( ZZ X. NN ) C_ ( CC X. ( CC \ { 0 } ) ) )
13 6 11 12 mp2an 
 |-  ( ZZ X. NN ) C_ ( CC X. ( CC \ { 0 } ) )
14 ovelimab 
 |-  ( ( / Fn ( CC X. ( CC \ { 0 } ) ) /\ ( ZZ X. NN ) C_ ( CC X. ( CC \ { 0 } ) ) ) -> ( A e. ( / " ( ZZ X. NN ) ) <-> E. x e. ZZ E. y e. NN A = ( x / y ) ) )
15 5 13 14 mp2an 
 |-  ( A e. ( / " ( ZZ X. NN ) ) <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
16 2 15 bitri 
 |-  ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )