Theorem evenz 48729

Description: An even number is an integer. (Contributed by AV, 14-Jun-2020.)

Assertion

Ref	Expression
evenz	⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ)

Proof of Theorem evenz

Step	Hyp	Ref	Expression
1		iseven 48727	. 2 ⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))
2	1	simplbi 502	1 ⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7421   / cdiv 11974  2c2 12398  ℤcz 12694   Even ceven 48723

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3900  df-un 3902  df-ss 3915  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6495  df-fv 6547  df-ov 7424  df-even 48725

This theorem is used by:  evenm1odd  48738  evenp1odd  48739  bits0eALTV  48779  opeoALTV  48783  omeoALTV  48785  epoo  48802  emoo  48803  epee  48804  emee  48805  evensumeven  48806  evenltle  48816  even3prm2  48818  mogoldbblem  48819  sbgoldbalt  48880  sgoldbeven3prm  48882  mogoldbb  48884  bgoldbachlt  48912  tgblthelfgott  48914