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 e. ZZ -> ( 0 <_ ( ( 2 x. N ) + 1 ) <-> 0 <_ N ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 1 a1i 
 |-  ( N e. ZZ -> 2 e. ZZ )
3 id 
 |-  ( N e. ZZ -> N e. ZZ )
4 2 3 zmulcld 
 |-  ( N e. ZZ -> ( 2 x. N ) e. ZZ )
5 4 peano2zd 
 |-  ( N e. ZZ -> ( ( 2 x. N ) + 1 ) e. ZZ )
6 5 zred 
 |-  ( N e. ZZ -> ( ( 2 x. N ) + 1 ) e. RR )
7 2rp 
 |-  2 e. RR+
8 7 a1i 
 |-  ( N e. ZZ -> 2 e. RR+ )
9 6 8 ge0divd 
 |-  ( N e. ZZ -> ( 0 <_ ( ( 2 x. N ) + 1 ) <-> 0 <_ ( ( ( 2 x. N ) + 1 ) / 2 ) ) )
10 4 zcnd 
 |-  ( N e. ZZ -> ( 2 x. N ) e. CC )
11 1cnd 
 |-  ( N e. ZZ -> 1 e. CC )
12 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
13 12 a1i 
 |-  ( N e. ZZ -> ( 2 e. CC /\ 2 =/= 0 ) )
14 divdir 
 |-  ( ( ( 2 x. N ) e. CC /\ 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( ( ( 2 x. N ) / 2 ) + ( 1 / 2 ) ) )
15 10 11 13 14 syl3anc 
 |-  ( N e. ZZ -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( ( ( 2 x. N ) / 2 ) + ( 1 / 2 ) ) )
16 zcn 
 |-  ( N e. ZZ -> N e. CC )
17 2cnd 
 |-  ( N e. ZZ -> 2 e. CC )
18 2ne0 
 |-  2 =/= 0
19 18 a1i 
 |-  ( N e. ZZ -> 2 =/= 0 )
20 16 17 19 divcan3d 
 |-  ( N e. ZZ -> ( ( 2 x. N ) / 2 ) = N )
21 20 oveq1d 
 |-  ( N e. ZZ -> ( ( ( 2 x. N ) / 2 ) + ( 1 / 2 ) ) = ( N + ( 1 / 2 ) ) )
22 15 21 eqtrd 
 |-  ( N e. ZZ -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( N + ( 1 / 2 ) ) )
23 22 breq2d 
 |-  ( N e. ZZ -> ( 0 <_ ( ( ( 2 x. N ) + 1 ) / 2 ) <-> 0 <_ ( N + ( 1 / 2 ) ) ) )
24 zre 
 |-  ( N e. ZZ -> N e. RR )
25 halfre 
 |-  ( 1 / 2 ) e. RR
26 25 a1i 
 |-  ( N e. ZZ -> ( 1 / 2 ) e. RR )
27 24 26 readdcld 
 |-  ( N e. ZZ -> ( N + ( 1 / 2 ) ) e. RR )
28 halfge0 
 |-  0 <_ ( 1 / 2 )
29 24 26 addge01d 
 |-  ( N e. ZZ -> ( 0 <_ ( 1 / 2 ) <-> N <_ ( N + ( 1 / 2 ) ) ) )
30 28 29 mpbii 
 |-  ( N e. ZZ -> N <_ ( N + ( 1 / 2 ) ) )
31 1red 
 |-  ( N e. ZZ -> 1 e. RR )
32 halflt1 
 |-  ( 1 / 2 ) < 1
33 32 a1i 
 |-  ( N e. ZZ -> ( 1 / 2 ) < 1 )
34 26 31 24 33 ltadd2dd 
 |-  ( N e. ZZ -> ( N + ( 1 / 2 ) ) < ( N + 1 ) )
35 btwnzge0 
 |-  ( ( ( ( N + ( 1 / 2 ) ) e. RR /\ N e. ZZ ) /\ ( N <_ ( N + ( 1 / 2 ) ) /\ ( N + ( 1 / 2 ) ) < ( N + 1 ) ) ) -> ( 0 <_ ( N + ( 1 / 2 ) ) <-> 0 <_ N ) )
36 27 3 30 34 35 syl22anc 
 |-  ( N e. ZZ -> ( 0 <_ ( N + ( 1 / 2 ) ) <-> 0 <_ N ) )
37 9 23 36 3bitrd 
 |-  ( N e. ZZ -> ( 0 <_ ( ( 2 x. N ) + 1 ) <-> 0 <_ N ) )