ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  axarch Unicode version

Theorem axarch 7424
Description: Archimedean axiom. The Archimedean property is more naturally stated once we have defined  NN. Unless we find another way to state it, we'll just use the right hand side of dfnn2 8422 in stating what we mean by "natural number" in the context of this axiom.

This construction-dependent theorem should not be referenced directly; instead, use ax-arch 7462. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)

Assertion
Ref Expression
axarch  |-  ( A  e.  RR  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } A  <RR  n )
Distinct variable group:    A, n, x, y

Proof of Theorem axarch
Dummy variables  l  u  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 7364 . . 3  |-  ( A  e.  RR  <->  E. z  e.  R.  <. z ,  0R >.  =  A )
21biimpi 118 . 2  |-  ( A  e.  RR  ->  E. z  e.  R.  <. z ,  0R >.  =  A )
3 archsr 7325 . . . 4  |-  ( z  e.  R.  ->  E. w  e.  N.  z  <R  [ <. (
<. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
43ad2antrl 474 . . 3  |-  ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  ->  E. w  e.  N.  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
5 simplrr 503 . . . . 5  |-  ( ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  /\  ( w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  ->  <. z ,  0R >.  =  A
)
6 simprr 499 . . . . . 6  |-  ( ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  /\  ( w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  ->  z  <R  [
<. ( <. { l  |  l  <Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
7 ltresr 7374 . . . . . 6  |-  ( <.
z ,  0R >.  <RR  <. [ <. ( <. { l  |  l  <Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. 
<->  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
86, 7sylibr 132 . . . . 5  |-  ( ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  /\  ( w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  ->  <. z ,  0R >.  <RR  <. [ <. (
<. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
95, 8eqbrtrrd 3867 . . . 4  |-  ( ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  /\  ( w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  ->  A  <RR  <. [ <. ( <. { l  |  l  <Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
10 pitonn 7383 . . . . . 6  |-  ( w  e.  N.  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } )
1110ad2antrl 474 . . . . 5  |-  ( ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  /\  ( w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  ->  <. [ <. (
<. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } )
12 simpr 108 . . . . . 6  |-  ( ( ( ( A  e.  RR  /\  ( z  e.  R.  /\  <. z ,  0R >.  =  A ) )  /\  (
w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  /\  n  =  <. [ <. ( <. { l  |  l  <Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  ->  n  =  <. [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
1312breq2d 3857 . . . . 5  |-  ( ( ( ( A  e.  RR  /\  ( z  e.  R.  /\  <. z ,  0R >.  =  A ) )  /\  (
w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  /\  n  =  <. [ <. ( <. { l  |  l  <Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  ->  ( A  <RR  n  <->  A  <RR  <. [ <. ( <. { l  |  l  <Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. ) )
1411, 13rspcedv 2726 . . . 4  |-  ( ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  /\  ( w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  ->  ( A  <RR 
<. [ <. ( <. { l  |  l  <Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } A  <RR  n ) )
159, 14mpd 13 . . 3  |-  ( ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  /\  ( w  e.  N.  /\  z  <R  [ <. ( <. { l  |  l 
<Q  [ <. w ,  1o >. ]  ~Q  } ,  { u  |  [ <. w ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  )
)  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } A  <RR  n )
164, 15rexlimddv 2493 . 2  |-  ( ( A  e.  RR  /\  ( z  e.  R.  /\ 
<. z ,  0R >.  =  A ) )  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } A  <RR  n )
172, 16rexlimddv 2493 1  |-  ( A  e.  RR  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } A  <RR  n )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1289    e. wcel 1438   {cab 2074   A.wral 2359   E.wrex 2360   <.cop 3449   |^|cint 3688   class class class wbr 3845  (class class class)co 5652   1oc1o 6174   [cec 6288   N.cnpi 6829    ~Q ceq 6836    <Q cltq 6842   1Pc1p 6849    +P. cpp 6850    ~R cer 6853   R.cnr 6854   0Rc0r 6855    <R cltr 6860   RRcr 7347   1c1 7349    + caddc 7351    <RR cltrr 7352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3954  ax-sep 3957  ax-nul 3965  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-setind 4353  ax-iinf 4403
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-int 3689  df-iun 3732  df-br 3846  df-opab 3900  df-mpt 3901  df-tr 3937  df-eprel 4116  df-id 4120  df-po 4123  df-iso 4124  df-iord 4193  df-on 4195  df-suc 4198  df-iom 4406  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022  df-fv 5023  df-ov 5655  df-oprab 5656  df-mpt2 5657  df-1st 5911  df-2nd 5912  df-recs 6070  df-irdg 6135  df-1o 6181  df-2o 6182  df-oadd 6185  df-omul 6186  df-er 6290  df-ec 6292  df-qs 6296  df-ni 6861  df-pli 6862  df-mi 6863  df-lti 6864  df-plpq 6901  df-mpq 6902  df-enq 6904  df-nqqs 6905  df-plqqs 6906  df-mqqs 6907  df-1nqqs 6908  df-rq 6909  df-ltnqqs 6910  df-enq0 6981  df-nq0 6982  df-0nq0 6983  df-plq0 6984  df-mq0 6985  df-inp 7023  df-i1p 7024  df-iplp 7025  df-iltp 7027  df-enr 7270  df-nr 7271  df-plr 7272  df-ltr 7274  df-0r 7275  df-1r 7276  df-c 7354  df-1 7356  df-r 7358  df-add 7359  df-lt 7361
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator