Theorem isodd7

Description: The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020)

	Ref	Expression
Assertion	isodd7	|- ( Z e. Odd <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		isodd3	|- ( Z e. Odd <-> ( Z e. ZZ /\ -. 2 || Z ) )
2		2prm	|- 2 e. Prime
3		coprm	|- ( ( 2 e. Prime /\ Z e. ZZ ) -> ( -. 2 || Z <-> ( 2 gcd Z ) = 1 ) )
4	2 3	mpan	|- ( Z e. ZZ -> ( -. 2 || Z <-> ( 2 gcd Z ) = 1 ) )
5	4	pm5.32i	|- ( ( Z e. ZZ /\ -. 2 || Z ) <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 1 ) )
6	1 5	bitri	|- ( Z e. Odd <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 1 ) )