Metamath Proof Explorer

Theorem 2tp1odd

Description: A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021)

Ref Expression
Assertion 2tp1odd 
|- ( ( A e. ZZ /\ B = ( ( 2 x. A ) + 1 ) ) -> -. 2 || B )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. ZZ -> A e. ZZ )
2 oveq2 
 |-  ( k = A -> ( 2 x. k ) = ( 2 x. A ) )
3 2 oveq1d 
 |-  ( k = A -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. A ) + 1 ) )
4 3 eqeq1d 
 |-  ( k = A -> ( ( ( 2 x. k ) + 1 ) = ( ( 2 x. A ) + 1 ) <-> ( ( 2 x. A ) + 1 ) = ( ( 2 x. A ) + 1 ) ) )
5 4 adantl 
 |-  ( ( A e. ZZ /\ k = A ) -> ( ( ( 2 x. k ) + 1 ) = ( ( 2 x. A ) + 1 ) <-> ( ( 2 x. A ) + 1 ) = ( ( 2 x. A ) + 1 ) ) )
6 eqidd 
 |-  ( A e. ZZ -> ( ( 2 x. A ) + 1 ) = ( ( 2 x. A ) + 1 ) )
7 1 5 6 rspcedvd 
 |-  ( A e. ZZ -> E. k e. ZZ ( ( 2 x. k ) + 1 ) = ( ( 2 x. A ) + 1 ) )
8 2z 
 |-  2 e. ZZ
9 8 a1i 
 |-  ( A e. ZZ -> 2 e. ZZ )
10 9 1 zmulcld 
 |-  ( A e. ZZ -> ( 2 x. A ) e. ZZ )
11 10 peano2zd 
 |-  ( A e. ZZ -> ( ( 2 x. A ) + 1 ) e. ZZ )
12 odd2np1 
 |-  ( ( ( 2 x. A ) + 1 ) e. ZZ -> ( -. 2 || ( ( 2 x. A ) + 1 ) <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = ( ( 2 x. A ) + 1 ) ) )
13 11 12 syl 
 |-  ( A e. ZZ -> ( -. 2 || ( ( 2 x. A ) + 1 ) <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = ( ( 2 x. A ) + 1 ) ) )
14 7 13 mpbird 
 |-  ( A e. ZZ -> -. 2 || ( ( 2 x. A ) + 1 ) )
15 14 adantr 
 |-  ( ( A e. ZZ /\ B = ( ( 2 x. A ) + 1 ) ) -> -. 2 || ( ( 2 x. A ) + 1 ) )
16 breq2 
 |-  ( B = ( ( 2 x. A ) + 1 ) -> ( 2 || B <-> 2 || ( ( 2 x. A ) + 1 ) ) )
17 16 adantl 
 |-  ( ( A e. ZZ /\ B = ( ( 2 x. A ) + 1 ) ) -> ( 2 || B <-> 2 || ( ( 2 x. A ) + 1 ) ) )
18 15 17 mtbird 
 |-  ( ( A e. ZZ /\ B = ( ( 2 x. A ) + 1 ) ) -> -. 2 || B )