Theorem iseven 47733

Description: The predicate "is an even number". An even number is an integer which is divisible by 2, i.e. the result of dividing the even integer by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)

Assertion

Ref	Expression
iseven	⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))

Proof of Theorem iseven

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7359	. . 3 ⊢ (𝑧 = 𝑍 → (𝑧 / 2) = (𝑍 / 2))
2	1	eleq1d 2816	. 2 ⊢ (𝑧 = 𝑍 → ((𝑧 / 2) ∈ ℤ ↔ (𝑍 / 2) ∈ ℤ))
3		df-even 47731	. 2 ⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
4	2, 3	elrab2 3645	1 ⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  (class class class)co 7352   / cdiv 11780  2c2 12186  ℤcz 12474   Even ceven 47729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6443  df-fv 6495  df-ov 7355  df-even 47731

This theorem is referenced by:  evenz  47735  evendiv2z  47737  evenm1odd  47744  evenp1odd  47745  oddp1eveni  47746  oddm1eveni  47747  evennodd  47748  oddneven  47749  enege  47750  zeoALTV  47775  oddm1evenALTV  47780  oddp1evenALTV  47781  0evenALTV  47793  2evenALTV  47797  6even  47816  8even  47818