# Metamath Proof Explorer

## Theorem xrnarchi

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

Ref Expression
Assertion xrnarchi ${⊢}¬{ℝ}_{𝑠}^{*}\in \mathrm{Archi}$

### Proof

Step Hyp Ref Expression
1 1xr ${⊢}1\in {ℝ}^{*}$
2 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
3 1rp ${⊢}1\in {ℝ}^{+}$
4 pnfinf ${⊢}1\in {ℝ}^{+}\to 1⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }$
5 3 4 ax-mp ${⊢}1⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }$
6 breq1 ${⊢}{x}=1\to \left({x}⋘\left({ℝ}_{𝑠}^{*}\right){y}↔1⋘\left({ℝ}_{𝑠}^{*}\right){y}\right)$
7 breq2 ${⊢}{y}=\mathrm{+\infty }\to \left(1⋘\left({ℝ}_{𝑠}^{*}\right){y}↔1⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }\right)$
8 6 7 rspc2ev ${⊢}\left(1\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 1⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}$
9 1 2 5 8 mp3an ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}$
10 rexnal ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}↔¬\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}$
11 dfrex2 ${⊢}\exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}↔¬\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}$
12 11 rexbii ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}$
13 xrsex ${⊢}{ℝ}_{𝑠}^{*}\in \mathrm{V}$
14 xrsbas ${⊢}{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$
15 xrs0 ${⊢}0={0}_{{ℝ}_{𝑠}^{*}}$
16 eqid ${⊢}⋘\left({ℝ}_{𝑠}^{*}\right)=⋘\left({ℝ}_{𝑠}^{*}\right)$
17 14 15 16 isarchi ${⊢}{ℝ}_{𝑠}^{*}\in \mathrm{V}\to \left({ℝ}_{𝑠}^{*}\in \mathrm{Archi}↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}\right)$
18 13 17 ax-mp ${⊢}{ℝ}_{𝑠}^{*}\in \mathrm{Archi}↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}$
19 18 notbii ${⊢}¬{ℝ}_{𝑠}^{*}\in \mathrm{Archi}↔¬\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}¬{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}$
20 10 12 19 3bitr4i ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{x}⋘\left({ℝ}_{𝑠}^{*}\right){y}↔¬{ℝ}_{𝑠}^{*}\in \mathrm{Archi}$
21 9 20 mpbi ${⊢}¬{ℝ}_{𝑠}^{*}\in \mathrm{Archi}$