Theorem nnunb 12495

Description: The set of positive integers is unbounded above. Theorem I.28 of [Apostol] p. 26. (Contributed by NM, 21-Jan-1997.)

Assertion

Ref	Expression
nnunb	⊢ ¬ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)

Distinct variable group:   𝑥,𝑦

Proof of Theorem nnunb

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm3.24 407	. . . 4 ⊢ ¬ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦)
2		peano2rem 11520	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ)
3		ltm1 12052	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) < 𝑥)
4		ovex 7443	. . . . . . . . . . . . 13 ⊢ (𝑥 − 1) ∈ V
5		eleq1 2851	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 − 1) → (𝑦 ∈ ℝ ↔ (𝑥 − 1) ∈ ℝ))
6		breq1 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 − 1) → (𝑦 < 𝑥 ↔ (𝑥 − 1) < 𝑥))
7		breq1 5112	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑥 − 1) → (𝑦 < 𝑧 ↔ (𝑥 − 1) < 𝑧))
8	7	rexbidv 3189	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 − 1) → (∃𝑧 ∈ ℕ 𝑦 < 𝑧 ↔ ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))
9	6, 8	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 − 1) → ((𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) ↔ ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)))
10	5, 9	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 − 1) → ((𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) ↔ ((𝑥 − 1) ∈ ℝ → ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))))
11	4, 10	spcv 3564	. . . . . . . . . . . 12 ⊢ (∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ((𝑥 − 1) ∈ ℝ → ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)))
12	3, 11	syl7 75	. . . . . . . . . . 11 ⊢ (∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ((𝑥 − 1) ∈ ℝ → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)))
13	2, 12	syl5 35	. . . . . . . . . 10 ⊢ (∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)))
14	13	pm2.43d 54	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))
15		df-rex 3090	. . . . . . . . 9 ⊢ (∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧 ↔ ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧))
16	14, 15	imbitrdi 254	. . . . . . . 8 ⊢ (∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧)))
17	16	com12 33	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧)))
18		nnre 12235	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
19		1re 11203	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
20		ltsubadd 11679	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 − 1) < 𝑧 ↔ 𝑥 < (𝑧 + 1)))
21	19, 20	mp3an2 1478	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 − 1) < 𝑧 ↔ 𝑥 < (𝑧 + 1)))
22	18, 21	sylan2 604	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℕ) → ((𝑥 − 1) < 𝑧 ↔ 𝑥 < (𝑧 + 1)))
23	22	pm5.32da 589	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → ((𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) ↔ (𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1))))
24	23	exbidv 1951	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → (∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) ↔ ∃𝑧(𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1))))
25		peano2nn 12240	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈ ℕ)
26		ovex 7443	. . . . . . . . . . 11 ⊢ (𝑧 + 1) ∈ V
27		eleq1 2851	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑧 + 1) → (𝑦 ∈ ℕ ↔ (𝑧 + 1) ∈ ℕ))
28		breq2 5113	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑧 + 1) → (𝑥 < 𝑦 ↔ 𝑥 < (𝑧 + 1)))
29	27, 28	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑧 + 1) → ((𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) ↔ ((𝑧 + 1) ∈ ℕ ∧ 𝑥 < (𝑧 + 1))))
30	26, 29	spcev 3565	. . . . . . . . . 10 ⊢ (((𝑧 + 1) ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))
31	25, 30	sylan 591	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))
32	31	exlimiv 1960	. . . . . . . 8 ⊢ (∃𝑧(𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))
33	24, 32	biimtrdi 256	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)))
34	17, 33	syld 48	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)))
35		df-ral 3080	. . . . . 6 ⊢ (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)))
36		df-ral 3080	. . . . . . . 8 ⊢ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ↔ ∀𝑦(𝑦 ∈ ℕ → ¬ 𝑥 < 𝑦))
37		alinexa 1873	. . . . . . . 8 ⊢ (∀𝑦(𝑦 ∈ ℕ → ¬ 𝑥 < 𝑦) ↔ ¬ ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))
38	36, 37	bitr2i 279	. . . . . . 7 ⊢ (¬ ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) ↔ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦)
39	38	con1bii 359	. . . . . 6 ⊢ (¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ↔ ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))
40	34, 35, 39	3imtr4g 299	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) → ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦))
41	40	anim2d 623	. . . 4 ⊢ (𝑥 ∈ ℝ → ((∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦)))
42	1, 41	mtoi 202	. . 3 ⊢ (𝑥 ∈ ℝ → ¬ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)))
43	42	nrex 3093	. 2 ⊢ ¬ ∃𝑥 ∈ ℝ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))
44		nnssre 12232	. . 3 ⊢ ℕ ⊆ ℝ
45		1nn 12239	. . . 4 ⊢ 1 ∈ ℕ
46	45	ne0ii 4297	. . 3 ⊢ ℕ ≠ ∅
47		sup2 12166	. . 3 ⊢ ((ℕ ⊆ ℝ ∧ ℕ ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)))
48	44, 46, 47	mp3an12 1480	. 2 ⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)))
49	43, 48	mto 200	1 ⊢ ¬ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089   ⊆ wss 3905  ∅c0 4286   class class class wbr 5109  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098   < clt 11238   − cmin 11436  ℕcn 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229

This theorem is referenced by:  arch  12496