Metamath Proof Explorer


Theorem 2teven

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

Ref Expression
Assertion 2teven AB=2A2B

Proof

Step Hyp Ref Expression
1 2z 2
2 dvdsmul1 2A22A
3 1 2 mpan A22A
4 3 adantr AB=2A22A
5 breq2 B=2A2B22A
6 5 adantl AB=2A2B22A
7 4 6 mpbird AB=2A2B