Theorem arch 12531

Description: Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed by NM, 21-Jan-1997.)

Assertion

Ref	Expression
arch	⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ℕ 𝐴 < 𝑛)

Distinct variable group:   𝐴,𝑛

Proof of Theorem arch

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5159	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 < 𝑛 ↔ 𝐴 < 𝑛))
2	1	rexbidv 3172	. 2 ⊢ (𝑦 = 𝐴 → (∃𝑛 ∈ ℕ 𝑦 < 𝑛 ↔ ∃𝑛 ∈ ℕ 𝐴 < 𝑛))
3		nnunb 12530	. . . 4 ⊢ ¬ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦)
4		ralnex 3065	. . . 4 ⊢ (∀𝑦 ∈ ℝ ¬ ∀𝑛 ∈ ℕ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦) ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦))
5	3, 4	mpbir 230	. . 3 ⊢ ∀𝑦 ∈ ℝ ¬ ∀𝑛 ∈ ℕ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦)
6		rexnal 3093	. . . . 5 ⊢ (∃𝑛 ∈ ℕ ¬ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦) ↔ ¬ ∀𝑛 ∈ ℕ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦))
7		nnre 12281	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
8		axlttri 11342	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑦 < 𝑛 ↔ ¬ (𝑦 = 𝑛 ∨ 𝑛 < 𝑦)))
9	7, 8	sylan2 591	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑦 < 𝑛 ↔ ¬ (𝑦 = 𝑛 ∨ 𝑛 < 𝑦)))
10		equcom 2014	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 ↔ 𝑛 = 𝑦)
11	10	orbi1i 911	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑛 ∨ 𝑛 < 𝑦) ↔ (𝑛 = 𝑦 ∨ 𝑛 < 𝑦))
12		orcom 868	. . . . . . . . . 10 ⊢ ((𝑛 = 𝑦 ∨ 𝑛 < 𝑦) ↔ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦))
13	11, 12	bitri 274	. . . . . . . . 9 ⊢ ((𝑦 = 𝑛 ∨ 𝑛 < 𝑦) ↔ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦))
14	13	notbii 319	. . . . . . . 8 ⊢ (¬ (𝑦 = 𝑛 ∨ 𝑛 < 𝑦) ↔ ¬ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦))
15	9, 14	bitrdi 286	. . . . . . 7 ⊢ ((𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑦 < 𝑛 ↔ ¬ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦)))
16	15	biimprd 247	. . . . . 6 ⊢ ((𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (¬ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦) → 𝑦 < 𝑛))
17	16	reximdva 3161	. . . . 5 ⊢ (𝑦 ∈ ℝ → (∃𝑛 ∈ ℕ ¬ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 < 𝑛))
18	6, 17	biimtrrid 242	. . . 4 ⊢ (𝑦 ∈ ℝ → (¬ ∀𝑛 ∈ ℕ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 < 𝑛))
19	18	ralimia 3073	. . 3 ⊢ (∀𝑦 ∈ ℝ ¬ ∀𝑛 ∈ ℕ (𝑛 < 𝑦 ∨ 𝑛 = 𝑦) → ∀𝑦 ∈ ℝ ∃𝑛 ∈ ℕ 𝑦 < 𝑛)
20	5, 19	ax-mp 5	. 2 ⊢ ∀𝑦 ∈ ℝ ∃𝑛 ∈ ℕ 𝑦 < 𝑛
21	2, 20	vtoclri 3588	1 ⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ℕ 𝐴 < 𝑛)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1534   ∈ wcel 2100  ∀wral 3054  ∃wrex 3063   class class class wbr 5156  ℝcr 11164   < clt 11305  ℕcn 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-mulcom 11229  ax-addass 11230  ax-mulass 11231  ax-distr 11232  ax-i2m1 11233  ax-1ne0 11234  ax-1rid 11235  ax-rnegex 11236  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240  ax-pre-ltadd 11241  ax-pre-mulgt0 11242  ax-pre-sup 11243

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-pss 3979  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-iun 5008  df-br 5157  df-opab 5219  df-mpt 5240  df-tr 5274  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5641  df-we 5643  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-pred 6317  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7386  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7885  df-2nd 8012  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311  df-sub 11503  df-neg 11504  df-nn 12275

This theorem is referenced by:  nnrecl  12532  bndndx  12533  btwnz  12727  uzwo3  12989  zmin  12990  rpnnen1lem5  13027  harmonic  15884  alzdvds  16343  ovolicc2lem4  25563  volsup2  25648  ismbf3d  25697  mbfi1fseqlem6  25764  itg2seq  25786  itg2cnlem1  25805  ply1divex  26187  plydivex  26348  lgamucov  27089  lgamcvg2  27106  ubthlem1  30826  lnconi  31989  rearchi  33252  esumcst  33934  hbtlem5  42851  prmunb2  44047  rfcnnnub  44697  archd  44828  stoweidlem14  45696  stoweidlem60  45742  sge0rpcpnf  46103  hoicvr  46230  fsupdm  46524