Theorem axarch 7925

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 8957 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 7965. (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.

Step	Hyp	Ref	Expression
1		elreal 7862	. . 3 ⊢ (𝐴 ∈ ℝ ↔ ∃𝑧 ∈ R ⟨𝑧, 0R⟩ = 𝐴)
2	1	biimpi 120	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑧 ∈ R ⟨𝑧, 0R⟩ = 𝐴)
3		archsr 7816	. . . 4 ⊢ (𝑧 ∈ R → ∃𝑤 ∈ N 𝑧 <R [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
4	3	ad2antrl 490	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ (𝑧 ∈ R ∧ ⟨𝑧, 0R⟩ = 𝐴)) → ∃𝑤 ∈ N 𝑧 <R [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
5		simplrr 536	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝑧 ∈ R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤 ∈ N ∧ 𝑧 <R [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ⟨𝑧, 0R⟩ = 𝐴)
6		simprr 531	. . . . . 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 7873	. . . . . 6 ⊢ (⟨𝑧, 0R⟩ <ℝ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ↔ 𝑧 <R [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
8	6, 7	sylibr 134	. . . . 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⟩)
9	5, 8	eqbrtrrd 4045	. . . 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 7882	. . . . . 6 ⊢ (𝑤 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
11	10	ad2antrl 490	. . . . 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 110	. . . . . 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⟩)
13	12	breq2d 4033	. . . . 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⟩))
14	11, 13	rspcedv 2860	. . . 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) ∈ 𝑥)}𝐴 <ℝ 𝑛))
15	9, 14	mpd 13	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ (𝑧 ∈ R ∧ ⟨𝑧, 0R⟩ = 𝐴)) ∧ (𝑤 ∈ N ∧ 𝑧 <R [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)
16	4, 15	rexlimddv 2612	. 2 ⊢ ((𝐴 ∈ ℝ ∧ (𝑧 ∈ R ∧ ⟨𝑧, 0R⟩ = 𝐴)) → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)
17	2, 16	rexlimddv 2612	1 ⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2160  {cab 2175  ∀wral 2468  ∃wrex 2469  ⟨cop 3613  ∩ cint 3862   class class class wbr 4021  (class class class)co 5900  1_oc1o 6438  [cec 6561  Ncnpi 7306   ~_Q ceq 7313   <_Q cltq 7319  1_Pc1p 7326   +_P cpp 7327   ~_R cer 7330  Rcnr 7331  0_Rc0r 7332   <_R cltr 7337  ℝcr 7845  1c1 7847   + caddc 7849   <_ℝ cltrr 7850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4136  ax-sep 4139  ax-nul 4147  ax-pow 4195  ax-pr 4230  ax-un 4454  ax-setind 4557  ax-iinf 4608

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-int 3863  df-iun 3906  df-br 4022  df-opab 4083  df-mpt 4084  df-tr 4120  df-eprel 4310  df-id 4314  df-po 4317  df-iso 4318  df-iord 4387  df-on 4389  df-suc 4392  df-iom 4611  df-xp 4653  df-rel 4654  df-cnv 4655  df-co 4656  df-dm 4657  df-rn 4658  df-res 4659  df-ima 4660  df-iota 5199  df-fun 5240  df-fn 5241  df-f 5242  df-f1 5243  df-fo 5244  df-f1o 5245  df-fv 5246  df-ov 5903  df-oprab 5904  df-mpo 5905  df-1st 6169  df-2nd 6170  df-recs 6334  df-irdg 6399  df-1o 6445  df-2o 6446  df-oadd 6449  df-omul 6450  df-er 6563  df-ec 6565  df-qs 6569  df-ni 7338  df-pli 7339  df-mi 7340  df-lti 7341  df-plpq 7378  df-mpq 7379  df-enq 7381  df-nqqs 7382  df-plqqs 7383  df-mqqs 7384  df-1nqqs 7385  df-rq 7386  df-ltnqqs 7387  df-enq0 7458  df-nq0 7459  df-0nq0 7460  df-plq0 7461  df-mq0 7462  df-inp 7500  df-i1p 7501  df-iplp 7502  df-iltp 7504  df-enr 7760  df-nr 7761  df-plr 7762  df-ltr 7764  df-0r 7765  df-1r 7766  df-c 7852  df-1 7854  df-r 7856  df-add 7857  df-lt 7859

This theorem is referenced by: (None)