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 ) ) ) )