Metamath Proof Explorer

Theorem oddflALTV

Description: Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 18-Jun-2020)

Ref Expression
Assertion oddflALTV ⊢ K ∈ Odd → K = 2 ⁢ K 2 + 1

Proof

Step Hyp Ref Expression
1 zofldiv2ALTV ⊢ K ∈ Odd → K 2 = K − 1 2
2 1 oveq2d ⊢ K ∈ Odd → 2 ⁢ K 2 = 2 ⁢ K − 1 2
3 2 oveq1d ⊢ K ∈ Odd → 2 ⁢ K 2 + 1 = 2 ⁢ K − 1 2 + 1
4 oddz ⊢ K ∈ Odd → K ∈ ℤ
5 peano2zm ⊢ K ∈ ℤ → K − 1 ∈ ℤ
6 5 zcnd ⊢ K ∈ ℤ → K − 1 ∈ ℂ
7 4 6 syl ⊢ K ∈ Odd → K − 1 ∈ ℂ
8 2cnd ⊢ K ∈ Odd → 2 ∈ ℂ
9 2ne0 ⊢ 2 ≠ 0
10 9 a1i ⊢ K ∈ Odd → 2 ≠ 0
11 7 8 10 divcan2d ⊢ K ∈ Odd → 2 ⁢ K − 1 2 = K − 1
12 11 oveq1d ⊢ K ∈ Odd → 2 ⁢ K − 1 2 + 1 = K - 1 + 1
13 4 zcnd ⊢ K ∈ Odd → K ∈ ℂ
14 npcan1 ⊢ K ∈ ℂ → K - 1 + 1 = K
15 13 14 syl ⊢ K ∈ Odd → K - 1 + 1 = K
16 3 12 15 3eqtrrd ⊢ K ∈ Odd → K = 2 ⁢ K 2 + 1