Metamath Proof Explorer


Theorem fldiv4lem1div2

Description: The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021)

Ref Expression
Assertion fldiv4lem1div2 N N 4 N 1 2

Proof

Step Hyp Ref Expression
1 elnn1uz2 N N = 1 N 2
2 1lt4 1 < 4
3 1nn0 1 0
4 4nn 4
5 divfl0 1 0 4 1 < 4 1 4 = 0
6 3 4 5 mp2an 1 < 4 1 4 = 0
7 2 6 mpbi 1 4 = 0
8 1re 1
9 4re 4
10 4ne0 4 0
11 redivcl 1 4 4 0 1 4
12 11 flcld 1 4 4 0 1 4
13 12 zred 1 4 4 0 1 4
14 8 9 10 13 mp3an 1 4
15 14 eqlei 1 4 = 0 1 4 0
16 7 15 mp1i N = 1 1 4 0
17 fvoveq1 N = 1 N 4 = 1 4
18 oveq1 N = 1 N 1 = 1 1
19 1m1e0 1 1 = 0
20 18 19 eqtrdi N = 1 N 1 = 0
21 20 oveq1d N = 1 N 1 2 = 0 2
22 2cnne0 2 2 0
23 div0 2 2 0 0 2 = 0
24 22 23 ax-mp 0 2 = 0
25 21 24 eqtrdi N = 1 N 1 2 = 0
26 16 17 25 3brtr4d N = 1 N 4 N 1 2
27 fldiv4lem1div2uz2 N 2 N 4 N 1 2
28 26 27 jaoi N = 1 N 2 N 4 N 1 2
29 1 28 sylbi N N 4 N 1 2