![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > oddz | Structured version Visualization version GIF version |
Description: An odd number is an integer. (Contributed by AV, 14-Jun-2020.) |
Ref | Expression |
---|---|
oddz | ⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isodd 47111 | . 2 ⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 + 1) / 2) ∈ ℤ)) | |
2 | 1 | simplbi 496 | 1 ⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 (class class class)co 7419 1c1 11146 + caddc 11148 / cdiv 11908 2c2 12305 ℤcz 12596 Odd codd 47107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-ov 7422 df-odd 47109 |
This theorem is referenced by: oddm1div2z 47116 oddp1eveni 47123 oddm1eveni 47124 m1expoddALTV 47130 2dvdsoddp1 47138 2dvdsoddm1 47139 zofldiv2ALTV 47144 oddflALTV 47145 gcd2odd1 47150 oexpnegALTV 47159 oexpnegnz 47160 bits0oALTV 47163 opoeALTV 47165 opeoALTV 47166 omoeALTV 47167 omeoALTV 47168 epoo 47185 emoo 47186 stgoldbwt 47258 sbgoldbwt 47259 sbgoldbst 47260 sbgoldbm 47266 bgoldbtbndlem1 47287 bgoldbtbndlem2 47288 bgoldbtbndlem3 47289 bgoldbtbndlem4 47290 bgoldbtbnd 47291 tgoldbach 47299 |
Copyright terms: Public domain | W3C validator |