This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝑋 (,) +∞ ) 𝑘 ∈ 𝑍 )