MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  odd2np1 Structured version   Visualization version   GIF version

Theorem odd2np1 16223
Description: An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
odd2np1 (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
Distinct variable group:   𝑛,𝑁

Proof of Theorem odd2np1
Dummy variables 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2z 12535 . . . 4 2 ∈ ℤ
2 divides 16138 . . . 4 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
31, 2mpan 688 . . 3 (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
43notbid 317 . 2 (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
5 elznn0 12514 . . . 4 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
6 odd2np1lem 16222 . . . . . 6 (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
76adantl 482 . . . . 5 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
8 peano2z 12544 . . . . . . . . . . 11 (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℤ)
9 znegcl 12538 . . . . . . . . . . 11 ((𝑥 + 1) ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
108, 9syl 17 . . . . . . . . . 10 (𝑥 ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
1110ad2antlr 725 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → -(𝑥 + 1) ∈ ℤ)
12 zcn 12504 . . . . . . . . . . . . . 14 (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
13 2cn 12228 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
14 mulcl 11135 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
1513, 14mpan 688 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
16 peano2cn 11327 . . . . . . . . . . . . . . 15 ((2 · 𝑥) ∈ ℂ → ((2 · 𝑥) + 1) ∈ ℂ)
1715, 16syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((2 · 𝑥) + 1) ∈ ℂ)
1812, 17syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) ∈ ℂ)
1918adantl 482 . . . . . . . . . . . 12 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((2 · 𝑥) + 1) ∈ ℂ)
20 simpl 483 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℝ)
2120recnd 11183 . . . . . . . . . . . 12 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℂ)
22 negcon2 11454 . . . . . . . . . . . 12 ((((2 · 𝑥) + 1) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 · 𝑥) + 1) = -𝑁𝑁 = -((2 · 𝑥) + 1)))
2319, 21, 22syl2anc 584 . . . . . . . . . . 11 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁𝑁 = -((2 · 𝑥) + 1)))
24 eqcom 2743 . . . . . . . . . . . 12 (𝑁 = -((2 · 𝑥) + 1) ↔ -((2 · 𝑥) + 1) = 𝑁)
2513, 12, 14sylancr 587 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → (2 · 𝑥) ∈ ℂ)
26 ax-1cn 11109 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
2713, 26mulcli 11162 . . . . . . . . . . . . . . . . . . . 20 (2 · 1) ∈ ℂ
28 addsubass 11411 . . . . . . . . . . . . . . . . . . . 20 (((2 · 𝑥) ∈ ℂ ∧ (2 · 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
2927, 26, 28mp3an23 1453 . . . . . . . . . . . . . . . . . . 19 ((2 · 𝑥) ∈ ℂ → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
3025, 29syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
31 2t1e2 12316 . . . . . . . . . . . . . . . . . . . . 21 (2 · 1) = 2
3231oveq1i 7367 . . . . . . . . . . . . . . . . . . . 20 ((2 · 1) − 1) = (2 − 1)
33 2m1e1 12279 . . . . . . . . . . . . . . . . . . . 20 (2 − 1) = 1
3432, 33eqtri 2764 . . . . . . . . . . . . . . . . . . 19 ((2 · 1) − 1) = 1
3534oveq2i 7368 . . . . . . . . . . . . . . . . . 18 ((2 · 𝑥) + ((2 · 1) − 1)) = ((2 · 𝑥) + 1)
3630, 35eqtr2di 2793 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = (((2 · 𝑥) + (2 · 1)) − 1))
37 adddi 11140 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
3813, 26, 37mp3an13 1452 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
3912, 38syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
4039oveq1d 7372 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℤ → ((2 · (𝑥 + 1)) − 1) = (((2 · 𝑥) + (2 · 1)) − 1))
4136, 40eqtr4d 2779 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = ((2 · (𝑥 + 1)) − 1))
4241negeqd 11395 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = -((2 · (𝑥 + 1)) − 1))
438zcnd 12608 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℂ)
44 mulneg2 11592 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
4513, 43, 44sylancr 587 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℤ → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
4645oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = (-(2 · (𝑥 + 1)) + 1))
47 mulcl 11135 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · (𝑥 + 1)) ∈ ℂ)
4813, 43, 47sylancr 587 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) ∈ ℂ)
49 negsubdi 11457 . . . . . . . . . . . . . . . . 17 (((2 · (𝑥 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
5048, 26, 49sylancl 586 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
5146, 50eqtr4d 2779 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = -((2 · (𝑥 + 1)) − 1))
5242, 51eqtr4d 2779 . . . . . . . . . . . . . 14 (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
5352adantl 482 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
5453eqeq1d 2738 . . . . . . . . . . . 12 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-((2 · 𝑥) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
5524, 54bitrid 282 . . . . . . . . . . 11 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑁 = -((2 · 𝑥) + 1) ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
5623, 55bitrd 278 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
5756biimpa 477 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → ((2 · -(𝑥 + 1)) + 1) = 𝑁)
58 oveq2 7365 . . . . . . . . . . . 12 (𝑛 = -(𝑥 + 1) → (2 · 𝑛) = (2 · -(𝑥 + 1)))
5958oveq1d 7372 . . . . . . . . . . 11 (𝑛 = -(𝑥 + 1) → ((2 · 𝑛) + 1) = ((2 · -(𝑥 + 1)) + 1))
6059eqeq1d 2738 . . . . . . . . . 10 (𝑛 = -(𝑥 + 1) → (((2 · 𝑛) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
6160rspcev 3581 . . . . . . . . 9 ((-(𝑥 + 1) ∈ ℤ ∧ ((2 · -(𝑥 + 1)) + 1) = 𝑁) → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)
6211, 57, 61syl2anc 584 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)
6362rexlimdva2 3154 . . . . . . 7 (𝑁 ∈ ℝ → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
64 znegcl 12538 . . . . . . . . . 10 (𝑦 ∈ ℤ → -𝑦 ∈ ℤ)
6564ad2antlr 725 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → -𝑦 ∈ ℤ)
66 zcn 12504 . . . . . . . . . . . . 13 (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
67 mulcl 11135 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑦 · 2) ∈ ℂ)
6866, 13, 67sylancl 586 . . . . . . . . . . . 12 (𝑦 ∈ ℤ → (𝑦 · 2) ∈ ℂ)
69 recn 11141 . . . . . . . . . . . 12 (𝑁 ∈ ℝ → 𝑁 ∈ ℂ)
70 negcon2 11454 . . . . . . . . . . . 12 (((𝑦 · 2) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑦 · 2) = -𝑁𝑁 = -(𝑦 · 2)))
7168, 69, 70syl2anr 597 . . . . . . . . . . 11 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁𝑁 = -(𝑦 · 2)))
72 eqcom 2743 . . . . . . . . . . . 12 (𝑁 = -(𝑦 · 2) ↔ -(𝑦 · 2) = 𝑁)
73 mulneg1 11591 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (-𝑦 · 2) = -(𝑦 · 2))
7466, 13, 73sylancl 586 . . . . . . . . . . . . . 14 (𝑦 ∈ ℤ → (-𝑦 · 2) = -(𝑦 · 2))
7574adantl 482 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (-𝑦 · 2) = -(𝑦 · 2))
7675eqeq1d 2738 . . . . . . . . . . . 12 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((-𝑦 · 2) = 𝑁 ↔ -(𝑦 · 2) = 𝑁))
7772, 76bitr4id 289 . . . . . . . . . . 11 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑁 = -(𝑦 · 2) ↔ (-𝑦 · 2) = 𝑁))
7871, 77bitrd 278 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ (-𝑦 · 2) = 𝑁))
7978biimpa 477 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → (-𝑦 · 2) = 𝑁)
80 oveq1 7364 . . . . . . . . . . 11 (𝑘 = -𝑦 → (𝑘 · 2) = (-𝑦 · 2))
8180eqeq1d 2738 . . . . . . . . . 10 (𝑘 = -𝑦 → ((𝑘 · 2) = 𝑁 ↔ (-𝑦 · 2) = 𝑁))
8281rspcev 3581 . . . . . . . . 9 ((-𝑦 ∈ ℤ ∧ (-𝑦 · 2) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
8365, 79, 82syl2anc 584 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
8483rexlimdva2 3154 . . . . . . 7 (𝑁 ∈ ℝ → (∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
8563, 84orim12d 963 . . . . . 6 (𝑁 ∈ ℝ → ((∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
86 odd2np1lem 16222 . . . . . 6 (-𝑁 ∈ ℕ0 → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁))
8785, 86impel 506 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
887, 87jaodan 956 . . . 4 ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
895, 88sylbi 216 . . 3 (𝑁 ∈ ℤ → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
90 halfnz 12581 . . . 4 ¬ (1 / 2) ∈ ℤ
91 reeanv 3217 . . . . 5 (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
92 eqtr3 2762 . . . . . . 7 ((((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → ((2 · 𝑛) + 1) = (𝑘 · 2))
93 zcn 12504 . . . . . . . . . . 11 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
94 mulcom 11137 . . . . . . . . . . 11 ((𝑘 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑘 · 2) = (2 · 𝑘))
9593, 13, 94sylancl 586 . . . . . . . . . 10 (𝑘 ∈ ℤ → (𝑘 · 2) = (2 · 𝑘))
9695eqeq2d 2747 . . . . . . . . 9 (𝑘 ∈ ℤ → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
9796adantl 482 . . . . . . . 8 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
98 mulcl 11135 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
9913, 93, 98sylancr 587 . . . . . . . . . 10 (𝑘 ∈ ℤ → (2 · 𝑘) ∈ ℂ)
100 zcn 12504 . . . . . . . . . . 11 (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
101 mulcl 11135 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
10213, 100, 101sylancr 587 . . . . . . . . . 10 (𝑛 ∈ ℤ → (2 · 𝑛) ∈ ℂ)
103 subadd 11404 . . . . . . . . . . 11 (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
10426, 103mp3an3 1450 . . . . . . . . . 10 (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
10599, 102, 104syl2anr 597 . . . . . . . . 9 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
106 subcl 11400 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑘𝑛) ∈ ℂ)
107 2cnne0 12363 . . . . . . . . . . . . . . 15 (2 ∈ ℂ ∧ 2 ≠ 0)
108 eqcom 2743 . . . . . . . . . . . . . . . 16 ((𝑘𝑛) = (1 / 2) ↔ (1 / 2) = (𝑘𝑛))
109 divmul 11816 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ (𝑘𝑛) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) = (𝑘𝑛) ↔ (2 · (𝑘𝑛)) = 1))
110108, 109bitrid 282 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ (𝑘𝑛) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑘𝑛) = (1 / 2) ↔ (2 · (𝑘𝑛)) = 1))
11126, 107, 110mp3an13 1452 . . . . . . . . . . . . . 14 ((𝑘𝑛) ∈ ℂ → ((𝑘𝑛) = (1 / 2) ↔ (2 · (𝑘𝑛)) = 1))
112106, 111syl 17 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑘𝑛) = (1 / 2) ↔ (2 · (𝑘𝑛)) = 1))
113112ancoms 459 . . . . . . . . . . . 12 ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘𝑛) = (1 / 2) ↔ (2 · (𝑘𝑛)) = 1))
114 subdi 11588 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
11513, 114mp3an1 1448 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
116115ancoms 459 . . . . . . . . . . . . 13 ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · (𝑘𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
117116eqeq1d 2738 . . . . . . . . . . . 12 ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((2 · (𝑘𝑛)) = 1 ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
118113, 117bitrd 278 . . . . . . . . . . 11 ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
119100, 93, 118syl2an 596 . . . . . . . . . 10 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
120 zsubcl 12545 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘𝑛) ∈ ℤ)
121 eleq1 2825 . . . . . . . . . . . 12 ((𝑘𝑛) = (1 / 2) → ((𝑘𝑛) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
122120, 121syl5ibcom 244 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑘𝑛) = (1 / 2) → (1 / 2) ∈ ℤ))
123122ancoms 459 . . . . . . . . . 10 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘𝑛) = (1 / 2) → (1 / 2) ∈ ℤ))
124119, 123sylbird 259 . . . . . . . . 9 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 → (1 / 2) ∈ ℤ))
125105, 124sylbird 259 . . . . . . . 8 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (2 · 𝑘) → (1 / 2) ∈ ℤ))
12697, 125sylbid 239 . . . . . . 7 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (𝑘 · 2) → (1 / 2) ∈ ℤ))
12792, 126syl5 34 . . . . . 6 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ))
128127rexlimivv 3196 . . . . 5 (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
12991, 128sylbir 234 . . . 4 ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
13090, 129mto 196 . . 3 ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
131 pm5.17 1010 . . . 4 (((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
132 bicom 221 . . . 4 ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ↔ (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
133131, 132bitri 274 . . 3 (((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) ↔ (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
13489, 130, 133sylanblc 589 . 2 (𝑁 ∈ ℤ → (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
1354, 134bitrd 278 1 (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wrex 3073   class class class wbr 5105  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  cmin 11385  -cneg 11386   / cdiv 11812  2c2 12208  0cn0 12413  cz 12499  cdvds 16136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-n0 12414  df-z 12500  df-dvds 16137
This theorem is referenced by:  oddm1even  16225  oexpneg  16227  mod2eq1n2dvds  16229  oddnn02np1  16230  2tp1odd  16234  sqoddm1div8z  16236  ltoddhalfle  16243  halfleoddlt  16244  opoe  16245  omoe  16246  opeo  16247  omeo  16248  m1expo  16257  m1exp1  16258  flodddiv4  16295  iserodd  16707  lgsquadlem1  26728  knoppndvlem9  34983  coskpi2  44097  cosknegpi  44100  stirlinglem5  44309  fourierswlem  44461  fmtnoodd  45715  dfodd3  45832
  Copyright terms: Public domain W3C validator