Theorem gcd2odd1

Description: The greatest common divisor of an odd number and 2 is 1, i.e., 2 and any odd number are coprime. Remark: The proof using dfodd7 is longer (see proof in comment)! (Contributed by AV, 5-Jun-2023)

	Ref	Expression
Assertion	gcd2odd1	|- ( Z e. Odd -> ( Z gcd 2 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		oddz	|- ( Z e. Odd -> Z e. ZZ )
2		2z	|- 2 e. ZZ
3		gcdcom	|- ( ( Z e. ZZ /\ 2 e. ZZ ) -> ( Z gcd 2 ) = ( 2 gcd Z ) )
4	1 2 3	sylancl	|- ( Z e. Odd -> ( Z gcd 2 ) = ( 2 gcd Z ) )
5		2ndvdsodd	|- ( Z e. Odd -> -. 2 || Z )
6		2prm	|- 2 e. Prime
7		coprm	|- ( ( 2 e. Prime /\ Z e. ZZ ) -> ( -. 2 || Z <-> ( 2 gcd Z ) = 1 ) )
8	6 1 7	sylancr	|- ( Z e. Odd -> ( -. 2 || Z <-> ( 2 gcd Z ) = 1 ) )
9	5 8	mpbid	|- ( Z e. Odd -> ( 2 gcd Z ) = 1 )
10	4 9	eqtrd	|- ( Z e. Odd -> ( Z gcd 2 ) = 1 )