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−12≤N2

Proof

Step Hyp Ref Expression
1 nn0eo ⊢N∈ℕ0→N2∈ℕ0∨N+12∈ℕ0
2 nn0re ⊢N∈ℕ0→N∈ℝ
3 peano2rem ⊢N∈ℝ→N−1∈ℝ
4 2 3 syl ⊢N∈ℕ0→N−1∈ℝ
5 4 adantl ⊢N2∈ℕ0∧N∈ℕ0→N−1∈ℝ
6 2 adantl ⊢N2∈ℕ0∧N∈ℕ0→N∈ℝ
7 2rp ⊢2∈ℝ+
8 7 a1i ⊢N2∈ℕ0∧N∈ℕ0→2∈ℝ+
9 2 lem1d ⊢N∈ℕ0→N−1≤N
10 9 adantl ⊢N2∈ℕ0∧N∈ℕ0→N−1≤N
11 5 6 8 10 lediv1dd ⊢N2∈ℕ0∧N∈ℕ0→N−12≤N2
12 nn0z ⊢N2∈ℕ0→N2∈ℤ
13 flid ⊢N2∈ℤ→N2=N2
14 12 13 syl ⊢N2∈ℕ0→N2=N2
15 14 adantr ⊢N2∈ℕ0∧N∈ℕ0→N2=N2
16 11 15 breqtrrd ⊢N2∈ℕ0∧N∈ℕ0→N−12≤N2
17 16 ex ⊢N2∈ℕ0→N∈ℕ0→N−12≤N2
18 nn0o ⊢N∈ℕ0∧N+12∈ℕ0→N−12∈ℕ0
19 18 ex ⊢N∈ℕ0→N+12∈ℕ0→N−12∈ℕ0
20 nn0z ⊢N−12∈ℕ0→N−12∈ℤ
21 20 adantl ⊢N∈ℕ0∧N−12∈ℕ0→N−12∈ℤ
22 flid ⊢N−12∈ℤ→N−12=N−12
23 21 22 syl ⊢N∈ℕ0∧N−12∈ℕ0→N−12=N−12
24 4 rehalfcld ⊢N∈ℕ0→N−12∈ℝ
25 24 adantr ⊢N∈ℕ0∧N−12∈ℕ0→N−12∈ℝ
26 2 rehalfcld ⊢N∈ℕ0→N2∈ℝ
27 26 adantr ⊢N∈ℕ0∧N−12∈ℕ0→N2∈ℝ
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−12≤N2
33 4 2 31 32 syl3anc ⊢N∈ℕ0→N−1≤N↔N−12≤N2
34 9 33 mpbid ⊢N∈ℕ0→N−12≤N2
35 34 adantr ⊢N∈ℕ0∧N−12∈ℕ0→N−12≤N2
36 flwordi ⊢N−12∈ℝ∧N2∈ℝ∧N−12≤N2→N−12≤N2
37 25 27 35 36 syl3anc ⊢N∈ℕ0∧N−12∈ℕ0→N−12≤N2
38 23 37 eqbrtrrd ⊢N∈ℕ0∧N−12∈ℕ0→N−12≤N2
39 38 ex ⊢N∈ℕ0→N−12∈ℕ0→N−12≤N2
40 19 39 syldc ⊢N+12∈ℕ0→N∈ℕ0→N−12≤N2
41 17 40 jaoi ⊢N2∈ℕ0∨N+12∈ℕ0→N∈ℕ0→N−12≤N2
42 1 41 mpcom ⊢N∈ℕ0→N−12≤N2