Theorem iseven 47632

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 7360	. . 3 ⊢ (𝑧 = 𝑍 → (𝑧 / 2) = (𝑍 / 2))
2	1	eleq1d 2813	. 2 ⊢ (𝑧 = 𝑍 → ((𝑧 / 2) ∈ ℤ ↔ (𝑍 / 2) ∈ ℤ))
3		df-even 47630	. 2 ⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
4	2, 3	elrab2 3653	1 ⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7353   / cdiv 11796  2c2 12202  ℤcz 12490   Even ceven 47628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-even 47630

This theorem is referenced by:  evenz  47634  evendiv2z  47636  evenm1odd  47643  evenp1odd  47644  oddp1eveni  47645  oddm1eveni  47646  evennodd  47647  oddneven  47648  enege  47649  zeoALTV  47674  oddm1evenALTV  47679  oddp1evenALTV  47680  0evenALTV  47692  2evenALTV  47696  6even  47715  8even  47717