Metamath Proof Explorer

Theorem div4p1lem1div2

Description: An integer greater than 5, divided by 4 and increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021)

Ref Expression
Assertion div4p1lem1div2 
|- ( ( N e. RR /\ 6 <_ N ) -> ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 6re 
 |-  6 e. RR
2 1 a1i 
 |-  ( N e. RR -> 6 e. RR )
3 id 
 |-  ( N e. RR -> N e. RR )
4 2 3 3 leadd2d 
 |-  ( N e. RR -> ( 6 <_ N <-> ( N + 6 ) <_ ( N + N ) ) )
5 4 biimpa 
 |-  ( ( N e. RR /\ 6 <_ N ) -> ( N + 6 ) <_ ( N + N ) )
6 recn 
 |-  ( N e. RR -> N e. CC )
7 6 times2d 
 |-  ( N e. RR -> ( N x. 2 ) = ( N + N ) )
8 7 adantr 
 |-  ( ( N e. RR /\ 6 <_ N ) -> ( N x. 2 ) = ( N + N ) )
9 5 8 breqtrrd 
 |-  ( ( N e. RR /\ 6 <_ N ) -> ( N + 6 ) <_ ( N x. 2 ) )
10 4cn 
 |-  4 e. CC
11 10 a1i 
 |-  ( N e. RR -> 4 e. CC )
12 2cn 
 |-  2 e. CC
13 12 a1i 
 |-  ( N e. RR -> 2 e. CC )
14 6 11 13 addassd 
 |-  ( N e. RR -> ( ( N + 4 ) + 2 ) = ( N + ( 4 + 2 ) ) )
15 4p2e6 
 |-  ( 4 + 2 ) = 6
16 15 oveq2i 
 |-  ( N + ( 4 + 2 ) ) = ( N + 6 )
17 14 16 eqtrdi 
 |-  ( N e. RR -> ( ( N + 4 ) + 2 ) = ( N + 6 ) )
18 17 breq1d 
 |-  ( N e. RR -> ( ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) <-> ( N + 6 ) <_ ( N x. 2 ) ) )
19 18 adantr 
 |-  ( ( N e. RR /\ 6 <_ N ) -> ( ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) <-> ( N + 6 ) <_ ( N x. 2 ) ) )
20 9 19 mpbird 
 |-  ( ( N e. RR /\ 6 <_ N ) -> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) )
21 4re 
 |-  4 e. RR
22 21 a1i 
 |-  ( N e. RR -> 4 e. RR )
23 4ne0 
 |-  4 =/= 0
24 23 a1i 
 |-  ( N e. RR -> 4 =/= 0 )
25 3 22 24 redivcld 
 |-  ( N e. RR -> ( N / 4 ) e. RR )
26 peano2re 
 |-  ( ( N / 4 ) e. RR -> ( ( N / 4 ) + 1 ) e. RR )
27 25 26 syl 
 |-  ( N e. RR -> ( ( N / 4 ) + 1 ) e. RR )
28 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
29 28 rehalfcld 
 |-  ( N e. RR -> ( ( N - 1 ) / 2 ) e. RR )
30 4pos 
 |-  0 < 4
31 21 30 pm3.2i 
 |-  ( 4 e. RR /\ 0 < 4 )
32 31 a1i 
 |-  ( N e. RR -> ( 4 e. RR /\ 0 < 4 ) )
33 lemul1 
 |-  ( ( ( ( N / 4 ) + 1 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( ( N / 4 ) + 1 ) x. 4 ) <_ ( ( ( N - 1 ) / 2 ) x. 4 ) ) )
34 27 29 32 33 syl3anc 
 |-  ( N e. RR -> ( ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( ( N / 4 ) + 1 ) x. 4 ) <_ ( ( ( N - 1 ) / 2 ) x. 4 ) ) )
35 25 recnd 
 |-  ( N e. RR -> ( N / 4 ) e. CC )
36 1cnd 
 |-  ( N e. RR -> 1 e. CC )
37 6 11 24 divcan1d 
 |-  ( N e. RR -> ( ( N / 4 ) x. 4 ) = N )
38 10 mullidi 
 |-  ( 1 x. 4 ) = 4
39 38 a1i 
 |-  ( N e. RR -> ( 1 x. 4 ) = 4 )
40 37 39 oveq12d 
 |-  ( N e. RR -> ( ( ( N / 4 ) x. 4 ) + ( 1 x. 4 ) ) = ( N + 4 ) )
