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−12∈ℤ→−A∈ℤ
3 znegcl ⊢A−12∈ℤ→−A−12∈ℤ
4 3 adantl ⊢A∈ℤ∧A−12∈ℤ→−A−12∈ℤ
5 peano2zm ⊢A∈ℤ→A−1∈ℤ
6 5 zcnd ⊢A∈ℤ→A−1∈ℂ
7 6 adantr ⊢A∈ℤ∧A−12∈ℤ→A−1∈ℂ
8 2cnd ⊢A∈ℤ∧A−12∈ℤ→2∈ℂ
9 2ne0 ⊢2≠0
10 9 a1i ⊢A∈ℤ∧A−12∈ℤ→2≠0
11 divneg ⊢A−1∈ℂ∧2∈ℂ∧2≠0→−A−12=−A−12
12 11 eleq1d ⊢A−1∈ℂ∧2∈ℂ∧2≠0→−A−12∈ℤ↔−A−12∈ℤ
13 7 8 10 12 syl3anc ⊢A∈ℤ∧A−12∈ℤ→−A−12∈ℤ↔−A−12∈ℤ
14 4 13 mpbid ⊢A∈ℤ∧A−12∈ℤ→−A−12∈ℤ
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+12=−A−12
21 20 eleq1d ⊢A∈ℤ→-A+12∈ℤ↔−A−12∈ℤ
22 21 adantr ⊢A∈ℤ∧A−12∈ℤ→-A+12∈ℤ↔−A−12∈ℤ
23 14 22 mpbird ⊢A∈ℤ∧A−12∈ℤ→-A+12∈ℤ
24 2 23 jca ⊢A∈ℤ∧A−12∈ℤ→−A∈ℤ∧-A+12∈ℤ
25 isodd2 ⊢A∈Odd↔A∈ℤ∧A−12∈ℤ
26 isodd ⊢−A∈Odd↔−A∈ℤ∧-A+12∈ℤ
27 24 25 26 3imtr4i ⊢A∈Odd→−A∈Odd