Description: A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | evennn2n | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 | |
|
2 | simpr | |
|
3 | 2re | |
|
4 | 3 | a1i | |
5 | zre | |
|
6 | 5 | adantl | |
7 | 0le2 | |
|
8 | 7 | a1i | |
9 | nngt0 | |
|
10 | 9 | adantr | |
11 | prodgt0 | |
|
12 | 4 6 8 10 11 | syl22anc | |
13 | elnnz | |
|
14 | 2 12 13 | sylanbrc | |
15 | 14 | ex | |
16 | 1 15 | syl6bir | |
17 | 16 | com13 | |
18 | 17 | impcom | |
19 | 18 | pm4.71rd | |
20 | 19 | bicomd | |
21 | 20 | rexbidva | |
22 | nnssz | |
|
23 | rexss | |
|
24 | 22 23 | mp1i | |
25 | even2n | |
|
26 | 25 | a1i | |
27 | 21 24 26 | 3bitr4rd | |