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

Theorem axarch 7022
 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 7991 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 7060. (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 6962 . . 3 (𝐴 ∈ ℝ ↔ ∃𝑧R𝑧, 0R⟩ = 𝐴)
21biimpi 117 . 2 (𝐴 ∈ ℝ → ∃𝑧R𝑧, 0R⟩ = 𝐴)
3 archsr 6923 . . . 4 (𝑧R → ∃𝑤N 𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
43ad2antrl 467 . . 3 ((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) → ∃𝑤N 𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
5 simplrr 496 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ⟨𝑧, 0R⟩ = 𝐴)
6 simprr 492 . . . . . 6 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → 𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
7 ltresr 6972 . . . . . 6 (⟨𝑧, 0R⟩ < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ↔ 𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
86, 7sylibr 141 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ⟨𝑧, 0R⟩ < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
95, 8eqbrtrrd 3813 . . . 4 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → 𝐴 < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
10 pitonn 6981 . . . . . 6 (𝑤N → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
1110ad2antrl 467 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
12 simpr 107 . . . . . 6 ((((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) ∧ 𝑛 = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) → 𝑛 = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
1312breq2d 3803 . . . . 5 ((((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) ∧ 𝑛 = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) → (𝐴 < 𝑛𝐴 < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
1411, 13rspcedv 2677 . . . 4 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → (𝐴 < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛))
159, 14mpd 13 . . 3 (((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤N𝑧 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑤, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
164, 15rexlimddv 2454 . 2 ((𝐴 ∈ ℝ ∧ (𝑧R ∧ ⟨𝑧, 0R⟩ = 𝐴)) → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
172, 16rexlimddv 2454 1 (𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   = wceq 1259   ∈ wcel 1409  {cab 2042  ∀wral 2323  ∃wrex 2324  ⟨cop 3405  ∩ cint 3642   class class class wbr 3791  (class class class)co 5539  1𝑜c1o 6024  [cec 6134  Ncnpi 6427   ~Q ceq 6434
 Copyright terms: Public domain W3C validator