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 ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )

Proof

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