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 ∥ 𝐵 )