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 ⊢ N ∈ ℤ → 0 ≤ 2 ⋅ N + 1 ↔ 0 ≤ N

Proof

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