Metamath Proof Explorer

Theorem 2tnp1ge0ge0

Description: Two times an integer plus one is not negative iff the integer is not negative. (Contributed by AV, 19-Jun-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion 2tnp1ge0ge0 ( 𝑁 ∈ ℤ → ( 0 ≤ ( ( 2 · 𝑁 ) + 1 ) ↔ 0 ≤ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℤ )
3 id ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℤ )
4 2 3 zmulcld ⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℤ )
5 4 peano2zd ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ )
6 5 zred ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
7 2rp ⊢ 2 ∈ ℝ+
8 7 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℝ+ )
9 6 8 ge0divd ⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ ( ( 2 · 𝑁 ) + 1 ) ↔ 0 ≤ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ) )
10 4 zcnd ⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℂ )
11 1cnd ⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℂ )
12 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
13 12 a1i ⊢ ( 𝑁 ∈ ℤ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
14 divdir ⊢ ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( ( ( 2 · 𝑁 ) / 2 ) + ( 1 / 2 ) ) )
15 10 11 13 14 syl3anc ⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( ( ( 2 · 𝑁 ) / 2 ) + ( 1 / 2 ) ) )
16 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
17 2cnd ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
18 2ne0 ⊢ 2 ≠ 0
19 18 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ≠ 0 )
20 16 17 19 divcan3d ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) / 2 ) = 𝑁 )
21 20 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑁 ) / 2 ) + ( 1 / 2 ) ) = ( 𝑁 + ( 1 / 2 ) ) )
22 15 21 eqtrd ⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( 𝑁 + ( 1 / 2 ) ) )
23 22 breq2d ⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ↔ 0 ≤ ( 𝑁 + ( 1 / 2 ) ) ) )
24 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
25 halfre ⊢ ( 1 / 2 ) ∈ ℝ
26 25 a1i ⊢ ( 𝑁 ∈ ℤ → ( 1 / 2 ) ∈ ℝ )
27 24 26 readdcld ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
28 halfge0 ⊢ 0 ≤ ( 1 / 2 )
29 24 26 addge01d ⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ ( 1 / 2 ) ↔ 𝑁 ≤ ( 𝑁 + ( 1 / 2 ) ) ) )
30 28 29 mpbii ⊢ ( 𝑁 ∈ ℤ → 𝑁 ≤ ( 𝑁 + ( 1 / 2 ) ) )
31 1red ⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℝ )
32 halflt1 ⊢ ( 1 / 2 ) < 1
33 32 a1i ⊢ ( 𝑁 ∈ ℤ → ( 1 / 2 ) < 1 )
34 26 31 24 33 ltadd2dd ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + ( 1 / 2 ) ) < ( 𝑁 + 1 ) )
35 btwnzge0 ⊢ ( ( ( ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≤ ( 𝑁 + ( 1 / 2 ) ) ∧ ( 𝑁 + ( 1 / 2 ) ) < ( 𝑁 + 1 ) ) ) → ( 0 ≤ ( 𝑁 + ( 1 / 2 ) ) ↔ 0 ≤ 𝑁 ) )
36 27 3 30 34 35 syl22anc ⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ ( 𝑁 + ( 1 / 2 ) ) ↔ 0 ≤ 𝑁 ) )
37 9 23 36 3bitrd ⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ ( ( 2 · 𝑁 ) + 1 ) ↔ 0 ≤ 𝑁 ) )