Metamath Proof Explorer

Theorem uzubioo

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

Ref Expression
Hypotheses uzubioo.1 ⊢ φ → M ∈ ℤ
uzubioo.2 ⊢ Z = ℤ ≥ M
uzubioo.3 ⊢ φ → X ∈ ℝ
Assertion uzubioo ⊢ φ → ∃ k ∈ X +∞ k ∈ Z

Proof

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