Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  axarch GIF version

Theorem axarch 7719
 Description: Archimedean axiom. The Archimedean property is more naturally stated once we have defined ℕ. Unless we find another way to state it, we'll just use the right hand side of dfnn2 8742 in stating what we mean by "natural number" in the context of this axiom. This construction-dependent theorem should not be referenced directly; instead, use ax-arch 7759. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)
Assertion
Ref Expression
axarch (𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
Distinct variable group:   𝐴,𝑛,𝑥,𝑦

Proof of Theorem axarch
Dummy variables 𝑙 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 7656 . . 3 (𝐴 ∈ ℝ ↔ ∃𝑧R𝑧, 0R⟩ = 𝐴)
21biimpi 119 . 2 (𝐴 ∈ ℝ → ∃𝑧R𝑧, 0R⟩ = 𝐴)
3 archsr 7610 . . . 4 (𝑧R → ∃𝑤N 𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
43ad2antrl 482 . . 3 ((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) → ∃𝑤N 𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
5 simplrr 526 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ⟨𝑧, 0R⟩ = 𝐴)
6 simprr 522 . . . . . 6 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → 𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
7 ltresr 7667 . . . . . 6 (⟨𝑧, 0R⟩ < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ↔ 𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
86, 7sylibr 133 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ⟨𝑧, 0R⟩ < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
95, 8eqbrtrrd 3956 . . . 4 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → 𝐴 < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
10 pitonn 7676 . . . . . 6 (𝑤N → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
1110ad2antrl 482 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
12 simpr 109 . . . . . 6 ((((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) ∧ 𝑛 = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) → 𝑛 = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
1312breq2d 3945 . . . . 5 ((((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) ∧ 𝑛 = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) → (𝐴 < 𝑛𝐴 < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
1411, 13rspcedv 2794 . . . 4 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → (𝐴 < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛))
159, 14mpd 13 . . 3 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
164, 15rexlimddv 2555 . 2 ((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
172, 16rexlimddv 2555 1 (𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332   ∈ wcel 1481  {cab 2126  ∀wral 2417  ∃wrex 2418  ⟨cop 3531  ∩ cint 3775   class class class wbr 3933  (class class class)co 5778  1oc1o 6310  [cec 6431  Ncnpi 7100   ~Q ceq 7107
 Copyright terms: Public domain W3C validator