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

Metamath Proof Explorer

Theorem xrnarchi

Description: The completed real line is not Archimedean. (Contributed by Thierry Arnoux, 1-Feb-2018)

Ref Expression
Assertion xrnarchi 
|- -. RR*s e. Archi

Proof

Step Hyp Ref Expression
1 1xr 
 |-  1 e. RR*
2 pnfxr 
 |-  +oo e. RR*
3 1rp 
 |-  1 e. RR+
4 pnfinf 
 |-  ( 1 e. RR+ -> 1 ( <<< ` RR*s ) +oo )
5 3 4 ax-mp 
 |-  1 ( <<< ` RR*s ) +oo
6 breq1 
 |-  ( x = 1 -> ( x ( <<< ` RR*s ) y <-> 1 ( <<< ` RR*s ) y ) )
7 breq2 
 |-  ( y = +oo -> ( 1 ( <<< ` RR*s ) y <-> 1 ( <<< ` RR*s ) +oo ) )
8 6 7 rspc2ev 
 |-  ( ( 1 e. RR* /\ +oo e. RR* /\ 1 ( <<< ` RR*s ) +oo ) -> E. x e. RR* E. y e. RR* x ( <<< ` RR*s ) y )
9 1 2 5 8 mp3an 
 |-  E. x e. RR* E. y e. RR* x ( <<< ` RR*s ) y
10 rexnal 
 |-  ( E. x e. RR* -. A. y e. RR* -. x ( <<< ` RR*s ) y <-> -. A. x e. RR* A. y e. RR* -. x ( <<< ` RR*s ) y )
11 dfrex2 
 |-  ( E. y e. RR* x ( <<< ` RR*s ) y <-> -. A. y e. RR* -. x ( <<< ` RR*s ) y )
12 11 rexbii 
 |-  ( E. x e. RR* E. y e. RR* x ( <<< ` RR*s ) y <-> E. x e. RR* -. A. y e. RR* -. x ( <<< ` RR*s ) y )
13 xrsex 
 |-  RR*s e. _V
14 xrsbas 
 |-  RR* = ( Base ` RR*s )
15 xrs0 
 |-  0 = ( 0g ` RR*s )
16 eqid 
 |-  ( <<< ` RR*s ) = ( <<< ` RR*s )
17 14 15 16 isarchi 
 |-  ( RR*s e. _V -> ( RR*s e. Archi <-> A. x e. RR* A. y e. RR* -. x ( <<< ` RR*s ) y ) )
18 13 17 ax-mp 
 |-  ( RR*s e. Archi <-> A. x e. RR* A. y e. RR* -. x ( <<< ` RR*s ) y )
19 18 notbii 
 |-  ( -. RR*s e. Archi <-> -. A. x e. RR* A. y e. RR* -. x ( <<< ` RR*s ) y )
20 10 12 19 3bitr4i 
 |-  ( E. x e. RR* E. y e. RR* x ( <<< ` RR*s ) y <-> -. RR*s e. Archi )
21 9 20 mpbi 
 |-  -. RR*s e. Archi