Theorem 2teven

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

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

Proof

Step	Hyp	Ref	Expression
1		2z	|- 2 e. ZZ
2		dvdsmul1	|- ( ( 2 e. ZZ /\ A e. ZZ ) -> 2 || ( 2 x. A ) )
3	1 2	mpan	|- ( A e. ZZ -> 2 || ( 2 x. A ) )
4	3	adantr	|- ( ( A e. ZZ /\ B = ( 2 x. A ) ) -> 2 || ( 2 x. A ) )
5		breq2	|- ( B = ( 2 x. A ) -> ( 2 || B <-> 2 || ( 2 x. A ) ) )
6	5	adantl	|- ( ( A e. ZZ /\ B = ( 2 x. A ) ) -> ( 2 || B <-> 2 || ( 2 x. A ) ) )
7	4 6	mpbird	|- ( ( A e. ZZ /\ B = ( 2 x. A ) ) -> 2 || B )