![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > oddp1even | GIF version |
Description: An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
Ref | Expression |
---|---|
oddp1even | ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oddm1even 11149 | . 2 ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 − 1))) | |
2 | 2z 8776 | . . 3 ⊢ 2 ∈ ℤ | |
3 | peano2zm 8786 | . . 3 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ) | |
4 | dvdsadd 11113 | . . 3 ⊢ ((2 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (2 ∥ (𝑁 − 1) ↔ 2 ∥ (2 + (𝑁 − 1)))) | |
5 | 2, 3, 4 | sylancr 405 | . 2 ⊢ (𝑁 ∈ ℤ → (2 ∥ (𝑁 − 1) ↔ 2 ∥ (2 + (𝑁 − 1)))) |
6 | 2cnd 8493 | . . . . 5 ⊢ (𝑁 ∈ ℤ → 2 ∈ ℂ) | |
7 | zcn 8753 | . . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) | |
8 | 1cnd 7502 | . . . . 5 ⊢ (𝑁 ∈ ℤ → 1 ∈ ℂ) | |
9 | 6, 7, 8 | addsub12d 7814 | . . . 4 ⊢ (𝑁 ∈ ℤ → (2 + (𝑁 − 1)) = (𝑁 + (2 − 1))) |
10 | 2m1e1 8538 | . . . . 5 ⊢ (2 − 1) = 1 | |
11 | 10 | oveq2i 5663 | . . . 4 ⊢ (𝑁 + (2 − 1)) = (𝑁 + 1) |
12 | 9, 11 | syl6eq 2136 | . . 3 ⊢ (𝑁 ∈ ℤ → (2 + (𝑁 − 1)) = (𝑁 + 1)) |
13 | 12 | breq2d 3857 | . 2 ⊢ (𝑁 ∈ ℤ → (2 ∥ (2 + (𝑁 − 1)) ↔ 2 ∥ (𝑁 + 1))) |
14 | 1, 5, 13 | 3bitrd 212 | 1 ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1))) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 103 ∈ wcel 1438 class class class wbr 3845 (class class class)co 5652 1c1 7349 + caddc 7351 − cmin 7651 2c2 8471 ℤcz 8748 ∥ cdvds 11070 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 579 ax-in2 580 ax-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-13 1449 ax-14 1450 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-sep 3957 ax-pow 4009 ax-pr 4036 ax-un 4260 ax-setind 4353 ax-cnex 7434 ax-resscn 7435 ax-1cn 7436 ax-1re 7437 ax-icn 7438 ax-addcl 7439 ax-addrcl 7440 ax-mulcl 7441 ax-mulrcl 7442 ax-addcom 7443 ax-mulcom 7444 ax-addass 7445 ax-mulass 7446 ax-distr 7447 ax-i2m1 7448 ax-0lt1 7449 ax-1rid 7450 ax-0id 7451 ax-rnegex 7452 ax-precex 7453 ax-cnre 7454 ax-pre-ltirr 7455 ax-pre-ltwlin 7456 ax-pre-lttrn 7457 ax-pre-apti 7458 ax-pre-ltadd 7459 ax-pre-mulgt0 7460 ax-pre-mulext 7461 |
This theorem depends on definitions: df-bi 115 df-3or 925 df-3an 926 df-tru 1292 df-fal 1295 df-xor 1312 df-nf 1395 df-sb 1693 df-eu 1951 df-mo 1952 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ne 2256 df-nel 2351 df-ral 2364 df-rex 2365 df-reu 2366 df-rmo 2367 df-rab 2368 df-v 2621 df-sbc 2841 df-dif 3001 df-un 3003 df-in 3005 df-ss 3012 df-pw 3431 df-sn 3452 df-pr 3453 df-op 3455 df-uni 3654 df-int 3689 df-br 3846 df-opab 3900 df-id 4120 df-po 4123 df-iso 4124 df-xp 4444 df-rel 4445 df-cnv 4446 df-co 4447 df-dm 4448 df-iota 4980 df-fun 5017 df-fv 5023 df-riota 5608 df-ov 5655 df-oprab 5656 df-mpt2 5657 df-pnf 7522 df-mnf 7523 df-xr 7524 df-ltxr 7525 df-le 7526 df-sub 7653 df-neg 7654 df-reap 8050 df-ap 8057 df-div 8138 df-inn 8421 df-2 8479 df-n0 8672 df-z 8749 df-dvds 11071 |
This theorem is referenced by: zeo5 11162 oddp1d2 11164 n2dvdsm1 11187 2sqpwodd 11428 oddennn 11479 |
Copyright terms: Public domain | W3C validator |