Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  evenz Structured version   Visualization version   GIF version

Theorem evenz 47617
Description: An even number is an integer. (Contributed by AV, 14-Jun-2020.)
Assertion
Ref Expression
evenz (𝑍 ∈ Even → 𝑍 ∈ ℤ)

Proof of Theorem evenz
StepHypRef Expression
1 iseven 47615 . 2 (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))
21simplbi 497 1 (𝑍 ∈ Even → 𝑍 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  (class class class)co 7431   / cdiv 11920  2c2 12321  cz 12613   Even ceven 47611
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-even 47613
This theorem is referenced by:  evenm1odd  47626  evenp1odd  47627  bits0eALTV  47667  opeoALTV  47671  omeoALTV  47673  epoo  47690  emoo  47691  epee  47692  emee  47693  evensumeven  47694  evenltle  47704  even3prm2  47706  mogoldbblem  47707  sbgoldbalt  47768  sgoldbeven3prm  47770  mogoldbb  47772  bgoldbachlt  47800  tgblthelfgott  47802
  Copyright terms: Public domain W3C validator