Description: Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | dfeven4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-even | |
|
2 | simpr | |
|
3 | oveq2 | |
|
4 | 3 | eqeq2d | |
5 | 4 | adantl | |
6 | zcn | |
|
7 | 6 | adantr | |
8 | 2cnd | |
|
9 | 2ne0 | |
|
10 | 9 | a1i | |
11 | 7 8 10 | divcan2d | |
12 | 11 | eqcomd | |
13 | 2 5 12 | rspcedvd | |
14 | 13 | ex | |
15 | oveq1 | |
|
16 | zcn | |
|
17 | 16 | adantl | |
18 | 2cnd | |
|
19 | 9 | a1i | |
20 | 17 18 19 | divcan3d | |
21 | 15 20 | sylan9eqr | |
22 | simpr | |
|
23 | 22 | adantr | |
24 | 21 23 | eqeltrd | |
25 | 24 | rexlimdva2 | |
26 | 14 25 | impbid | |
27 | 26 | rabbiia | |
28 | 1 27 | eqtri | |