onego

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

		Ref	Expression
	Assertion	onego	⊢ ( 𝐴 ∈ Odd → - 𝐴 ∈ Odd )

Proof

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

Metamath Proof Explorer

Theorem onego

Proof