MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  arch Structured version   Unicode version

Theorem arch 10812
Description: Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed by NM, 21-Jan-1997.)
Assertion
Ref Expression
arch  |-  ( A  e.  RR  ->  E. n  e.  NN  A  <  n
)
Distinct variable group:    A, n

Proof of Theorem arch
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 breq1 4364 . . 3  |-  ( y  =  A  ->  (
y  <  n  <->  A  <  n ) )
21rexbidv 2873 . 2  |-  ( y  =  A  ->  ( E. n  e.  NN  y  <  n  <->  E. n  e.  NN  A  <  n
) )
3 nnunb 10811 . . . 4  |-  -.  E. y  e.  RR  A. n  e.  NN  ( n  < 
y  \/  n  =  y )
4 ralnex 2806 . . . 4  |-  ( A. y  e.  RR  -.  A. n  e.  NN  (
n  <  y  \/  n  =  y )  <->  -. 
E. y  e.  RR  A. n  e.  NN  (
n  <  y  \/  n  =  y )
)
53, 4mpbir 212 . . 3  |-  A. y  e.  RR  -.  A. n  e.  NN  ( n  < 
y  \/  n  =  y )
6 rexnal 2808 . . . . 5  |-  ( E. n  e.  NN  -.  ( n  <  y  \/  n  =  y )  <->  -.  A. n  e.  NN  ( n  <  y  \/  n  =  y ) )
7 nnre 10562 . . . . . . . . 9  |-  ( n  e.  NN  ->  n  e.  RR )
8 axlttri 9651 . . . . . . . . 9  |-  ( ( y  e.  RR  /\  n  e.  RR )  ->  ( y  <  n  <->  -.  ( y  =  n  \/  n  <  y
) ) )
97, 8sylan2 476 . . . . . . . 8  |-  ( ( y  e.  RR  /\  n  e.  NN )  ->  ( y  <  n  <->  -.  ( y  =  n  \/  n  <  y
) ) )
10 equcom 1848 . . . . . . . . . . 11  |-  ( y  =  n  <->  n  =  y )
1110orbi1i 522 . . . . . . . . . 10  |-  ( ( y  =  n  \/  n  <  y )  <-> 
( n  =  y  \/  n  <  y
) )
12 orcom 388 . . . . . . . . . 10  |-  ( ( n  =  y  \/  n  <  y )  <-> 
( n  <  y  \/  n  =  y
) )
1311, 12bitri 252 . . . . . . . . 9  |-  ( ( y  =  n  \/  n  <  y )  <-> 
( n  <  y  \/  n  =  y
) )
1413notbii 297 . . . . . . . 8  |-  ( -.  ( y  =  n  \/  n  <  y
)  <->  -.  ( n  <  y  \/  n  =  y ) )
159, 14syl6bb 264 . . . . . . 7  |-  ( ( y  e.  RR  /\  n  e.  NN )  ->  ( y  <  n  <->  -.  ( n  <  y  \/  n  =  y
) ) )
1615biimprd 226 . . . . . 6  |-  ( ( y  e.  RR  /\  n  e.  NN )  ->  ( -.  ( n  <  y  \/  n  =  y )  -> 
y  <  n )
)
1716reximdva 2834 . . . . 5  |-  ( y  e.  RR  ->  ( E. n  e.  NN  -.  ( n  <  y  \/  n  =  y
)  ->  E. n  e.  NN  y  <  n
) )
186, 17syl5bir 221 . . . 4  |-  ( y  e.  RR  ->  ( -.  A. n  e.  NN  ( n  <  y  \/  n  =  y )  ->  E. n  e.  NN  y  <  n ) )
1918ralimia 2751 . . 3  |-  ( A. y  e.  RR  -.  A. n  e.  NN  (
n  <  y  \/  n  =  y )  ->  A. y  e.  RR  E. n  e.  NN  y  <  n )
205, 19ax-mp 5 . 2  |-  A. y  e.  RR  E. n  e.  NN  y  <  n
212, 20vtoclri 3094 1  |-  ( A  e.  RR  ->  E. n  e.  NN  A  <  n
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2709   E.wrex 2710   class class class wbr 4361   RRcr 9484    < clt 9621   NNcn 10555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556
This theorem is referenced by:  nnrecl  10813  bndndx  10814  btwnz  10983  uzwo3  11205  zmin  11206  rpnnen1lem5  11240  harmonic  13855  alzdvds  14293  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  volsup2  22500  ismbf3d  22547  mbfi1fseqlem6  22615  itg2seq  22637  itg2cnlem1  22656  ply1divex  23024  plydivex  23187  lgamucov  23900  lgamcvg2  23917  ubthlem1  26449  lnconi  27623  rearchi  28552  esumcst  28831  hbtlem5  35900  prmunb2  36572  rfcnnnub  37273  stoweidlem14  37757  stoweidlem60  37804  sge0rpcpnf  38114  hoicvr  38217
  Copyright terms: Public domain W3C validator