![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > iseven | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
iseven | ⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 7431 | . . 3 ⊢ (𝑧 = 𝑍 → (𝑧 / 2) = (𝑍 / 2)) | |
2 | 1 | eleq1d 2811 | . 2 ⊢ (𝑧 = 𝑍 → ((𝑧 / 2) ∈ ℤ ↔ (𝑍 / 2) ∈ ℤ)) |
3 | df-even 47198 | . 2 ⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ} | |
4 | 2, 3 | elrab2 3684 | 1 ⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2099 (class class class)co 7424 / cdiv 11921 2c2 12319 ℤcz 12610 Even ceven 47196 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-iota 6506 df-fv 6562 df-ov 7427 df-even 47198 |
This theorem is referenced by: evenz 47202 evendiv2z 47204 evenm1odd 47211 evenp1odd 47212 oddp1eveni 47213 oddm1eveni 47214 evennodd 47215 oddneven 47216 enege 47217 zeoALTV 47242 oddm1evenALTV 47247 oddp1evenALTV 47248 0evenALTV 47260 2evenALTV 47264 6even 47283 8even 47285 |
Copyright terms: Public domain | W3C validator |