Metamath Proof Explorer

Theorem dfceil2

Description: Alternative definition of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018)

Ref Expression
Assertion dfceil2 ⊢ . = x ∈ ℝ ⟼ ι y ∈ ℤ | x ≤ y ∧ y < x + 1

Proof

Step Hyp Ref Expression
1 df-ceil ⊢ . = x ∈ ℝ ⟼ − − x
2 zre ⊢ z ∈ ℤ → z ∈ ℝ
3 lenegcon2 ⊢ x ∈ ℝ ∧ z ∈ ℝ → x ≤ − z ↔ z ≤ − x
4 peano2re ⊢ x ∈ ℝ → x + 1 ∈ ℝ
5 4 anim1ci ⊢ x ∈ ℝ ∧ z ∈ ℝ → z ∈ ℝ ∧ x + 1 ∈ ℝ
6 ltnegcon1 ⊢ z ∈ ℝ ∧ x + 1 ∈ ℝ → − z < x + 1 ↔ − x + 1 < z
7 5 6 syl ⊢ x ∈ ℝ ∧ z ∈ ℝ → − z < x + 1 ↔ − x + 1 < z
8 recn ⊢ x ∈ ℝ → x ∈ ℂ
9 1cnd ⊢ x ∈ ℝ → 1 ∈ ℂ
10 8 9 negdid ⊢ x ∈ ℝ → − x + 1 = - x + -1
11 10 adantr ⊢ x ∈ ℝ ∧ z ∈ ℝ → − x + 1 = - x + -1
12 11 breq1d ⊢ x ∈ ℝ ∧ z ∈ ℝ → − x + 1 < z ↔ - x + -1 < z
13 renegcl ⊢ x ∈ ℝ → − x ∈ ℝ
14 13 adantr ⊢ x ∈ ℝ ∧ z ∈ ℝ → − x ∈ ℝ
15 neg1rr ⊢ − 1 ∈ ℝ
16 15 a1i ⊢ x ∈ ℝ ∧ z ∈ ℝ → − 1 ∈ ℝ
17 simpr ⊢ x ∈ ℝ ∧ z ∈ ℝ → z ∈ ℝ
18 14 16 17 ltaddsubd ⊢ x ∈ ℝ ∧ z ∈ ℝ → - x + -1 < z ↔ − x < z − -1
19 recn ⊢ z ∈ ℝ → z ∈ ℂ
20 1cnd ⊢ z ∈ ℝ → 1 ∈ ℂ
21 19 20 subnegd ⊢ z ∈ ℝ → z − -1 = z + 1
22 21 adantl ⊢ x ∈ ℝ ∧ z ∈ ℝ → z − -1 = z + 1
23 22 breq2d ⊢ x ∈ ℝ ∧ z ∈ ℝ → − x < z − -1 ↔ − x < z + 1
24 18 23 bitrd ⊢ x ∈ ℝ ∧ z ∈ ℝ → - x + -1 < z ↔ − x < z + 1
25 7 12 24 3bitrd ⊢ x ∈ ℝ ∧ z ∈ ℝ → − z < x + 1 ↔ − x < z + 1
26 3 25 anbi12d ⊢ x ∈ ℝ ∧ z ∈ ℝ → x ≤ − z ∧ − z < x + 1 ↔ z ≤ − x ∧ − x < z + 1
27 2 26 sylan2 ⊢ x ∈ ℝ ∧ z ∈ ℤ → x ≤ − z ∧ − z < x + 1 ↔ z ≤ − x ∧ − x < z + 1
28 27 riotabidva ⊢ x ∈ ℝ → ι z ∈ ℤ | x ≤ − z ∧ − z < x + 1 = ι z ∈ ℤ | z ≤ − x ∧ − x < z + 1
29 28 negeqd ⊢ x ∈ ℝ → − ι z ∈ ℤ | x ≤ − z ∧ − z < x + 1 = − ι z ∈ ℤ | z ≤ − x ∧ − x < z + 1
30 zbtwnre ⊢ x ∈ ℝ → ∃! y ∈ ℤ x ≤ y ∧ y < x + 1
31 breq2 ⊢ y = − z → x ≤ y ↔ x ≤ − z
32 breq1 ⊢ y = − z → y < x + 1 ↔ − z < x + 1
33 31 32 anbi12d ⊢ y = − z → x ≤ y ∧ y < x + 1 ↔ x ≤ − z ∧ − z < x + 1
34 33 zriotaneg ⊢ ∃! y ∈ ℤ x ≤ y ∧ y < x + 1 → ι y ∈ ℤ | x ≤ y ∧ y < x + 1 = − ι z ∈ ℤ | x ≤ − z ∧ − z < x + 1
35 30 34 syl ⊢ x ∈ ℝ → ι y ∈ ℤ | x ≤ y ∧ y < x + 1 = − ι z ∈ ℤ | x ≤ − z ∧ − z < x + 1
36 flval ⊢ − x ∈ ℝ → − x = ι z ∈ ℤ | z ≤ − x ∧ − x < z + 1
37 13 36 syl ⊢ x ∈ ℝ → − x = ι z ∈ ℤ | z ≤ − x ∧ − x < z + 1
38 37 negeqd ⊢ x ∈ ℝ → − − x = − ι z ∈ ℤ | z ≤ − x ∧ − x < z + 1
39 29 35 38 3eqtr4rd ⊢ x ∈ ℝ → − − x = ι y ∈ ℤ | x ≤ y ∧ y < x + 1
40 39 mpteq2ia ⊢ x ∈ ℝ ⟼ − − x = x ∈ ℝ ⟼ ι y ∈ ℤ | x ≤ y ∧ y < x + 1
41 1 40 eqtri ⊢ . = x ∈ ℝ ⟼ ι y ∈ ℤ | x ≤ y ∧ y < x + 1