41 35 11 36 40 joinlmuladdmuld 
 |-  ( N e. RR -> ( ( ( N / 4 ) + 1 ) x. 4 ) = ( N + 4 ) )
42 2t2e4 
 |-  ( 2 x. 2 ) = 4
43 42 eqcomi 
 |-  4 = ( 2 x. 2 )
44 43 a1i 
 |-  ( N e. RR -> 4 = ( 2 x. 2 ) )
45 44 oveq2d 
 |-  ( N e. RR -> ( ( ( N - 1 ) / 2 ) x. 4 ) = ( ( ( N - 1 ) / 2 ) x. ( 2 x. 2 ) ) )
46 29 recnd 
 |-  ( N e. RR -> ( ( N - 1 ) / 2 ) e. CC )
47 mulass 
 |-  ( ( ( ( N - 1 ) / 2 ) e. CC /\ 2 e. CC /\ 2 e. CC ) -> ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) = ( ( ( N - 1 ) / 2 ) x. ( 2 x. 2 ) ) )
48 47 eqcomd 
 |-  ( ( ( ( N - 1 ) / 2 ) e. CC /\ 2 e. CC /\ 2 e. CC ) -> ( ( ( N - 1 ) / 2 ) x. ( 2 x. 2 ) ) = ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) )
49 46 13 13 48 syl3anc 
 |-  ( N e. RR -> ( ( ( N - 1 ) / 2 ) x. ( 2 x. 2 ) ) = ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) )
50 28 recnd 
 |-  ( N e. RR -> ( N - 1 ) e. CC )
51 2ne0 
 |-  2 =/= 0
52 51 a1i 
 |-  ( N e. RR -> 2 =/= 0 )
53 50 13 52 divcan1d 
 |-  ( N e. RR -> ( ( ( N - 1 ) / 2 ) x. 2 ) = ( N - 1 ) )
54 53 oveq1d 
 |-  ( N e. RR -> ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) = ( ( N - 1 ) x. 2 ) )
55 6 36 13 subdird 
 |-  ( N e. RR -> ( ( N - 1 ) x. 2 ) = ( ( N x. 2 ) - ( 1 x. 2 ) ) )
56 12 mullidi 
 |-  ( 1 x. 2 ) = 2
57 56 a1i 
 |-  ( N e. RR -> ( 1 x. 2 ) = 2 )
58 57 oveq2d 
 |-  ( N e. RR -> ( ( N x. 2 ) - ( 1 x. 2 ) ) = ( ( N x. 2 ) - 2 ) )
59 54 55 58 3eqtrd 
 |-  ( N e. RR -> ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) = ( ( N x. 2 ) - 2 ) )
60 45 49 59 3eqtrd 
 |-  ( N e. RR -> ( ( ( N - 1 ) / 2 ) x. 4 ) = ( ( N x. 2 ) - 2 ) )
61 41 60 breq12d 
 |-  ( N e. RR -> ( ( ( ( N / 4 ) + 1 ) x. 4 ) <_ ( ( ( N - 1 ) / 2 ) x. 4 ) <-> ( N + 4 ) <_ ( ( N x. 2 ) - 2 ) ) )
62 3 22 readdcld 
 |-  ( N e. RR -> ( N + 4 ) e. RR )
63 2re 
 |-  2 e. RR
64 63 a1i 
 |-  ( N e. RR -> 2 e. RR )
65 3 64 remulcld 
 |-  ( N e. RR -> ( N x. 2 ) e. RR )
66 leaddsub 
 |-  ( ( ( N + 4 ) e. RR /\ 2 e. RR /\ ( N x. 2 ) e. RR ) -> ( ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) <-> ( N + 4 ) <_ ( ( N x. 2 ) - 2 ) ) )
67 66 bicomd 
 |-  ( ( ( N + 4 ) e. RR /\ 2 e. RR /\ ( N x. 2 ) e. RR ) -> ( ( N + 4 ) <_ ( ( N x. 2 ) - 2 ) <-> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) ) )
68 62 64 65 67 syl3anc 
 |-  ( N e. RR -> ( ( N + 4 ) <_ ( ( N x. 2 ) - 2 ) <-> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) ) )
69 34 61 68 3bitrd 
 |-  ( N e. RR -> ( ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) ) )
70 69 adantr 
 |-  ( ( N e. RR /\ 6 <_ N ) -> ( ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) ) )
71 20 70 mpbird 
 |-  ( ( N e. RR /\ 6 <_ N ) -> ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) )