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