divgcdoddALTV

Description: Either A / ( A gcd B ) is odd or B / ( A gcd B ) is odd. (Contributed by Scott Fenton, 19-Apr-2014) (Revised by AV, 21-Jun-2020)

		Ref	Expression
	Assertion	divgcdoddALTV	$⊢ (A \in ℕ \land B \in ℕ) \to (\frac{A}{A \gcd B} \in Odd \lor \frac{B}{A \gcd B} \in Odd)$

Proof

Step	Hyp	Ref	Expression
1		divgcdodd	$⊢ (A \in ℕ \land B \in ℕ) \to (\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B}))$
2		nnz	$⊢ A \in ℕ \to A \in ℤ$
3		nnz	$⊢ B \in ℕ \to B \in ℤ$
4		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
5	2 3 4	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
6	5	simpld	$⊢ (A \in ℕ \land B \in ℕ) \to (A \gcd B) ∥ A$
7	2 3	anim12i	$⊢ (A \in ℕ \land B \in ℕ) \to (A \in ℤ \land B \in ℤ)$
8		nnne0	$⊢ A \in ℕ \to A \neq 0$
9	8	neneqd	$⊢ A \in ℕ \to \neg A = 0$
10	9	intnanrd	$⊢ A \in ℕ \to \neg (A = 0 \land B = 0)$
11	10	adantr	$⊢ (A \in ℕ \land B \in ℕ) \to \neg (A = 0 \land B = 0)$
12		gcdn0cl	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in ℕ$
13	7 11 12	syl2anc	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℕ$
14	13	nnzd	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℤ$
15	13	nnne0d	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \neq 0$
16	2	adantr	$⊢ (A \in ℕ \land B \in ℕ) \to A \in ℤ$
17		dvdsval2	$⊢ (A \gcd B \in ℤ \land A \gcd B \neq 0 \land A \in ℤ) \to ((A \gcd B) ∥ A \leftrightarrow \frac{A}{A \gcd B} \in ℤ)$
18	14 15 16 17	syl3anc	$⊢ (A \in ℕ \land B \in ℕ) \to ((A \gcd B) ∥ A \leftrightarrow \frac{A}{A \gcd B} \in ℤ)$
19	6 18	mpbid	$⊢ (A \in ℕ \land B \in ℕ) \to \frac{A}{A \gcd B} \in ℤ$
20	19	biantrurd	$⊢ (A \in ℕ \land B \in ℕ) \to (\neg 2 ∥ (\frac{A}{A \gcd B}) \leftrightarrow (\frac{A}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{A}{A \gcd B})))$
21	5	simprd	$⊢ (A \in ℕ \land B \in ℕ) \to (A \gcd B) ∥ B$
22	3	adantl	$⊢ (A \in ℕ \land B \in ℕ) \to B \in ℤ$
23		dvdsval2	$⊢ (A \gcd B \in ℤ \land A \gcd B \neq 0 \land B \in ℤ) \to ((A \gcd B) ∥ B \leftrightarrow \frac{B}{A \gcd B} \in ℤ)$
24	14 15 22 23	syl3anc	$⊢ (A \in ℕ \land B \in ℕ) \to ((A \gcd B) ∥ B \leftrightarrow \frac{B}{A \gcd B} \in ℤ)$
25	21 24	mpbid	$⊢ (A \in ℕ \land B \in ℕ) \to \frac{B}{A \gcd B} \in ℤ$
26	25	biantrurd	$⊢ (A \in ℕ \land B \in ℕ) \to (\neg 2 ∥ (\frac{B}{A \gcd B}) \leftrightarrow (\frac{B}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{B}{A \gcd B})))$
27	20 26	orbi12d	$⊢ (A \in ℕ \land B \in ℕ) \to ((\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B})) \leftrightarrow ((\frac{A}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{A}{A \gcd B})) \lor (\frac{B}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{B}{A \gcd B}))))$
28	1 27	mpbid	$⊢ (A \in ℕ \land B \in ℕ) \to ((\frac{A}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{A}{A \gcd B})) \lor (\frac{B}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{B}{A \gcd B})))$
29		isodd3	$⊢ \frac{A}{A \gcd B} \in Odd \leftrightarrow (\frac{A}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{A}{A \gcd B}))$
30		isodd3	$⊢ \frac{B}{A \gcd B} \in Odd \leftrightarrow (\frac{B}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{B}{A \gcd B}))$
31	29 30	orbi12i	$⊢ (\frac{A}{A \gcd B} \in Odd \lor \frac{B}{A \gcd B} \in Odd) \leftrightarrow ((\frac{A}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{A}{A \gcd B})) \lor (\frac{B}{A \gcd B} \in ℤ \land \neg 2 ∥ (\frac{B}{A \gcd B})))$
32	28 31	sylibr	$⊢ (A \in ℕ \land B \in ℕ) \to (\frac{A}{A \gcd B} \in Odd \lor \frac{B}{A \gcd B} \in Odd)$

Metamath Proof Explorer

Theorem divgcdoddALTV

Proof