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 e. Odd -> -u A e. Odd )

Proof

Step Hyp Ref Expression
1 znegcl 
 |-  ( A e. ZZ -> -u A e. ZZ )
2 1 adantr 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> -u A e. ZZ )
3 znegcl 
 |-  ( ( ( A - 1 ) / 2 ) e. ZZ -> -u ( ( A - 1 ) / 2 ) e. ZZ )
4 3 adantl 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> -u ( ( A - 1 ) / 2 ) e. ZZ )
5 peano2zm 
 |-  ( A e. ZZ -> ( A - 1 ) e. ZZ )
6 5 zcnd 
 |-  ( A e. ZZ -> ( A - 1 ) e. CC )
7 6 adantr 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> ( A - 1 ) e. CC )
8 2cnd 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> 2 e. CC )
9 2ne0 
 |-  2 =/= 0
10 9 a1i 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> 2 =/= 0 )
11 divneg 
 |-  ( ( ( A - 1 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( ( A - 1 ) / 2 ) = ( -u ( A - 1 ) / 2 ) )
12 11 eleq1d 
 |-  ( ( ( A - 1 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( -u ( ( A - 1 ) / 2 ) e. ZZ <-> ( -u ( A - 1 ) / 2 ) e. ZZ ) )
13 7 8 10 12 syl3anc 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> ( -u ( ( A - 1 ) / 2 ) e. ZZ <-> ( -u ( A - 1 ) / 2 ) e. ZZ ) )
14 4 13 mpbid 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> ( -u ( A - 1 ) / 2 ) e. ZZ )
15 zcn 
 |-  ( A e. ZZ -> A e. CC )
16 1cnd 
 |-  ( A e. ZZ -> 1 e. CC )
17 negsubdi 
 |-  ( ( A e. CC /\ 1 e. CC ) -> -u ( A - 1 ) = ( -u A + 1 ) )
18 17 eqcomd 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( -u A + 1 ) = -u ( A - 1 ) )
19 15 16 18 syl2anc 
 |-  ( A e. ZZ -> ( -u A + 1 ) = -u ( A - 1 ) )
20 19 oveq1d 
 |-  ( A e. ZZ -> ( ( -u A + 1 ) / 2 ) = ( -u ( A - 1 ) / 2 ) )
21 20 eleq1d 
 |-  ( A e. ZZ -> ( ( ( -u A + 1 ) / 2 ) e. ZZ <-> ( -u ( A - 1 ) / 2 ) e. ZZ ) )
22 21 adantr 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> ( ( ( -u A + 1 ) / 2 ) e. ZZ <-> ( -u ( A - 1 ) / 2 ) e. ZZ ) )
23 14 22 mpbird 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> ( ( -u A + 1 ) / 2 ) e. ZZ )
24 2 23 jca 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) -> ( -u A e. ZZ /\ ( ( -u A + 1 ) / 2 ) e. ZZ ) )
25 isodd2 
 |-  ( A e. Odd <-> ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. ZZ ) )
26 isodd 
 |-  ( -u A e. Odd <-> ( -u A e. ZZ /\ ( ( -u A + 1 ) / 2 ) e. ZZ ) )
27 24 25 26 3imtr4i 
 |-  ( A e. Odd -> -u A e. Odd )