This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 = ( ( 2 · 𝐴 ) + 1 ) ) → ¬ 2 ∥ 𝐵 )

Proof

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