Metamath Proof Explorer

Theorem ltoddhalfle

Description: An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021)

Ref Expression
Assertion ltoddhalfle ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ ) → ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 odd2np1 ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
2 halfre ⊢ ( 1 / 2 ) ∈ ℝ
3 2 a1i ⊢ ( 𝑛 ∈ ℤ → ( 1 / 2 ) ∈ ℝ )
4 1red ⊢ ( 𝑛 ∈ ℤ → 1 ∈ ℝ )
5 zre ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
6 3 4 5 3jca ⊢ ( 𝑛 ∈ ℤ → ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
7 6 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
8 halflt1 ⊢ ( 1 / 2 ) < 1
9 axltadd ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 1 / 2 ) < 1 → ( 𝑛 + ( 1 / 2 ) ) < ( 𝑛 + 1 ) ) )
10 7 8 9 mpisyl ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑛 + ( 1 / 2 ) ) < ( 𝑛 + 1 ) )
11 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
12 11 adantl ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℝ )
13 5 3 readdcld ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 + ( 1 / 2 ) ) ∈ ℝ )
14 13 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑛 + ( 1 / 2 ) ) ∈ ℝ )
15 peano2z ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 + 1 ) ∈ ℤ )
16 15 zred ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 + 1 ) ∈ ℝ )
17 16 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑛 + 1 ) ∈ ℝ )
18 lttr ⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑛 + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑛 + 1 ) ∈ ℝ ) → ( ( 𝑀 < ( 𝑛 + ( 1 / 2 ) ) ∧ ( 𝑛 + ( 1 / 2 ) ) < ( 𝑛 + 1 ) ) → 𝑀 < ( 𝑛 + 1 ) ) )
19 12 14 17 18 syl3anc ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑀 < ( 𝑛 + ( 1 / 2 ) ) ∧ ( 𝑛 + ( 1 / 2 ) ) < ( 𝑛 + 1 ) ) → 𝑀 < ( 𝑛 + 1 ) ) )
20 10 19 mpan2d ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 < ( 𝑛 + ( 1 / 2 ) ) → 𝑀 < ( 𝑛 + 1 ) ) )
21 zleltp1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑀 ≤ 𝑛 ↔ 𝑀 < ( 𝑛 + 1 ) ) )
22 21 ancoms ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ≤ 𝑛 ↔ 𝑀 < ( 𝑛 + 1 ) ) )
23 20 22 sylibrd ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 < ( 𝑛 + ( 1 / 2 ) ) → 𝑀 ≤ 𝑛 ) )
24 halfgt0 ⊢ 0 < ( 1 / 2 )
25 3 5 jca ⊢ ( 𝑛 ∈ ℤ → ( ( 1 / 2 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
26 25 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 1 / 2 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
27 ltaddpos ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 0 < ( 1 / 2 ) ↔ 𝑛 < ( 𝑛 + ( 1 / 2 ) ) ) )
28 26 27 syl ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 0 < ( 1 / 2 ) ↔ 𝑛 < ( 𝑛 + ( 1 / 2 ) ) ) )
29 24 28 mpbii ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑛 < ( 𝑛 + ( 1 / 2 ) ) )
30 5 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑛 ∈ ℝ )
31 lelttr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 𝑛 + ( 1 / 2 ) ) ∈ ℝ ) → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 < ( 𝑛 + ( 1 / 2 ) ) ) → 𝑀 < ( 𝑛 + ( 1 / 2 ) ) ) )
32 12 30 14 31 syl3anc ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 < ( 𝑛 + ( 1 / 2 ) ) ) → 𝑀 < ( 𝑛 + ( 1 / 2 ) ) ) )
33 29 32 mpan2d ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ≤ 𝑛 → 𝑀 < ( 𝑛 + ( 1 / 2 ) ) ) )
34 23 33 impbid ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 < ( 𝑛 + ( 1 / 2 ) ) ↔ 𝑀 ≤ 𝑛 ) )
35 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
36 1cnd ⊢ ( 𝑛 ∈ ℤ → 1 ∈ ℂ )
37 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
38 37 a1i ⊢ ( 𝑛 ∈ ℤ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
39 muldivdir ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) = ( 𝑛 + ( 1 / 2 ) ) )
40 35 36 38 39 syl3anc ⊢ ( 𝑛 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) = ( 𝑛 + ( 1 / 2 ) ) )
41 40 breq2d ⊢ ( 𝑛 ∈ ℤ → ( 𝑀 < ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ↔ 𝑀 < ( 𝑛 + ( 1 / 2 ) ) ) )
42 41 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 < ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ↔ 𝑀 < ( 𝑛 + ( 1 / 2 ) ) ) )
43 2z ⊢ 2 ∈ ℤ
44 43 a1i ⊢ ( 𝑛 ∈ ℤ → 2 ∈ ℤ )
45 id ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℤ )
46 44 45 zmulcld ⊢ ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) ∈ ℤ )
47 46 zcnd ⊢ ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) ∈ ℂ )
48 47 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 2 · 𝑛 ) ∈ ℂ )
49 pncan1 ⊢ ( ( 2 · 𝑛 ) ∈ ℂ → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
50 48 49 syl ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
51 50 oveq1d ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) = ( ( 2 · 𝑛 ) / 2 ) )
52 2cnd ⊢ ( 𝑛 ∈ ℤ → 2 ∈ ℂ )
53 2ne0 ⊢ 2 ≠ 0
54 53 a1i ⊢ ( 𝑛 ∈ ℤ → 2 ≠ 0 )
55 35 52 54 divcan3d ⊢ ( 𝑛 ∈ ℤ → ( ( 2 · 𝑛 ) / 2 ) = 𝑛 )
56 55 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 2 · 𝑛 ) / 2 ) = 𝑛 )
57 51 56 eqtrd ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) = 𝑛 )
58 57 breq2d ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ≤ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ↔ 𝑀 ≤ 𝑛 ) )
59 34 42 58 3bitr4d ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 < ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ↔ 𝑀 ≤ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) )
60 oveq1 ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) = ( 𝑁 / 2 ) )
61 60 breq2d ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 < ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ↔ 𝑀 < ( 𝑁 / 2 ) ) )
62 oveq1 ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 𝑁 − 1 ) )
63 62 oveq1d ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) = ( ( 𝑁 − 1 ) / 2 ) )
64 63 breq2d ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 ≤ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
65 61 64 bibi12d ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( 𝑀 < ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ↔ 𝑀 ≤ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) ↔ ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) ) )
66 59 65 syl5ibcom ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) ) )
67 66 ex ⊢ ( 𝑛 ∈ ℤ → ( 𝑀 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
68 67 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑀 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
69 68 com23 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 ∈ ℤ → ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
70 69 rexlimdva ⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 ∈ ℤ → ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
71 1 70 sylbid ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 → ( 𝑀 ∈ ℤ → ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
72 71 3imp ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ ) → ( 𝑀 < ( 𝑁 / 2 ) ↔ 𝑀 ≤ ( ( 𝑁 − 1 ) / 2 ) ) )