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 = ( 0_g ‘ ℝ^*_𝑠 )
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

Metamath Proof Explorer

Theorem xrnarchi

Proof