Proof of Theorem oddfl
| Step | Hyp | Ref
| Expression |
| 1 | | zre 12617 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
| 2 | | 1red 11262 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → 1 ∈
ℝ) |
| 3 | 1, 2 | resubcld 11691 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℝ) |
| 4 | | 2rp 13039 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
| 5 | 4 | a1i 11 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → 2 ∈
ℝ+) |
| 6 | 1 | lem1d 12201 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ≤ 𝐾) |
| 7 | 3, 1, 5, 6 | lediv1dd 13135 |
. . . . . . 7
⊢ (𝐾 ∈ ℤ → ((𝐾 − 1) / 2) ≤ (𝐾 / 2)) |
| 8 | 1 | rehalfcld 12513 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (𝐾 / 2) ∈
ℝ) |
| 9 | 5 | rpreccld 13087 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (1 / 2)
∈ ℝ+) |
| 10 | 8, 9 | ltaddrpd 13110 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → (𝐾 / 2) < ((𝐾 / 2) + (1 / 2))) |
| 11 | | zcn 12618 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
| 12 | 2 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → 1 ∈
ℂ) |
| 13 | | 2cnd 12344 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → 2 ∈
ℂ) |
| 14 | 5 | rpne0d 13082 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → 2 ≠
0) |
| 15 | 11, 12, 13, 14 | divsubdird 12082 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → ((𝐾 − 1) / 2) = ((𝐾 / 2) − (1 /
2))) |
| 16 | 15 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (((𝐾 − 1) / 2) + 1) = (((𝐾 / 2) − (1 / 2)) +
1)) |
| 17 | 11 | halfcld 12511 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (𝐾 / 2) ∈
ℂ) |
| 18 | 13, 14 | reccld 12036 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (1 / 2)
∈ ℂ) |
| 19 | 17, 18, 12 | subadd23d 11642 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (((𝐾 / 2) − (1 / 2)) + 1) =
((𝐾 / 2) + (1 − (1 /
2)))) |
| 20 | | 1mhlfehlf 12485 |
. . . . . . . . . . 11
⊢ (1
− (1 / 2)) = (1 / 2) |
| 21 | 20 | oveq2i 7442 |
. . . . . . . . . 10
⊢ ((𝐾 / 2) + (1 − (1 / 2))) =
((𝐾 / 2) + (1 /
2)) |
| 22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → ((𝐾 / 2) + (1 − (1 / 2))) =
((𝐾 / 2) + (1 /
2))) |
| 23 | 16, 19, 22 | 3eqtrrd 2782 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → ((𝐾 / 2) + (1 / 2)) = (((𝐾 − 1) / 2) +
1)) |
| 24 | 10, 23 | breqtrd 5169 |
. . . . . . 7
⊢ (𝐾 ∈ ℤ → (𝐾 / 2) < (((𝐾 − 1) / 2) + 1)) |
| 25 | 7, 24 | jca 511 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → (((𝐾 − 1) / 2) ≤ (𝐾 / 2) ∧ (𝐾 / 2) < (((𝐾 − 1) / 2) + 1))) |
| 26 | 25 | adantr 480 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (((𝐾 − 1) / 2) ≤ (𝐾 / 2) ∧ (𝐾 / 2) < (((𝐾 − 1) / 2) + 1))) |
| 27 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 ∈
ℝ) |
| 28 | 27 | rehalfcld 12513 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (𝐾 / 2) ∈
ℝ) |
| 29 | 11, 12 | npcand 11624 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → ((𝐾 − 1) + 1) = 𝐾) |
| 30 | 29 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (((𝐾 − 1) + 1) / 2) = (𝐾 / 2)) |
| 31 | 30 | adantr 480 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (((𝐾 − 1) + 1) / 2) = (𝐾 / 2)) |
| 32 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (𝐾 mod 2) ≠ 0) |
| 33 | 32 | neneqd 2945 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ¬
(𝐾 mod 2) =
0) |
| 34 | | mod0 13916 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℝ ∧ 2 ∈
ℝ+) → ((𝐾 mod 2) = 0 ↔ (𝐾 / 2) ∈ ℤ)) |
| 35 | 1, 5, 34 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → ((𝐾 mod 2) = 0 ↔ (𝐾 / 2) ∈
ℤ)) |
| 36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((𝐾 mod 2) = 0 ↔ (𝐾 / 2) ∈
ℤ)) |
| 37 | 33, 36 | mtbid 324 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ¬
(𝐾 / 2) ∈
ℤ) |
| 38 | 31, 37 | eqneltrd 2861 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ¬
(((𝐾 − 1) + 1) / 2)
∈ ℤ) |
| 39 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 ∈
ℤ) |
| 40 | | 1zzd 12648 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 1 ∈
ℤ) |
| 41 | 39, 40 | zsubcld 12727 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (𝐾 − 1) ∈
ℤ) |
| 42 | | zeo2 12705 |
. . . . . . . 8
⊢ ((𝐾 − 1) ∈ ℤ
→ (((𝐾 − 1) / 2)
∈ ℤ ↔ ¬ (((𝐾 − 1) + 1) / 2) ∈
ℤ)) |
| 43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (((𝐾 − 1) / 2) ∈ ℤ
↔ ¬ (((𝐾 −
1) + 1) / 2) ∈ ℤ)) |
| 44 | 38, 43 | mpbird 257 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((𝐾 − 1) / 2) ∈
ℤ) |
| 45 | | flbi 13856 |
. . . . . 6
⊢ (((𝐾 / 2) ∈ ℝ ∧
((𝐾 − 1) / 2) ∈
ℤ) → ((⌊‘(𝐾 / 2)) = ((𝐾 − 1) / 2) ↔ (((𝐾 − 1) / 2) ≤ (𝐾 / 2) ∧ (𝐾 / 2) < (((𝐾 − 1) / 2) + 1)))) |
| 46 | 28, 44, 45 | syl2anc 584 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) →
((⌊‘(𝐾 / 2)) =
((𝐾 − 1) / 2) ↔
(((𝐾 − 1) / 2) ≤
(𝐾 / 2) ∧ (𝐾 / 2) < (((𝐾 − 1) / 2) + 1)))) |
| 47 | 26, 46 | mpbird 257 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) →
(⌊‘(𝐾 / 2)) =
((𝐾 − 1) /
2)) |
| 48 | 47 | oveq2d 7447 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → (2
· (⌊‘(𝐾
/ 2))) = (2 · ((𝐾
− 1) / 2))) |
| 49 | 48 | oveq1d 7446 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((2
· (⌊‘(𝐾
/ 2))) + 1) = ((2 · ((𝐾 − 1) / 2)) + 1)) |
| 50 | 11, 12 | subcld 11620 |
. . . . 5
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℂ) |
| 51 | 50, 13, 14 | divcan2d 12045 |
. . . 4
⊢ (𝐾 ∈ ℤ → (2
· ((𝐾 − 1) /
2)) = (𝐾 −
1)) |
| 52 | 51 | oveq1d 7446 |
. . 3
⊢ (𝐾 ∈ ℤ → ((2
· ((𝐾 − 1) /
2)) + 1) = ((𝐾 − 1) +
1)) |
| 53 | 52 | adantr 480 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((2
· ((𝐾 − 1) /
2)) + 1) = ((𝐾 − 1) +
1)) |
| 54 | 29 | adantr 480 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → ((𝐾 − 1) + 1) = 𝐾) |
| 55 | 49, 53, 54 | 3eqtrrd 2782 |
1
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 ·
(⌊‘(𝐾 / 2))) +
1)) |