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