Description: A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021) (Proof shortened by AV, 10-Jul-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | evennn02n | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 | |
|
2 | simpr | |
|
3 | 2rp | |
|
4 | 3 | a1i | |
5 | zre | |
|
6 | 5 | adantl | |
7 | nn0ge0 | |
|
8 | 7 | adantr | |
9 | 4 6 8 | prodge0rd | |
10 | elnn0z | |
|
11 | 2 9 10 | sylanbrc | |
12 | 11 | ex | |
13 | 1 12 | syl6bir | |
14 | 13 | com13 | |
15 | 14 | impcom | |
16 | 15 | pm4.71rd | |
17 | 16 | bicomd | |
18 | 17 | rexbidva | |
19 | nn0ssz | |
|
20 | rexss | |
|
21 | 19 20 | mp1i | |
22 | even2n | |
|
23 | 22 | a1i | |
24 | 18 21 23 | 3bitr4rd | |