Description: A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | 2tp1odd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |
|
2 | oveq2 | |
|
3 | 2 | oveq1d | |
4 | 3 | eqeq1d | |
5 | 4 | adantl | |
6 | eqidd | |
|
7 | 1 5 6 | rspcedvd | |
8 | 2z | |
|
9 | 8 | a1i | |
10 | 9 1 | zmulcld | |
11 | 10 | peano2zd | |
12 | odd2np1 | |
|
13 | 11 12 | syl | |
14 | 7 13 | mpbird | |
15 | 14 | adantr | |
16 | breq2 | |
|
17 | 16 | adantl | |
18 | 15 17 | mtbird | |