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 AB=2A+1¬2B

Proof

Step Hyp Ref Expression
1 id AA
2 oveq2 k=A2k=2A
3 2 oveq1d k=A2k+1=2A+1
4 3 eqeq1d k=A2k+1=2A+12A+1=2A+1
5 4 adantl Ak=A2k+1=2A+12A+1=2A+1
6 eqidd A2A+1=2A+1
7 1 5 6 rspcedvd Ak2k+1=2A+1
8 2z 2
9 8 a1i A2
10 9 1 zmulcld A2A
11 10 peano2zd A2A+1
12 odd2np1 2A+1¬22A+1k2k+1=2A+1
13 11 12 syl A¬22A+1k2k+1=2A+1
14 7 13 mpbird A¬22A+1
15 14 adantr AB=2A+1¬22A+1
16 breq2 B=2A+12B22A+1
17 16 adantl AB=2A+12B22A+1
18 15 17 mtbird AB=2A+1¬2B