Metamath Proof Explorer

Theorem onego

Description: The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020)

Ref Expression
Assertion onego ⊢ A ∈ Odd → − A ∈ Odd

Proof

Step Hyp Ref Expression
1 znegcl ⊢ A ∈ ℤ → − A ∈ ℤ
2 1 adantr ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → − A ∈ ℤ
3 znegcl ⊢ A − 1 2 ∈ ℤ → − A − 1 2 ∈ ℤ
4 3 adantl ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → − A − 1 2 ∈ ℤ
5 peano2zm ⊢ A ∈ ℤ → A − 1 ∈ ℤ
6 5 zcnd ⊢ A ∈ ℤ → A − 1 ∈ ℂ
7 6 adantr ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → A − 1 ∈ ℂ
8 2cnd ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → 2 ∈ ℂ
9 2ne0 ⊢ 2 ≠ 0
10 9 a1i ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → 2 ≠ 0
11 divneg ⊢ A − 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → − A − 1 2 = − A − 1 2
12 11 eleq1d ⊢ A − 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → − A − 1 2 ∈ ℤ ↔ − A − 1 2 ∈ ℤ
13 7 8 10 12 syl3anc ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → − A − 1 2 ∈ ℤ ↔ − A − 1 2 ∈ ℤ
14 4 13 mpbid ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → − A − 1 2 ∈ ℤ
15 zcn ⊢ A ∈ ℤ → A ∈ ℂ
16 1cnd ⊢ A ∈ ℤ → 1 ∈ ℂ
17 negsubdi ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → − A − 1 = - A + 1
18 17 eqcomd ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → - A + 1 = − A − 1
19 15 16 18 syl2anc ⊢ A ∈ ℤ → - A + 1 = − A − 1
20 19 oveq1d ⊢ A ∈ ℤ → - A + 1 2 = − A − 1 2
21 20 eleq1d ⊢ A ∈ ℤ → - A + 1 2 ∈ ℤ ↔ − A − 1 2 ∈ ℤ
22 21 adantr ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → - A + 1 2 ∈ ℤ ↔ − A − 1 2 ∈ ℤ
23 14 22 mpbird ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → - A + 1 2 ∈ ℤ
24 2 23 jca ⊢ A ∈ ℤ ∧ A − 1 2 ∈ ℤ → − A ∈ ℤ ∧ - A + 1 2 ∈ ℤ
25 isodd2 ⊢ A ∈ Odd ↔ A ∈ ℤ ∧ A − 1 2 ∈ ℤ
26 isodd ⊢ − A ∈ Odd ↔ − A ∈ ℤ ∧ - A + 1 2 ∈ ℤ
27 24 25 26 3imtr4i ⊢ A ∈ Odd → − A ∈ Odd