Proof of Theorem dfodd6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfodd2 47623 | . 2
⊢  Odd =
{𝑧 ∈ ℤ ∣
((𝑧 − 1) / 2) ∈
ℤ} | 
| 2 |  | simpr 484 | . . . . . 6
⊢ ((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
→ ((𝑧 − 1) / 2)
∈ ℤ) | 
| 3 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑖 = ((𝑧 − 1) / 2) → (2 · 𝑖) = (2 · ((𝑧 − 1) /
2))) | 
| 4 |  | peano2zm 12660 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℤ → (𝑧 − 1) ∈
ℤ) | 
| 5 | 4 | zcnd 12723 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℤ → (𝑧 − 1) ∈
ℂ) | 
| 6 |  | 2cnd 12344 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℤ → 2 ∈
ℂ) | 
| 7 |  | 2ne0 12370 | . . . . . . . . . . . . . 14
⊢ 2 ≠
0 | 
| 8 | 7 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℤ → 2 ≠
0) | 
| 9 | 5, 6, 8 | 3jca 1129 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ℤ → ((𝑧 − 1) ∈ ℂ ∧
2 ∈ ℂ ∧ 2 ≠ 0)) | 
| 10 | 9 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
→ ((𝑧 − 1)
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0)) | 
| 11 |  | divcan2 11930 | . . . . . . . . . . 11
⊢ (((𝑧 − 1) ∈ ℂ ∧
2 ∈ ℂ ∧ 2 ≠ 0) → (2 · ((𝑧 − 1) / 2)) = (𝑧 − 1)) | 
| 12 | 10, 11 | syl 17 | . . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
→ (2 · ((𝑧
− 1) / 2)) = (𝑧
− 1)) | 
| 13 | 3, 12 | sylan9eqr 2799 | . . . . . . . . 9
⊢ (((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
∧ 𝑖 = ((𝑧 − 1) / 2)) → (2
· 𝑖) = (𝑧 − 1)) | 
| 14 | 13 | oveq1d 7446 | . . . . . . . 8
⊢ (((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
∧ 𝑖 = ((𝑧 − 1) / 2)) → ((2
· 𝑖) + 1) = ((𝑧 − 1) +
1)) | 
| 15 |  | zcn 12618 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℂ) | 
| 16 |  | npcan1 11688 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ → ((𝑧 − 1) + 1) = 𝑧) | 
| 17 | 15, 16 | syl 17 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℤ → ((𝑧 − 1) + 1) = 𝑧) | 
| 18 | 17 | adantr 480 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
→ ((𝑧 − 1) + 1)
= 𝑧) | 
| 19 | 18 | adantr 480 | . . . . . . . 8
⊢ (((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
∧ 𝑖 = ((𝑧 − 1) / 2)) → ((𝑧 − 1) + 1) = 𝑧) | 
| 20 | 14, 19 | eqtrd 2777 | . . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
∧ 𝑖 = ((𝑧 − 1) / 2)) → ((2
· 𝑖) + 1) = 𝑧) | 
| 21 | 20 | eqeq2d 2748 | . . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
∧ 𝑖 = ((𝑧 − 1) / 2)) → (𝑧 = ((2 · 𝑖) + 1) ↔ 𝑧 = 𝑧)) | 
| 22 |  | eqidd 2738 | . . . . . 6
⊢ ((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
→ 𝑧 = 𝑧) | 
| 23 | 2, 21, 22 | rspcedvd 3624 | . . . . 5
⊢ ((𝑧 ∈ ℤ ∧ ((𝑧 − 1) / 2) ∈ ℤ)
→ ∃𝑖 ∈
ℤ 𝑧 = ((2 ·
𝑖) + 1)) | 
| 24 | 23 | ex 412 | . . . 4
⊢ (𝑧 ∈ ℤ → (((𝑧 − 1) / 2) ∈ ℤ
→ ∃𝑖 ∈
ℤ 𝑧 = ((2 ·
𝑖) + 1))) | 
| 25 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑧 = ((2 · 𝑖) + 1) → (𝑧 − 1) = (((2 ·
𝑖) + 1) −
1)) | 
| 26 |  | zcn 12618 | . . . . . . . . . . 11
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) | 
| 27 |  | mulcl 11239 | . . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑖
∈ ℂ) → (2 · 𝑖) ∈ ℂ) | 
| 28 | 6, 26, 27 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (2
· 𝑖) ∈
ℂ) | 
| 29 |  | pncan1 11687 | . . . . . . . . . 10
⊢ ((2
· 𝑖) ∈ ℂ
→ (((2 · 𝑖) +
1) − 1) = (2 · 𝑖)) | 
| 30 | 28, 29 | syl 17 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (((2
· 𝑖) + 1) − 1)
= (2 · 𝑖)) | 
| 31 | 25, 30 | sylan9eqr 2799 | . . . . . . . 8
⊢ (((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝑧 = ((2 · 𝑖) + 1)) → (𝑧 − 1) = (2 · 𝑖)) | 
| 32 | 31 | oveq1d 7446 | . . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝑧 = ((2 · 𝑖) + 1)) → ((𝑧 − 1) / 2) = ((2 ·
𝑖) / 2)) | 
| 33 | 26 | adantl 481 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 ∈
ℂ) | 
| 34 |  | 2cnd 12344 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 2 ∈
ℂ) | 
| 35 | 7 | a1i 11 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 2 ≠
0) | 
| 36 | 33, 34, 35 | divcan3d 12048 | . . . . . . . 8
⊢ ((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((2
· 𝑖) / 2) = 𝑖) | 
| 37 | 36 | adantr 480 | . . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝑧 = ((2 · 𝑖) + 1)) → ((2 ·
𝑖) / 2) = 𝑖) | 
| 38 | 32, 37 | eqtrd 2777 | . . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝑧 = ((2 · 𝑖) + 1)) → ((𝑧 − 1) / 2) = 𝑖) | 
| 39 |  | simpr 484 | . . . . . . 7
⊢ ((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 ∈
ℤ) | 
| 40 | 39 | adantr 480 | . . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝑧 = ((2 · 𝑖) + 1)) → 𝑖 ∈
ℤ) | 
| 41 | 38, 40 | eqeltrd 2841 | . . . . 5
⊢ (((𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ 𝑧 = ((2 · 𝑖) + 1)) → ((𝑧 − 1) / 2) ∈
ℤ) | 
| 42 | 41 | rexlimdva2 3157 | . . . 4
⊢ (𝑧 ∈ ℤ →
(∃𝑖 ∈ ℤ
𝑧 = ((2 · 𝑖) + 1) → ((𝑧 − 1) / 2) ∈
ℤ)) | 
| 43 | 24, 42 | impbid 212 | . . 3
⊢ (𝑧 ∈ ℤ → (((𝑧 − 1) / 2) ∈ ℤ
↔ ∃𝑖 ∈
ℤ 𝑧 = ((2 ·
𝑖) + 1))) | 
| 44 | 43 | rabbiia 3440 | . 2
⊢ {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ}
= {𝑧 ∈ ℤ ∣
∃𝑖 ∈ ℤ
𝑧 = ((2 · 𝑖) + 1)} | 
| 45 | 1, 44 | eqtri 2765 | 1
⊢  Odd =
{𝑧 ∈ ℤ ∣
∃𝑖 ∈ ℤ
𝑧 = ((2 · 𝑖) + 1)} |