Metamath Proof Explorer

Theorem 2tp1odd

Description: A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021)

Ref Expression
Assertion 2tp1odd ⊢ A ∈ ℤ ∧ B = 2 ⁢ A + 1 → ¬ 2 ∥ B

Proof

Step Hyp Ref Expression
1 id ⊢ A ∈ ℤ → A ∈ ℤ
2 oveq2 ⊢ k = A → 2 ⁢ k = 2 ⁢ A
3 2 oveq1d ⊢ k = A → 2 ⁢ k + 1 = 2 ⁢ A + 1
4 3 eqeq1d ⊢ k = A → 2 ⁢ k + 1 = 2 ⁢ A + 1 ↔ 2 ⁢ A + 1 = 2 ⁢ A + 1
5 4 adantl ⊢ A ∈ ℤ ∧ k = A → 2 ⁢ k + 1 = 2 ⁢ A + 1 ↔ 2 ⁢ A + 1 = 2 ⁢ A + 1
6 eqidd ⊢ A ∈ ℤ → 2 ⁢ A + 1 = 2 ⁢ A + 1
7 1 5 6 rspcedvd ⊢ A ∈ ℤ → ∃ k ∈ ℤ 2 ⁢ k + 1 = 2 ⁢ A + 1
8 2z ⊢ 2 ∈ ℤ
9 8 a1i ⊢ A ∈ ℤ → 2 ∈ ℤ
10 9 1 zmulcld ⊢ A ∈ ℤ → 2 ⁢ A ∈ ℤ
11 10 peano2zd ⊢ A ∈ ℤ → 2 ⁢ A + 1 ∈ ℤ
12 odd2np1 ⊢ 2 ⁢ A + 1 ∈ ℤ → ¬ 2 ∥ 2 ⁢ A + 1 ↔ ∃ k ∈ ℤ 2 ⁢ k + 1 = 2 ⁢ A + 1
13 11 12 syl ⊢ A ∈ ℤ → ¬ 2 ∥ 2 ⁢ A + 1 ↔ ∃ k ∈ ℤ 2 ⁢ k + 1 = 2 ⁢ A + 1
14 7 13 mpbird ⊢ A ∈ ℤ → ¬ 2 ∥ 2 ⁢ A + 1
15 14 adantr ⊢ A ∈ ℤ ∧ B = 2 ⁢ A + 1 → ¬ 2 ∥ 2 ⁢ A + 1
16 breq2 ⊢ B = 2 ⁢ A + 1 → 2 ∥ B ↔ 2 ∥ 2 ⁢ A + 1
17 16 adantl ⊢ A ∈ ℤ ∧ B = 2 ⁢ A + 1 → 2 ∥ B ↔ 2 ∥ 2 ⁢ A + 1
18 15 17 mtbird ⊢ A ∈ ℤ ∧ B = 2 ⁢ A + 1 → ¬ 2 ∥ B