Metamath Proof Explorer

Theorem ceilbi

Description: A condition equivalent to ceiling. Analogous to flbi . (Contributed by AV, 2-Nov-2025)

Ref Expression
Assertion ceilbi ⊢ A ∈ ℝ ∧ B ∈ ℤ → A = B ↔ A ≤ B ∧ B < A + 1

Proof

Step Hyp Ref Expression
1 ceilval ⊢ A ∈ ℝ → A = − − A
2 1 adantr ⊢ A ∈ ℝ ∧ B ∈ ℤ → A = − − A
3 2 eqeq1d ⊢ A ∈ ℝ ∧ B ∈ ℤ → A = B ↔ − − A = B
4 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
5 4 flcld ⊢ A ∈ ℝ → − A ∈ ℤ
6 5 zcnd ⊢ A ∈ ℝ → − A ∈ ℂ
7 zcn ⊢ B ∈ ℤ → B ∈ ℂ
8 negcon1 ⊢ − A ∈ ℂ ∧ B ∈ ℂ → − − A = B ↔ − B = − A
9 6 7 8 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℤ → − − A = B ↔ − B = − A
10 eqcom ⊢ − B = − A ↔ − A = − B
11 10 a1i ⊢ A ∈ ℝ ∧ B ∈ ℤ → − B = − A ↔ − A = − B
12 znegcl ⊢ B ∈ ℤ → − B ∈ ℤ
13 flbi ⊢ − A ∈ ℝ ∧ − B ∈ ℤ → − A = − B ↔ − B ≤ − A ∧ − A < - B + 1
14 4 12 13 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℤ → − A = − B ↔ − B ≤ − A ∧ − A < - B + 1
15 simpl ⊢ A ∈ ℝ ∧ B ∈ ℤ → A ∈ ℝ
16 zre ⊢ B ∈ ℤ → B ∈ ℝ
17 16 adantl ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ∈ ℝ
18 15 17 lenegd ⊢ A ∈ ℝ ∧ B ∈ ℤ → A ≤ B ↔ − B ≤ − A
19 18 bicomd ⊢ A ∈ ℝ ∧ B ∈ ℤ → − B ≤ − A ↔ A ≤ B
20 peano2rem ⊢ B ∈ ℝ → B − 1 ∈ ℝ
21 16 20 syl ⊢ B ∈ ℤ → B − 1 ∈ ℝ
22 21 adantl ⊢ A ∈ ℝ ∧ B ∈ ℤ → B − 1 ∈ ℝ
23 22 15 ltnegd ⊢ A ∈ ℝ ∧ B ∈ ℤ → B − 1 < A ↔ − A < − B − 1
24 1red ⊢ A ∈ ℝ ∧ B ∈ ℤ → 1 ∈ ℝ
25 17 24 15 ltsubaddd ⊢ A ∈ ℝ ∧ B ∈ ℤ → B − 1 < A ↔ B < A + 1
26 1cnd ⊢ A ∈ ℝ → 1 ∈ ℂ
27 negsubdi ⊢ B ∈ ℂ ∧ 1 ∈ ℂ → − B − 1 = - B + 1
28 7 26 27 syl2anr ⊢ A ∈ ℝ ∧ B ∈ ℤ → − B − 1 = - B + 1
29 28 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℤ → − A < − B − 1 ↔ − A < - B + 1
30 23 25 29 3bitr3rd ⊢ A ∈ ℝ ∧ B ∈ ℤ → − A < - B + 1 ↔ B < A + 1
31 19 30 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℤ → − B ≤ − A ∧ − A < - B + 1 ↔ A ≤ B ∧ B < A + 1
32 11 14 31 3bitrd ⊢ A ∈ ℝ ∧ B ∈ ℤ → − B = − A ↔ A ≤ B ∧ B < A + 1
33 3 9 32 3bitrd ⊢ A ∈ ℝ ∧ B ∈ ℤ → A = B ↔ A ≤ B ∧ B < A + 1