divgcdodd

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

		Ref	Expression
	Assertion	divgcdodd	$⊢ (A \in ℕ \land B \in ℕ) \to (\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B}))$

Proof

Step	Hyp	Ref	Expression
1		n2dvds1	$⊢ \neg 2 ∥ 1$
2		2z	$⊢ 2 \in ℤ$
3		nnz	$⊢ A \in ℕ \to A \in ℤ$
4		nnz	$⊢ B \in ℕ \to B \in ℤ$
5		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
6	3 4 5	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
7	6	simpld	$⊢ (A \in ℕ \land B \in ℕ) \to (A \gcd B) ∥ A$
8		gcdnncl	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℕ$
9	8	nnzd	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℤ$
10	8	nnne0d	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \neq 0$
11	3	adantr	$⊢ (A \in ℕ \land B \in ℕ) \to A \in ℤ$
12		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 ℤ)$
13	9 10 11 12	syl3anc	$⊢ (A \in ℕ \land B \in ℕ) \to ((A \gcd B) ∥ A \leftrightarrow \frac{A}{A \gcd B} \in ℤ)$
14	7 13	mpbid	$⊢ (A \in ℕ \land B \in ℕ) \to \frac{A}{A \gcd B} \in ℤ$
15	6	simprd	$⊢ (A \in ℕ \land B \in ℕ) \to (A \gcd B) ∥ B$
16	4	adantl	$⊢ (A \in ℕ \land B \in ℕ) \to B \in ℤ$
17		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 ℤ)$
18	9 10 16 17	syl3anc	$⊢ (A \in ℕ \land B \in ℕ) \to ((A \gcd B) ∥ B \leftrightarrow \frac{B}{A \gcd B} \in ℤ)$
19	15 18	mpbid	$⊢ (A \in ℕ \land B \in ℕ) \to \frac{B}{A \gcd B} \in ℤ$
20		dvdsgcdb	$⊢ (2 \in ℤ \land \frac{A}{A \gcd B} \in ℤ \land \frac{B}{A \gcd B} \in ℤ) \to ((2 ∥ (\frac{A}{A \gcd B}) \land 2 ∥ (\frac{B}{A \gcd B})) \leftrightarrow 2 ∥ ((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})))$
21	2 14 19 20	mp3an2i	$⊢ (A \in ℕ \land B \in ℕ) \to ((2 ∥ (\frac{A}{A \gcd B}) \land 2 ∥ (\frac{B}{A \gcd B})) \leftrightarrow 2 ∥ ((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})))$
22		gcddiv	$⊢ ((A \in ℤ \land B \in ℤ \land A \gcd B \in ℕ) \land ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)) \to \frac{A \gcd B}{A \gcd B} = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
23	11 16 8 6 22	syl31anc	$⊢ (A \in ℕ \land B \in ℕ) \to \frac{A \gcd B}{A \gcd B} = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
24	8	nncnd	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℂ$
25	24 10	dividd	$⊢ (A \in ℕ \land B \in ℕ) \to \frac{A \gcd B}{A \gcd B} = 1$
26	23 25	eqtr3d	$⊢ (A \in ℕ \land B \in ℕ) \to (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1$
27	26	breq2d	$⊢ (A \in ℕ \land B \in ℕ) \to (2 ∥ ((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})) \leftrightarrow 2 ∥ 1)$
28	27	biimpd	$⊢ (A \in ℕ \land B \in ℕ) \to (2 ∥ ((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})) \to 2 ∥ 1)$
29	21 28	sylbid	$⊢ (A \in ℕ \land B \in ℕ) \to ((2 ∥ (\frac{A}{A \gcd B}) \land 2 ∥ (\frac{B}{A \gcd B})) \to 2 ∥ 1)$
30	29	expdimp	$⊢ ((A \in ℕ \land B \in ℕ) \land 2 ∥ (\frac{A}{A \gcd B})) \to (2 ∥ (\frac{B}{A \gcd B}) \to 2 ∥ 1)$
31	1 30	mtoi	$⊢ ((A \in ℕ \land B \in ℕ) \land 2 ∥ (\frac{A}{A \gcd B})) \to \neg 2 ∥ (\frac{B}{A \gcd B})$
32	31	ex	$⊢ (A \in ℕ \land B \in ℕ) \to (2 ∥ (\frac{A}{A \gcd B}) \to \neg 2 ∥ (\frac{B}{A \gcd B}))$
33		imor	$⊢ (2 ∥ (\frac{A}{A \gcd B}) \to \neg 2 ∥ (\frac{B}{A \gcd B})) \leftrightarrow (\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B}))$
34	32 33	sylib	$⊢ (A \in ℕ \land B \in ℕ) \to (\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B}))$

Metamath Proof Explorer

Theorem divgcdodd

Proof