Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Even and odd numbers
Definitions and basic properties
enege
Next ⟩
onego
Metamath Proof Explorer
Ascii
Unicode
Theorem
enege
Description:
The negative of an even number is even.
(Contributed by
AV
, 20-Jun-2020)
Ref
Expression
Assertion
enege
⊢
A
∈
Even
→
−
A
∈
Even
Proof
Step
Hyp
Ref
Expression
1
znegcl
⊢
A
∈
ℤ
→
−
A
∈
ℤ
2
1
adantr
⊢
A
∈
ℤ
∧
A
2
∈
ℤ
→
−
A
∈
ℤ
3
znegcl
⊢
A
2
∈
ℤ
→
−
A
2
∈
ℤ
4
3
adantl
⊢
A
∈
ℤ
∧
A
2
∈
ℤ
→
−
A
2
∈
ℤ
5
zcn
⊢
A
∈
ℤ
→
A
∈
ℂ
6
2cnd
⊢
A
∈
ℤ
→
2
∈
ℂ
7
2ne0
⊢
2
≠
0
8
7
a1i
⊢
A
∈
ℤ
→
2
≠
0
9
5
6
8
3jca
⊢
A
∈
ℤ
→
A
∈
ℂ
∧
2
∈
ℂ
∧
2
≠
0
10
9
adantr
⊢
A
∈
ℤ
∧
A
2
∈
ℤ
→
A
∈
ℂ
∧
2
∈
ℂ
∧
2
≠
0
11
divneg
⊢
A
∈
ℂ
∧
2
∈
ℂ
∧
2
≠
0
→
−
A
2
=
−
A
2
12
11
eleq1d
⊢
A
∈
ℂ
∧
2
∈
ℂ
∧
2
≠
0
→
−
A
2
∈
ℤ
↔
−
A
2
∈
ℤ
13
10
12
syl
⊢
A
∈
ℤ
∧
A
2
∈
ℤ
→
−
A
2
∈
ℤ
↔
−
A
2
∈
ℤ
14
4
13
mpbid
⊢
A
∈
ℤ
∧
A
2
∈
ℤ
→
−
A
2
∈
ℤ
15
2
14
jca
⊢
A
∈
ℤ
∧
A
2
∈
ℤ
→
−
A
∈
ℤ
∧
−
A
2
∈
ℤ
16
iseven
⊢
A
∈
Even
↔
A
∈
ℤ
∧
A
2
∈
ℤ
17
iseven
⊢
−
A
∈
Even
↔
−
A
∈
ℤ
∧
−
A
2
∈
ℤ
18
15
16
17
3imtr4i
⊢
A
∈
Even
→
−
A
∈
Even