dvdsexpnn

Description: Two positive integers are divisible iff their positive integer powers are. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) Generalized to arbitrary positive integer exponents. (Revised by SN, 20-Aug-2024)

		Ref	Expression
	Assertion	dvdsexpnn	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A ∥ B \leftrightarrow A^{N} ∥ B^{N})$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ A \in ℕ \to A \in ℤ$
2		nnz	$⊢ B \in ℕ \to B \in ℤ$
3		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
4		dvdsexpim	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ_{0}) \to (A ∥ B \to A^{N} ∥ B^{N})$
5	1 2 3 4	syl3an	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A ∥ B \to A^{N} ∥ B^{N})$
6		gcdnncl	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℕ$
7	6	nnrpd	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℝ^{+}$
8	7	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A \gcd B \in ℝ^{+}$
9	8	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to A \gcd B \in ℝ^{+}$
10		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to A \in ℕ$
11	10	nnrpd	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to A \in ℝ^{+}$
12		simpl3	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to N \in ℕ$
13		expgcd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
14	3 13	syl3an3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
15	14	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
16		simp1	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A \in ℕ$
17	3	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to N \in ℕ_{0}$
18	16 17	nnexpcld	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A^{N} \in ℕ$
19		simp2	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to B \in ℕ$
20	19 17	nnexpcld	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to B^{N} \in ℕ$
21		gcdeq	$⊢ (A^{N} \in ℕ \land B^{N} \in ℕ) \to (A^{N} \gcd B^{N} = A^{N} \leftrightarrow A^{N} ∥ B^{N})$
22	18 20 21	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A^{N} \gcd B^{N} = A^{N} \leftrightarrow A^{N} ∥ B^{N})$
23	22	biimpar	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to A^{N} \gcd B^{N} = A^{N}$
24	15 23	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to {(A \gcd B)}^{N} = A^{N}$
25	9 11 12 24	exp11nnd	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to A \gcd B = A$
26		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
27	26	simprd	$⊢ (A \in ℤ \land B \in ℤ) \to (A \gcd B) ∥ B$
28	1 2 27	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to (A \gcd B) ∥ B$
29	28	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B) ∥ B$
30	29	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to (A \gcd B) ∥ B$
31	25 30	eqbrtrrd	$⊢ ((A \in ℕ \land B \in ℕ \land N \in ℕ) \land A^{N} ∥ B^{N}) \to A ∥ B$
32	31	ex	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A^{N} ∥ B^{N} \to A ∥ B)$
33	5 32	impbid	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A ∥ B \leftrightarrow A^{N} ∥ B^{N})$

Metamath Proof Explorer

Theorem dvdsexpnn

Proof