Metamath Proof Explorer

Theorem eirr

Description: _e is irrational. (Contributed by Paul Chapman, 9-Feb-2008) (Proof shortened by Mario Carneiro, 29-Apr-2014)

Ref Expression
Assertion eirr 
|- _e e/ QQ

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( n e. NN0 |-> ( 1 / ( ! ` n ) ) ) = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
2 simpll 
 |-  ( ( ( p e. ZZ /\ q e. NN ) /\ _e = ( p / q ) ) -> p e. ZZ )
3 simplr 
 |-  ( ( ( p e. ZZ /\ q e. NN ) /\ _e = ( p / q ) ) -> q e. NN )
4 simpr 
 |-  ( ( ( p e. ZZ /\ q e. NN ) /\ _e = ( p / q ) ) -> _e = ( p / q ) )
5 1 2 3 4 eirrlem 
 |-  -. ( ( p e. ZZ /\ q e. NN ) /\ _e = ( p / q ) )
6 5 imnani 
 |-  ( ( p e. ZZ /\ q e. NN ) -> -. _e = ( p / q ) )
7 6 nrexdv 
 |-  ( p e. ZZ -> -. E. q e. NN _e = ( p / q ) )
8 7 nrex 
 |-  -. E. p e. ZZ E. q e. NN _e = ( p / q )
9 elq 
 |-  ( _e e. QQ <-> E. p e. ZZ E. q e. NN _e = ( p / q ) )
10 8 9 mtbir 
 |-  -. _e e. QQ
11 10 nelir 
 |-  _e e/ QQ