Theorem uzubioo

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

	Ref	Expression
Hypotheses	uzubioo.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	uzubioo.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	uzubioo.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
Assertion	uzubioo	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝑋 (,) +∞ ) 𝑘 ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		uzubioo.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		uzubioo.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		uzubioo.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4	3	rexrd	⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
5		pnfxr	⊢ +∞ ∈ ℝ*
6	5	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
7	3	ceilcld	⊢ ( 𝜑 → ( ⌈ ‘ 𝑋 ) ∈ ℤ )
8		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
9	7 8	zaddcld	⊢ ( 𝜑 → ( ( ⌈ ‘ 𝑋 ) + 1 ) ∈ ℤ )
10	9	zred	⊢ ( 𝜑 → ( ( ⌈ ‘ 𝑋 ) + 1 ) ∈ ℝ )
11	1	zred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
12	10 11	ifcld	⊢ ( 𝜑 → if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) ∈ ℝ )
13	7	zred	⊢ ( 𝜑 → ( ⌈ ‘ 𝑋 ) ∈ ℝ )
14	3	ceilged	⊢ ( 𝜑 → 𝑋 ≤ ( ⌈ ‘ 𝑋 ) )
15	13	ltp1d	⊢ ( 𝜑 → ( ⌈ ‘ 𝑋 ) < ( ( ⌈ ‘ 𝑋 ) + 1 ) )
16	3 13 10 14 15	lelttrd	⊢ ( 𝜑 → 𝑋 < ( ( ⌈ ‘ 𝑋 ) + 1 ) )
17	11 10	max2d	⊢ ( 𝜑 → ( ( ⌈ ‘ 𝑋 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) )
18	3 10 12 16 17	ltletrd	⊢ ( 𝜑 → 𝑋 < if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) )
19	12	ltpnfd	⊢ ( 𝜑 → if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) < +∞ )
20	4 6 12 18 19	eliood	⊢ ( 𝜑 → if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) ∈ ( 𝑋 (,) +∞ ) )
21	9 1	ifcld	⊢ ( 𝜑 → if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) ∈ ℤ )
22		max1	⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌈ ‘ 𝑋 ) + 1 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) )
23	11 10 22	syl2anc	⊢ ( 𝜑 → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) )
24	2 1 21 23	eluzd	⊢ ( 𝜑 → if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) ∈ 𝑍 )
25		eleq1	⊢ ( 𝑘 = if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) → ( 𝑘 ∈ 𝑍 ↔ if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) ∈ 𝑍 ) )
26	25	rspcev	⊢ ( ( if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) ∈ ( 𝑋 (,) +∞ ) ∧ if ( 𝑀 ≤ ( ( ⌈ ‘ 𝑋 ) + 1 ) , ( ( ⌈ ‘ 𝑋 ) + 1 ) , 𝑀 ) ∈ 𝑍 ) → ∃ 𝑘 ∈ ( 𝑋 (,) +∞ ) 𝑘 ∈ 𝑍 )
27	20 24 26	syl2anc	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝑋 (,) +∞ ) 𝑘 ∈ 𝑍 )