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