Metamath Proof Explorer

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 ⊢ x = 1 → x ⋘ ⁡ ℝ 𝑠 * y ↔ 1 ⋘ ⁡ ℝ 𝑠 * y
7 breq2 ⊢ y = +∞ → 1 ⋘ ⁡ ℝ 𝑠 * y ↔ 1 ⋘ ⁡ ℝ 𝑠 * +∞
8 6 7 rspc2ev ⊢ 1 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ 1 ⋘ ⁡ ℝ 𝑠 * +∞ → ∃ x ∈ ℝ * ∃ y ∈ ℝ * x ⋘ ⁡ ℝ 𝑠 * y
9 1 2 5 8 mp3an ⊢ ∃ x ∈ ℝ * ∃ y ∈ ℝ * x ⋘ ⁡ ℝ 𝑠 * y
10 rexnal ⊢ ∃ x ∈ ℝ * ¬ ∀ y ∈ ℝ * ¬ x ⋘ ⁡ ℝ 𝑠 * y ↔ ¬ ∀ x ∈ ℝ * ∀ y ∈ ℝ * ¬ x ⋘ ⁡ ℝ 𝑠 * y
11 dfrex2 ⊢ ∃ y ∈ ℝ * x ⋘ ⁡ ℝ 𝑠 * y ↔ ¬ ∀ y ∈ ℝ * ¬ x ⋘ ⁡ ℝ 𝑠 * y
12 11 rexbii ⊢ ∃ x ∈ ℝ * ∃ y ∈ ℝ * x ⋘ ⁡ ℝ 𝑠 * y ↔ ∃ x ∈ ℝ * ¬ ∀ y ∈ ℝ * ¬ x ⋘ ⁡ ℝ 𝑠 * y
13 xrsex ⊢ ℝ 𝑠 * ∈ V
14 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
15 xrs0 ⊢ 0 = 0 ℝ 𝑠 *
16 eqid ⊢ ⋘ ⁡ ℝ 𝑠 * = ⋘ ⁡ ℝ 𝑠 *
17 14 15 16 isarchi ⊢ ℝ 𝑠 * ∈ V → ℝ 𝑠 * ∈ Archi ↔ ∀ x ∈ ℝ * ∀ y ∈ ℝ * ¬ x ⋘ ⁡ ℝ 𝑠 * y
18 13 17 ax-mp ⊢ ℝ 𝑠 * ∈ Archi ↔ ∀ x ∈ ℝ * ∀ y ∈ ℝ * ¬ x ⋘ ⁡ ℝ 𝑠 * y
19 18 notbii ⊢ ¬ ℝ 𝑠 * ∈ Archi ↔ ¬ ∀ x ∈ ℝ * ∀ y ∈ ℝ * ¬ x ⋘ ⁡ ℝ 𝑠 * y
20 10 12 19 3bitr4i ⊢ ∃ x ∈ ℝ * ∃ y ∈ ℝ * x ⋘ ⁡ ℝ 𝑠 * y ↔ ¬ ℝ 𝑠 * ∈ Archi
21 9 20 mpbi ⊢ ¬ ℝ 𝑠 * ∈ Archi