Theorem uzubioo

Description: The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	uzubioo.1	$$⊢\phi \to M\in \mathbb{Z}$$
	uzubioo.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	uzubioo.3	$$⊢\phi \to X\in ℝ$$
Assertion	uzubioo	$$⊢\phi \to \exists k\in \left(X,\mathrm{+\infty }\right)k\in Z$$

Proof

Step	Hyp	Ref	Expression
1		uzubioo.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		uzubioo.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		uzubioo.3	$$⊢\phi \to X\in ℝ$$
4	3	rexrd	$$⊢\phi \to X\in {ℝ}^{*}$$
5		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
6	5	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
7	3	ceilcld	$$⊢\phi \to ⌈X⌉\in \mathbb{Z}$$
8		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
9	7 8	zaddcld	$$⊢\phi \to ⌈X⌉+1\in \mathbb{Z}$$
10	9	zred	$$⊢\phi \to ⌈X⌉+1\in ℝ$$
11	1	zred	$$⊢\phi \to M\in ℝ$$
12	10 11	ifcld	$$⊢\phi \to if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)\in ℝ$$
13	7	zred	$$⊢\phi \to ⌈X⌉\in ℝ$$
14	3	ceilged	$$⊢\phi \to X\le ⌈X⌉$$
15	13	ltp1d	$$⊢\phi \to ⌈X⌉<⌈X⌉+1$$
16	3 13 10 14 15	lelttrd	$$⊢\phi \to X<⌈X⌉+1$$
17	11 10	max2d	$$⊢\phi \to ⌈X⌉+1\le if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)$$
18	3 10 12 16 17	ltletrd	$$⊢\phi \to X<if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)$$
19	12	ltpnfd	$$⊢\phi \to if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)<\mathrm{+\infty }$$
20	4 6 12 18 19	eliood	$$⊢\phi \to if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)\in \left(X,\mathrm{+\infty }\right)$$
21	9 1	ifcld	$$⊢\phi \to if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)\in \mathbb{Z}$$
22		max1	$$⊢\left(M\in ℝ\wedge ⌈X⌉+1\in ℝ\right)\to M\le if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)$$
23	11 10 22	syl2anc	$$⊢\phi \to M\le if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)$$
24	2 1 21 23	eluzd	$$⊢\phi \to if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)\in Z$$
25		eleq1	$$⊢k=if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)\to \left(k\in Z\leftrightarrow if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)\in Z\right)$$
26	25	rspcev	$$⊢\left(if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)\in \left(X,\mathrm{+\infty }\right)\wedge if\left(M\le ⌈X⌉+1,⌈X⌉+1,M\right)\in Z\right)\to \exists k\in \left(X,\mathrm{+\infty }\right)k\in Z$$
27	20 24 26	syl2anc	$$⊢\phi \to \exists k\in \left(X,\mathrm{+\infty }\right)k\in Z$$