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+12
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+12=2⋅ N2+12
15 10 11 13 14 syl3anc ⊢N∈ℤ→2⋅ N+12=2⋅ N2+12
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⋅ N2=N
21 20 oveq1d ⊢N∈ℤ→2⋅ N2+12=N+12
22 15 21 eqtrd ⊢N∈ℤ→2⋅ N+12=N+12
23 22 breq2d ⊢N∈ℤ→0≤2⋅ N+12↔0≤N+12
24 zre ⊢N∈ℤ→N∈ℝ
25 halfre ⊢12∈ℝ
26 25 a1i ⊢N∈ℤ→12∈ℝ
27 24 26 readdcld ⊢N∈ℤ→N+12∈ℝ
28 halfge0 ⊢0≤12
29 24 26 addge01d ⊢N∈ℤ→0≤12↔N≤N+12
30 28 29 mpbii ⊢N∈ℤ→N≤N+12
31 1red ⊢N∈ℤ→1∈ℝ
32 halflt1 ⊢12<1
33 32 a1i ⊢N∈ℤ→12<1
34 26 31 24 33 ltadd2dd ⊢N∈ℤ→N+12<N+1
35 btwnzge0 ⊢N+12∈ℝ∧N∈ℤ∧N≤N+12∧N+12<N+1→0≤N+12↔0≤N
36 27 3 30 34 35 syl22anc ⊢N∈ℤ→0≤N+12↔0≤N
37 9 23 36 3bitrd ⊢N∈ℤ→0≤2⋅ N+1↔0≤N