Theorem z4even

Description: 2 divides 4. That means 4 is even. (Contributed by AV, 23-Jul-2020) (Revised by AV, 4-Jul-2021)

	Ref	Expression
Assertion	z4even	⊢ 2 ∥ 4

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		dvdsmul1	⊢ ( ( 2 ∈ ℤ ∧ 2 ∈ ℤ ) → 2 ∥ ( 2 · 2 ) )
3	1 1 2	mp2an	⊢ 2 ∥ ( 2 · 2 )
4		2t2e4	⊢ ( 2 · 2 ) = 4
5	3 4	breqtri	⊢ 2 ∥ 4