fltdvdsabdvdsc

Description: Any factor of both A and B also divides C . This establishes the validity of fltabcoprmex . (Contributed by SN, 21-Aug-2024)

Step	Hyp	Ref	Expression
1		fltdvdsabdvdsc.a	$⊢ φ \to A \in ℕ$
2		fltdvdsabdvdsc.b	$⊢ φ \to B \in ℕ$
3		fltdvdsabdvdsc.c	$⊢ φ \to C \in ℕ$
4		fltdvdsabdvdsc.n	$⊢ φ \to N \in ℕ$
5		fltdvdsabdvdsc.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
6		gcdnncl	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℕ$
7	1 2 6	syl2anc	$⊢ φ \to A \gcd B \in ℕ$
8	4	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
9	7 8	nnexpcld	$⊢ φ \to {(A \gcd B)}^{N} \in ℕ$
10	9	nnzd	$⊢ φ \to {(A \gcd B)}^{N} \in ℤ$
11	1 8	nnexpcld	$⊢ φ \to A^{N} \in ℕ$
12	11	nnzd	$⊢ φ \to A^{N} \in ℤ$
13	2 8	nnexpcld	$⊢ φ \to B^{N} \in ℕ$
14	13	nnzd	$⊢ φ \to B^{N} \in ℤ$
15	7	nnzd	$⊢ φ \to A \gcd B \in ℤ$
16	1	nnzd	$⊢ φ \to A \in ℤ$
17	2	nnzd	$⊢ φ \to B \in ℤ$
18		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
19	16 17 18	syl2anc	$⊢ φ \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
20	19	simpld	$⊢ φ \to (A \gcd B) ∥ A$
21	15 16 8 20	dvdsexpad	$⊢ φ \to {(A \gcd B)}^{N} ∥ A^{N}$
22	19	simprd	$⊢ φ \to (A \gcd B) ∥ B$
23	15 17 8 22	dvdsexpad	$⊢ φ \to {(A \gcd B)}^{N} ∥ B^{N}$
24	10 12 14 21 23	dvds2addd	$⊢ φ \to {(A \gcd B)}^{N} ∥ (A^{N} + B^{N})$
25	24 5	breqtrd	$⊢ φ \to {(A \gcd B)}^{N} ∥ C^{N}$
26		dvdsexpnn	$⊢ (A \gcd B \in ℕ \land C \in ℕ \land N \in ℕ) \to ((A \gcd B) ∥ C \leftrightarrow {(A \gcd B)}^{N} ∥ C^{N})$
27	7 3 4 26	syl3anc	$⊢ φ \to ((A \gcd B) ∥ C \leftrightarrow {(A \gcd B)}^{N} ∥ C^{N})$
28	25 27	mpbird	$⊢ φ \to (A \gcd B) ∥ C$

Metamath Proof Explorer