Metamath Proof Explorer

Theorem flodddiv4t2lthalf

Description: The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion flodddiv4t2lthalf 
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( ( |_ ` ( N / 4 ) ) x. 2 ) < ( N / 2 ) )

Proof

Step Hyp Ref Expression
1 flodddiv4lt 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( |_ ` ( N / 4 ) ) < ( N / 4 ) )
2 zre 
 |-  ( N e. ZZ -> N e. RR )
3 4re 
 |-  4 e. RR
4 3 a1i 
 |-  ( N e. ZZ -> 4 e. RR )
5 4ne0 
 |-  4 =/= 0
6 5 a1i 
 |-  ( N e. ZZ -> 4 =/= 0 )
7 2 4 6 redivcld 
 |-  ( N e. ZZ -> ( N / 4 ) e. RR )
8 7 flcld 
 |-  ( N e. ZZ -> ( |_ ` ( N / 4 ) ) e. ZZ )
9 8 zred 
 |-  ( N e. ZZ -> ( |_ ` ( N / 4 ) ) e. RR )
10 2rp 
 |-  2 e. RR+
11 10 a1i 
 |-  ( N e. ZZ -> 2 e. RR+ )
12 9 7 11 ltmul1d 
 |-  ( N e. ZZ -> ( ( |_ ` ( N / 4 ) ) < ( N / 4 ) <-> ( ( |_ ` ( N / 4 ) ) x. 2 ) < ( ( N / 4 ) x. 2 ) ) )
13 12 adantr 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( ( |_ ` ( N / 4 ) ) < ( N / 4 ) <-> ( ( |_ ` ( N / 4 ) ) x. 2 ) < ( ( N / 4 ) x. 2 ) ) )
14 1 13 mpbid 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( ( |_ ` ( N / 4 ) ) x. 2 ) < ( ( N / 4 ) x. 2 ) )
15 zcn 
 |-  ( N e. ZZ -> N e. CC )
16 15 halfcld 
 |-  ( N e. ZZ -> ( N / 2 ) e. CC )
17 2cnd 
 |-  ( N e. ZZ -> 2 e. CC )
18 2ne0 
 |-  2 =/= 0
19 18 a1i 
 |-  ( N e. ZZ -> 2 =/= 0 )
20 16 17 19 divcan1d 
 |-  ( N e. ZZ -> ( ( ( N / 2 ) / 2 ) x. 2 ) = ( N / 2 ) )
21 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
22 21 a1i 
 |-  ( N e. ZZ -> ( 2 e. CC /\ 2 =/= 0 ) )
23 divdiv1 
 |-  ( ( N e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( N / 2 ) / 2 ) = ( N / ( 2 x. 2 ) ) )
24 15 22 22 23 syl3anc 
 |-  ( N e. ZZ -> ( ( N / 2 ) / 2 ) = ( N / ( 2 x. 2 ) ) )
25 2t2e4 
 |-  ( 2 x. 2 ) = 4
26 25 a1i 
 |-  ( N e. ZZ -> ( 2 x. 2 ) = 4 )
27 26 oveq2d 
 |-  ( N e. ZZ -> ( N / ( 2 x. 2 ) ) = ( N / 4 ) )
28 24 27 eqtrd 
 |-  ( N e. ZZ -> ( ( N / 2 ) / 2 ) = ( N / 4 ) )
29 28 oveq1d 
 |-  ( N e. ZZ -> ( ( ( N / 2 ) / 2 ) x. 2 ) = ( ( N / 4 ) x. 2 ) )
30 20 29 eqtr3d 
 |-  ( N e. ZZ -> ( N / 2 ) = ( ( N / 4 ) x. 2 ) )
31 30 adantr 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( N / 2 ) = ( ( N / 4 ) x. 2 ) )
32 14 31 breqtrrd 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( ( |_ ` ( N / 4 ) ) x. 2 ) < ( N / 2 ) )