ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  odd2np1 GIF version

Theorem odd2np1 11861
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 9270 . . . 4 2 ∈ ℤ
2 divides 11780 . . . 4 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
31, 2mpan 424 . . 3 (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
43notbid 667 . 2 (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
5 elznn0 9257 . . . 4 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
6 odd2np1lem 11860 . . . . . 6 (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
76adantl 277 . . . . 5 ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
8 odd2np1lem 11860 . . . . . . 7 (-𝑁 ∈ ℕ0 → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁))
9 peano2z 9278 . . . . . . . . . . . . 13 (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℤ)
10 znegcl 9273 . . . . . . . . . . . . 13 ((𝑥 + 1) ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
119, 10syl 14 . . . . . . . . . . . 12 (𝑥 ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
1211ad2antlr 489 . . . . . . . . . . 11 (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → -(𝑥 + 1) ∈ ℤ)
13 zcn 9247 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
14 2cn 8979 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
15 mulcl 7929 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
1614, 15mpan 424 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
17 peano2cn 8082 . . . . . . . . . . . . . . . . 17 ((2 · 𝑥) ∈ ℂ → ((2 · 𝑥) + 1) ∈ ℂ)
1816, 17syl 14 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → ((2 · 𝑥) + 1) ∈ ℂ)
1913, 18syl 14 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) ∈ ℂ)
2019adantl 277 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((2 · 𝑥) + 1) ∈ ℂ)
21 simpl 109 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℝ)
2221recnd 7976 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℂ)
23 negcon2 8200 . . . . . . . . . . . . . 14 ((((2 · 𝑥) + 1) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 · 𝑥) + 1) = -𝑁𝑁 = -((2 · 𝑥) + 1)))
2420, 22, 23syl2anc 411 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁𝑁 = -((2 · 𝑥) + 1)))
25 eqcom 2179 . . . . . . . . . . . . . 14 (𝑁 = -((2 · 𝑥) + 1) ↔ -((2 · 𝑥) + 1) = 𝑁)
2614, 13, 15sylancr 414 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℤ → (2 · 𝑥) ∈ ℂ)
27 ax-1cn 7895 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℂ
2814, 27mulcli 7953 . . . . . . . . . . . . . . . . . . . . . 22 (2 · 1) ∈ ℂ
29 addsubass 8157 . . . . . . . . . . . . . . . . . . . . . 22 (((2 · 𝑥) ∈ ℂ ∧ (2 · 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
3028, 27, 29mp3an23 1329 . . . . . . . . . . . . . . . . . . . . 21 ((2 · 𝑥) ∈ ℂ → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
3126, 30syl 14 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℤ → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
32 2t1e2 9061 . . . . . . . . . . . . . . . . . . . . . . 23 (2 · 1) = 2
3332oveq1i 5879 . . . . . . . . . . . . . . . . . . . . . 22 ((2 · 1) − 1) = (2 − 1)
34 2m1e1 9026 . . . . . . . . . . . . . . . . . . . . . 22 (2 − 1) = 1
3533, 34eqtri 2198 . . . . . . . . . . . . . . . . . . . . 21 ((2 · 1) − 1) = 1
3635oveq2i 5880 . . . . . . . . . . . . . . . . . . . 20 ((2 · 𝑥) + ((2 · 1) − 1)) = ((2 · 𝑥) + 1)
3731, 36eqtr2di 2227 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = (((2 · 𝑥) + (2 · 1)) − 1))
38 adddi 7934 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
3914, 27, 38mp3an13 1328 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
4013, 39syl 14 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
4140oveq1d 5884 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → ((2 · (𝑥 + 1)) − 1) = (((2 · 𝑥) + (2 · 1)) − 1))
4237, 41eqtr4d 2213 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = ((2 · (𝑥 + 1)) − 1))
4342negeqd 8142 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = -((2 · (𝑥 + 1)) − 1))
449zcnd 9365 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℂ)
45 mulneg2 8343 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
4614, 44, 45sylancr 414 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
4746oveq1d 5884 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = (-(2 · (𝑥 + 1)) + 1))
48 mulcl 7929 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · (𝑥 + 1)) ∈ ℂ)
4914, 44, 48sylancr 414 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) ∈ ℂ)
50 negsubdi 8203 . . . . . . . . . . . . . . . . . . 19 (((2 · (𝑥 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
5149, 27, 50sylancl 413 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
5247, 51eqtr4d 2213 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = -((2 · (𝑥 + 1)) − 1))
5343, 52eqtr4d 2213 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
5453adantl 277 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
5554eqeq1d 2186 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-((2 · 𝑥) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
5625, 55bitrid 192 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑁 = -((2 · 𝑥) + 1) ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
5724, 56bitrd 188 . . . . . . . . . . . 12 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
5857biimpa 296 . . . . . . . . . . 11 (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → ((2 · -(𝑥 + 1)) + 1) = 𝑁)
59 oveq2 5877 . . . . . . . . . . . . . 14 (𝑛 = -(𝑥 + 1) → (2 · 𝑛) = (2 · -(𝑥 + 1)))
6059oveq1d 5884 . . . . . . . . . . . . 13 (𝑛 = -(𝑥 + 1) → ((2 · 𝑛) + 1) = ((2 · -(𝑥 + 1)) + 1))
6160eqeq1d 2186 . . . . . . . . . . . 12 (𝑛 = -(𝑥 + 1) → (((2 · 𝑛) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
6261rspcev 2841 . . . . . . . . . . 11 ((-(𝑥 + 1) ∈ ℤ ∧ ((2 · -(𝑥 + 1)) + 1) = 𝑁) → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)
6312, 58, 62syl2anc 411 . . . . . . . . . 10 (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)
6463ex 115 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
6564rexlimdva 2594 . . . . . . . 8 (𝑁 ∈ ℝ → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
66 znegcl 9273 . . . . . . . . . . . 12 (𝑦 ∈ ℤ → -𝑦 ∈ ℤ)
6766ad2antlr 489 . . . . . . . . . . 11 (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → -𝑦 ∈ ℤ)
68 zcn 9247 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
69 mulcl 7929 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑦 · 2) ∈ ℂ)
7068, 14, 69sylancl 413 . . . . . . . . . . . . . 14 (𝑦 ∈ ℤ → (𝑦 · 2) ∈ ℂ)
71 recn 7935 . . . . . . . . . . . . . 14 (𝑁 ∈ ℝ → 𝑁 ∈ ℂ)
72 negcon2 8200 . . . . . . . . . . . . . 14 (((𝑦 · 2) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑦 · 2) = -𝑁𝑁 = -(𝑦 · 2)))
7370, 71, 72syl2anr 290 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁𝑁 = -(𝑦 · 2)))
74 eqcom 2179 . . . . . . . . . . . . . 14 (𝑁 = -(𝑦 · 2) ↔ -(𝑦 · 2) = 𝑁)
75 mulneg1 8342 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (-𝑦 · 2) = -(𝑦 · 2))
7668, 14, 75sylancl 413 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℤ → (-𝑦 · 2) = -(𝑦 · 2))
7776adantl 277 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (-𝑦 · 2) = -(𝑦 · 2))
7877eqeq1d 2186 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((-𝑦 · 2) = 𝑁 ↔ -(𝑦 · 2) = 𝑁))
7974, 78bitr4id 199 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑁 = -(𝑦 · 2) ↔ (-𝑦 · 2) = 𝑁))
8073, 79bitrd 188 . . . . . . . . . . . 12 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ (-𝑦 · 2) = 𝑁))
8180biimpa 296 . . . . . . . . . . 11 (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → (-𝑦 · 2) = 𝑁)
82 oveq1 5876 . . . . . . . . . . . . 13 (𝑘 = -𝑦 → (𝑘 · 2) = (-𝑦 · 2))
8382eqeq1d 2186 . . . . . . . . . . . 12 (𝑘 = -𝑦 → ((𝑘 · 2) = 𝑁 ↔ (-𝑦 · 2) = 𝑁))
8483rspcev 2841 . . . . . . . . . . 11 ((-𝑦 ∈ ℤ ∧ (-𝑦 · 2) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
8567, 81, 84syl2anc 411 . . . . . . . . . 10 (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
8685ex 115 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
8786rexlimdva 2594 . . . . . . . 8 (𝑁 ∈ ℝ → (∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
8865, 87orim12d 786 . . . . . . 7 (𝑁 ∈ ℝ → ((∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
898, 88syl5 32 . . . . . 6 (𝑁 ∈ ℝ → (-𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
9089imp 124 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
917, 90jaodan 797 . . . 4 ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
925, 91sylbi 121 . . 3 (𝑁 ∈ ℤ → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
93 halfnz 9338 . . . 4 ¬ (1 / 2) ∈ ℤ
94 reeanv 2646 . . . . 5 (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
95 eqtr3 2197 . . . . . . 7 ((((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → ((2 · 𝑛) + 1) = (𝑘 · 2))
96 zcn 9247 . . . . . . . . . . 11 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
97 mulcom 7931 . . . . . . . . . . 11 ((𝑘 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑘 · 2) = (2 · 𝑘))
9896, 14, 97sylancl 413 . . . . . . . . . 10 (𝑘 ∈ ℤ → (𝑘 · 2) = (2 · 𝑘))
9998eqeq2d 2189 . . . . . . . . 9 (𝑘 ∈ ℤ → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
10099adantl 277 . . . . . . . 8 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
101 mulcl 7929 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
10214, 96, 101sylancr 414 . . . . . . . . . 10 (𝑘 ∈ ℤ → (2 · 𝑘) ∈ ℂ)
103 zcn 9247 . . . . . . . . . . 11 (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
104 mulcl 7929 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
10514, 103, 104sylancr 414 . . . . . . . . . 10 (𝑛 ∈ ℤ → (2 · 𝑛) ∈ ℂ)
106 subadd 8150 . . . . . . . . . . 11 (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
10727, 106mp3an3 1326 . . . . . . . . . 10 (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
108102, 105, 107syl2anr 290 . . . . . . . . 9 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
109 subcl 8146 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑘𝑛) ∈ ℂ)
110 2ap0 9001 . . . . . . . . . . . . . . . 16 2 # 0
11114, 110pm3.2i 272 . . . . . . . . . . . . . . 15 (2 ∈ ℂ ∧ 2 # 0)
112 eqcom 2179 . . . . . . . . . . . . . . . 16 ((𝑘𝑛) = (1 / 2) ↔ (1 / 2) = (𝑘𝑛))
113 divmulap 8621 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ (𝑘𝑛) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((1 / 2) = (𝑘𝑛) ↔ (2 · (𝑘𝑛)) = 1))
114112, 113bitrid 192 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ (𝑘𝑛) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((𝑘𝑛) = (1 / 2) ↔ (2 · (𝑘𝑛)) = 1))
11527, 111, 114mp3an13 1328 . . . . . . . . . . . . . 14 ((𝑘𝑛) ∈ ℂ → ((𝑘𝑛) = (1 / 2) ↔ (2 · (𝑘𝑛)) = 1))
116109, 115syl 14 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑘𝑛) = (1 / 2) ↔ (2 · (𝑘𝑛)) = 1))
117116ancoms 268 . . . . . . . . . . . 12 ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘𝑛) = (1 / 2) ↔ (2 · (𝑘𝑛)) = 1))
118 subdi 8332 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
11914, 118mp3an1 1324 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
120119ancoms 268 . . . . . . . . . . . . 13 ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · (𝑘𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
121120eqeq1d 2186 . . . . . . . . . . . 12 ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((2 · (𝑘𝑛)) = 1 ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
122117, 121bitrd 188 . . . . . . . . . . 11 ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
123103, 96, 122syl2an 289 . . . . . . . . . 10 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
124 zsubcl 9283 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘𝑛) ∈ ℤ)
125 eleq1 2240 . . . . . . . . . . . 12 ((𝑘𝑛) = (1 / 2) → ((𝑘𝑛) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
126124, 125syl5ibcom 155 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑘𝑛) = (1 / 2) → (1 / 2) ∈ ℤ))
127126ancoms 268 . . . . . . . . . 10 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘𝑛) = (1 / 2) → (1 / 2) ∈ ℤ))
128123, 127sylbird 170 . . . . . . . . 9 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 → (1 / 2) ∈ ℤ))
129108, 128sylbird 170 . . . . . . . 8 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (2 · 𝑘) → (1 / 2) ∈ ℤ))
130100, 129sylbid 150 . . . . . . 7 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (𝑘 · 2) → (1 / 2) ∈ ℤ))
13195, 130syl5 32 . . . . . 6 ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ))
132131rexlimivv 2600 . . . . 5 (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
13394, 132sylbir 135 . . . 4 ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
13493, 133mto 662 . . 3 ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
135 df-xor 1376 . . . . 5 ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ⊻ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ↔ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
136 xorbin 1384 . . . . 5 ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ⊻ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
137135, 136sylbir 135 . . . 4 (((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
138137bicomd 141 . . 3 (((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) → (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
13992, 134, 138sylancl 413 . 2 (𝑁 ∈ ℤ → (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
1404, 139bitrd 188 1 (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  w3a 978   = wceq 1353  wxo 1375  wcel 2148  wrex 2456   class class class wbr 4000  (class class class)co 5869  cc 7800  cr 7801  0cc0 7802  1c1 7803   + caddc 7805   · cmul 7807  cmin 8118  -cneg 8119   # cap 8528   / cdiv 8618  2c2 8959  0cn0 9165  cz 9242  cdvds 11778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920
This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-xor 1376  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-id 4290  df-po 4293  df-iso 4294  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-iota 5174  df-fun 5214  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-2 8967  df-n0 9166  df-z 9243  df-dvds 11779
This theorem is referenced by:  oddm1even  11863  oexpneg  11865  oddnn02np1  11868  2tp1odd  11872  sqoddm1div8z  11874  ltoddhalfle  11881  halfleoddlt  11882  opoe  11883  omoe  11884  opeo  11885  omeo  11886  m1expo  11888  m1exp1  11889  flodddiv4  11922
  Copyright terms: Public domain W3C validator