Theorem xrnarchi

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

	Ref	Expression
Assertion	xrnarchi	$$⊢\neg {ℝ}_{𝑠}^{*}\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\leftrightarrow 1⋘\left({ℝ}_{𝑠}^{*}\right)y\right)$$
7		breq2	$$⊢y=\mathrm{+\infty }\to \left(1⋘\left({ℝ}_{𝑠}^{*}\right)y\leftrightarrow 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 {ℝ}^{*}\exists y\in {ℝ}^{*}x⋘\left({ℝ}_{𝑠}^{*}\right)y$$
9	1 2 5 8	mp3an	$$⊢\exists x\in {ℝ}^{*}\exists y\in {ℝ}^{*}x⋘\left({ℝ}_{𝑠}^{*}\right)y$$
10		rexnal	$$⊢\exists x\in {ℝ}^{*}\neg \forall y\in {ℝ}^{*}\neg x⋘\left({ℝ}_{𝑠}^{*}\right)y\leftrightarrow \neg \forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\neg x⋘\left({ℝ}_{𝑠}^{*}\right)y$$
11		dfrex2	$$⊢\exists y\in {ℝ}^{*}x⋘\left({ℝ}_{𝑠}^{*}\right)y\leftrightarrow \neg \forall y\in {ℝ}^{*}\neg x⋘\left({ℝ}_{𝑠}^{*}\right)y$$
12	11	rexbii	$$⊢\exists x\in {ℝ}^{*}\exists y\in {ℝ}^{*}x⋘\left({ℝ}_{𝑠}^{*}\right)y\leftrightarrow \exists x\in {ℝ}^{*}\neg \forall y\in {ℝ}^{*}\neg 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}\leftrightarrow \forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\neg x⋘\left({ℝ}_{𝑠}^{*}\right)y\right)$$
18	13 17	ax-mp	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{Archi}\leftrightarrow \forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\neg x⋘\left({ℝ}_{𝑠}^{*}\right)y$$
19	18	notbii	$$⊢\neg {ℝ}_{𝑠}^{*}\in \mathrm{Archi}\leftrightarrow \neg \forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\neg x⋘\left({ℝ}_{𝑠}^{*}\right)y$$
20	10 12 19	3bitr4i	$$⊢\exists x\in {ℝ}^{*}\exists y\in {ℝ}^{*}x⋘\left({ℝ}_{𝑠}^{*}\right)y\leftrightarrow \neg {ℝ}_{𝑠}^{*}\in \mathrm{Archi}$$
21	9 20	mpbi	$$⊢\neg {ℝ}_{𝑠}^{*}\in \mathrm{Archi}$$