Metamath Proof Explorer


Theorem flnn0div2ge

Description: The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020)

Ref Expression
Assertion flnn0div2ge N 0 N 1 2 N 2

Proof

Step Hyp Ref Expression
1 nn0eo N 0 N 2 0 N + 1 2 0
2 nn0re N 0 N
3 peano2rem N N 1
4 2 3 syl N 0 N 1
5 4 adantl N 2 0 N 0 N 1
6 2 adantl N 2 0 N 0 N
7 2rp 2 +
8 7 a1i N 2 0 N 0 2 +
9 2 lem1d N 0 N 1 N
10 9 adantl N 2 0 N 0 N 1 N
11 5 6 8 10 lediv1dd N 2 0 N 0 N 1 2 N 2
12 nn0z N 2 0 N 2
13 flid N 2 N 2 = N 2
14 12 13 syl N 2 0 N 2 = N 2
15 14 adantr N 2 0 N 0 N 2 = N 2
16 11 15 breqtrrd N 2 0 N 0 N 1 2 N 2
17 16 ex N 2 0 N 0 N 1 2 N 2
18 nn0o N 0 N + 1 2 0 N 1 2 0
19 18 ex N 0 N + 1 2 0 N 1 2 0
20 nn0z N 1 2 0 N 1 2
21 20 adantl N 0 N 1 2 0 N 1 2
22 flid N 1 2 N 1 2 = N 1 2
23 21 22 syl N 0 N 1 2 0 N 1 2 = N 1 2
24 4 rehalfcld N 0 N 1 2
25 24 adantr N 0 N 1 2 0 N 1 2
26 2 rehalfcld N 0 N 2
27 26 adantr N 0 N 1 2 0 N 2
28 2re 2
29 2pos 0 < 2
30 28 29 pm3.2i 2 0 < 2
31 30 a1i N 0 2 0 < 2
32 lediv1 N 1 N 2 0 < 2 N 1 N N 1 2 N 2
33 4 2 31 32 syl3anc N 0 N 1 N N 1 2 N 2
34 9 33 mpbid N 0 N 1 2 N 2
35 34 adantr N 0 N 1 2 0 N 1 2 N 2
36 flwordi N 1 2 N 2 N 1 2 N 2 N 1 2 N 2
37 25 27 35 36 syl3anc N 0 N 1 2 0 N 1 2 N 2
38 23 37 eqbrtrrd N 0 N 1 2 0 N 1 2 N 2
39 38 ex N 0 N 1 2 0 N 1 2 N 2
40 19 39 syldc N + 1 2 0 N 0 N 1 2 N 2
41 17 40 jaoi N 2 0 N + 1 2 0 N 0 N 1 2 N 2
42 1 41 mpcom N 0 N 1 2 N 2