Metamath Proof Explorer

Theorem ceilbi

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

Ref Expression
Assertion ceilbi ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( ⌈ ‘ 𝐴 ) = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 < ( 𝐴 + 1 ) ) ) )

Proof

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