Theorem xrnarchi

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

	Ref	Expression
Assertion	xrnarchi	⊢ ¬ ℝ*𝑠 ∈ Archi

Proof

Step	Hyp	Ref	Expression
1		1xr	⊢ 1 ∈ ℝ*
2		pnfxr	⊢ +∞ ∈ ℝ*
3		1rp	⊢ 1 ∈ ℝ+
4		pnfinf	⊢ ( 1 ∈ ℝ+ → 1 ( ⋘ ‘ ℝ*𝑠 ) +∞ )
5	3 4	ax-mp	⊢ 1 ( ⋘ ‘ ℝ*𝑠 ) +∞
6		breq1	⊢ ( 𝑥 = 1 → ( 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 ↔ 1 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 ) )
7		breq2	⊢ ( 𝑦 = +∞ → ( 1 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 ↔ 1 ( ⋘ ‘ ℝ*𝑠 ) +∞ ) )
8	6 7	rspc2ev	⊢ ( ( 1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1 ( ⋘ ‘ ℝ*𝑠 ) +∞ ) → ∃ 𝑥 ∈ ℝ* ∃ 𝑦 ∈ ℝ* 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 )
9	1 2 5 8	mp3an	⊢ ∃ 𝑥 ∈ ℝ* ∃ 𝑦 ∈ ℝ* 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦
10		rexnal	⊢ ( ∃ 𝑥 ∈ ℝ* ¬ ∀ 𝑦 ∈ ℝ* ¬ 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 ↔ ¬ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ¬ 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 )
11		dfrex2	⊢ ( ∃ 𝑦 ∈ ℝ* 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 ↔ ¬ ∀ 𝑦 ∈ ℝ* ¬ 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 )
12	11	rexbii	⊢ ( ∃ 𝑥 ∈ ℝ* ∃ 𝑦 ∈ ℝ* 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 ↔ ∃ 𝑥 ∈ ℝ* ¬ ∀ 𝑦 ∈ ℝ* ¬ 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 )
13		xrsex	⊢ ℝ*𝑠 ∈ V
14		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
15		xrs0	⊢ 0 = ( 0g ‘ ℝ*𝑠 )
16		eqid	⊢ ( ⋘ ‘ ℝ*𝑠 ) = ( ⋘ ‘ ℝ*𝑠 )
17	14 15 16	isarchi	⊢ ( ℝ*𝑠 ∈ V → ( ℝ*𝑠 ∈ Archi ↔ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ¬ 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 ) )
18	13 17	ax-mp	⊢ ( ℝ*𝑠 ∈ Archi ↔ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ¬ 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 )
19	18	notbii	⊢ ( ¬ ℝ*𝑠 ∈ Archi ↔ ¬ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ¬ 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 )
20	10 12 19	3bitr4i	⊢ ( ∃ 𝑥 ∈ ℝ* ∃ 𝑦 ∈ ℝ* 𝑥 ( ⋘ ‘ ℝ*𝑠 ) 𝑦 ↔ ¬ ℝ*𝑠 ∈ Archi )
21	9 20	mpbi	⊢ ¬ ℝ*𝑠 ∈ Archi