Step |
Hyp |
Ref |
Expression |
1 |
|
1re |
⊢ 1 ∈ ℝ |
2 |
|
3re |
⊢ 3 ∈ ℝ |
3 |
2
|
rehalfcli |
⊢ ( 3 / 2 ) ∈ ℝ |
4 |
|
2cn |
⊢ 2 ∈ ℂ |
5 |
4
|
mulid2i |
⊢ ( 1 · 2 ) = 2 |
6 |
|
2lt3 |
⊢ 2 < 3 |
7 |
5 6
|
eqbrtri |
⊢ ( 1 · 2 ) < 3 |
8 |
|
2pos |
⊢ 0 < 2 |
9 |
|
2re |
⊢ 2 ∈ ℝ |
10 |
1 2 9
|
ltmuldivi |
⊢ ( 0 < 2 → ( ( 1 · 2 ) < 3 ↔ 1 < ( 3 / 2 ) ) ) |
11 |
8 10
|
ax-mp |
⊢ ( ( 1 · 2 ) < 3 ↔ 1 < ( 3 / 2 ) ) |
12 |
7 11
|
mpbi |
⊢ 1 < ( 3 / 2 ) |
13 |
1 3 12
|
ltleii |
⊢ 1 ≤ ( 3 / 2 ) |
14 |
|
3lt4 |
⊢ 3 < 4 |
15 |
|
2t2e4 |
⊢ ( 2 · 2 ) = 4 |
16 |
14 15
|
breqtrri |
⊢ 3 < ( 2 · 2 ) |
17 |
9 8
|
pm3.2i |
⊢ ( 2 ∈ ℝ ∧ 0 < 2 ) |
18 |
|
ltdivmul |
⊢ ( ( 3 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 3 / 2 ) < 2 ↔ 3 < ( 2 · 2 ) ) ) |
19 |
2 9 17 18
|
mp3an |
⊢ ( ( 3 / 2 ) < 2 ↔ 3 < ( 2 · 2 ) ) |
20 |
16 19
|
mpbir |
⊢ ( 3 / 2 ) < 2 |
21 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
22 |
20 21
|
breqtri |
⊢ ( 3 / 2 ) < ( 1 + 1 ) |
23 |
|
1z |
⊢ 1 ∈ ℤ |
24 |
|
flbi |
⊢ ( ( ( 3 / 2 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ ( 3 / 2 ) ) = 1 ↔ ( 1 ≤ ( 3 / 2 ) ∧ ( 3 / 2 ) < ( 1 + 1 ) ) ) ) |
25 |
3 23 24
|
mp2an |
⊢ ( ( ⌊ ‘ ( 3 / 2 ) ) = 1 ↔ ( 1 ≤ ( 3 / 2 ) ∧ ( 3 / 2 ) < ( 1 + 1 ) ) ) |
26 |
13 22 25
|
mpbir2an |
⊢ ( ⌊ ‘ ( 3 / 2 ) ) = 1 |
27 |
9
|
renegcli |
⊢ - 2 ∈ ℝ |
28 |
3
|
renegcli |
⊢ - ( 3 / 2 ) ∈ ℝ |
29 |
3 9
|
ltnegi |
⊢ ( ( 3 / 2 ) < 2 ↔ - 2 < - ( 3 / 2 ) ) |
30 |
20 29
|
mpbi |
⊢ - 2 < - ( 3 / 2 ) |
31 |
27 28 30
|
ltleii |
⊢ - 2 ≤ - ( 3 / 2 ) |
32 |
4
|
negcli |
⊢ - 2 ∈ ℂ |
33 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
34 |
|
negdi2 |
⊢ ( ( - 2 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( - 2 + 1 ) = ( - - 2 − 1 ) ) |
35 |
32 33 34
|
mp2an |
⊢ - ( - 2 + 1 ) = ( - - 2 − 1 ) |
36 |
4
|
negnegi |
⊢ - - 2 = 2 |
37 |
36
|
oveq1i |
⊢ ( - - 2 − 1 ) = ( 2 − 1 ) |
38 |
35 37
|
eqtri |
⊢ - ( - 2 + 1 ) = ( 2 − 1 ) |
39 |
|
2m1e1 |
⊢ ( 2 − 1 ) = 1 |
40 |
39 12
|
eqbrtri |
⊢ ( 2 − 1 ) < ( 3 / 2 ) |
41 |
38 40
|
eqbrtri |
⊢ - ( - 2 + 1 ) < ( 3 / 2 ) |
42 |
27 1
|
readdcli |
⊢ ( - 2 + 1 ) ∈ ℝ |
43 |
42 3
|
ltnegcon1i |
⊢ ( - ( - 2 + 1 ) < ( 3 / 2 ) ↔ - ( 3 / 2 ) < ( - 2 + 1 ) ) |
44 |
41 43
|
mpbi |
⊢ - ( 3 / 2 ) < ( - 2 + 1 ) |
45 |
|
2z |
⊢ 2 ∈ ℤ |
46 |
|
znegcl |
⊢ ( 2 ∈ ℤ → - 2 ∈ ℤ ) |
47 |
45 46
|
ax-mp |
⊢ - 2 ∈ ℤ |
48 |
|
flbi |
⊢ ( ( - ( 3 / 2 ) ∈ ℝ ∧ - 2 ∈ ℤ ) → ( ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 ↔ ( - 2 ≤ - ( 3 / 2 ) ∧ - ( 3 / 2 ) < ( - 2 + 1 ) ) ) ) |
49 |
28 47 48
|
mp2an |
⊢ ( ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 ↔ ( - 2 ≤ - ( 3 / 2 ) ∧ - ( 3 / 2 ) < ( - 2 + 1 ) ) ) |
50 |
31 44 49
|
mpbir2an |
⊢ ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 |
51 |
26 50
|
pm3.2i |
⊢ ( ( ⌊ ‘ ( 3 / 2 ) ) = 1 ∧ ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 ) |