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 ⌈ = ( 𝑥 ∈ ℝ ↦ ( ℩ 𝑦 ∈ ℤ ( 𝑥 ≤ 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) ) )

Proof

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