nn0rppwr

Description: If A and B are relatively prime, then so are A ^ N and B ^ N . rppwr extended to nonnegative integers. Less general than rpexp12i . (Contributed by Steven Nguyen, 4-Apr-2023)

		Ref	Expression
	Assertion	nn0rppwr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N \in ℕ_{0}) \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1)$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		elnn0	$⊢ A \in ℕ_{0} \leftrightarrow (A \in ℕ \lor A = 0)$
3		elnn0	$⊢ B \in ℕ_{0} \leftrightarrow (B \in ℕ \lor B = 0)$
4		rppwr	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1)$
5	4	3expia	$⊢ (A \in ℕ \land B \in ℕ) \to (N \in ℕ \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1))$
6		simp1l	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to A = 0$
7	6	oveq1d	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to A^{N} = 0^{N}$
8		0exp	$⊢ N \in ℕ \to 0^{N} = 0$
9	8	3ad2ant2	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to 0^{N} = 0$
10	7 9	eqtrd	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to A^{N} = 0$
11	6	oveq1d	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to A \gcd B = 0 \gcd B$
12		simp3	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to A \gcd B = 1$
13		simp1r	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to B \in ℕ$
14		nnz	$⊢ B \in ℕ \to B \in ℤ$
15		gcd0id	$⊢ B \in ℤ \to 0 \gcd B = \|B\|$
16	14 15	syl	$⊢ B \in ℕ \to 0 \gcd B = \|B\|$
17		nnre	$⊢ B \in ℕ \to B \in ℝ$
18		0red	$⊢ B \in ℕ \to 0 \in ℝ$
19		nngt0	$⊢ B \in ℕ \to 0 < B$
20	18 17 19	ltled	$⊢ B \in ℕ \to 0 \leq B$
21	17 20	absidd	$⊢ B \in ℕ \to \|B\| = B$
22	16 21	eqtrd	$⊢ B \in ℕ \to 0 \gcd B = B$
23	13 22	syl	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to 0 \gcd B = B$
24	11 12 23	3eqtr3rd	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to B = 1$
25	24	oveq1d	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to B^{N} = 1^{N}$
26		nnz	$⊢ N \in ℕ \to N \in ℤ$
27	26	3ad2ant2	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to N \in ℤ$
28		1exp	$⊢ N \in ℤ \to 1^{N} = 1$
29	27 28	syl	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to 1^{N} = 1$
30	25 29	eqtrd	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to B^{N} = 1$
31	10 30	oveq12d	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to A^{N} \gcd B^{N} = 0 \gcd 1$
32		1z	$⊢ 1 \in ℤ$
33		gcd0id	$⊢ 1 \in ℤ \to 0 \gcd 1 = \|1\|$
34	32 33	ax-mp	$⊢ 0 \gcd 1 = \|1\|$
35		abs1	$⊢ \|1\| = 1$
36	34 35	eqtri	$⊢ 0 \gcd 1 = 1$
37	31 36	eqtrdi	$⊢ ((A = 0 \land B \in ℕ) \land N \in ℕ \land A \gcd B = 1) \to A^{N} \gcd B^{N} = 1$
38	37	3exp	$⊢ (A = 0 \land B \in ℕ) \to (N \in ℕ \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1))$
39		simp1r	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to B = 0$
40	39	oveq2d	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A \gcd B = A \gcd 0$
41		simp3	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A \gcd B = 1$
42		simp1l	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A \in ℕ$
43	42	nnnn0d	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A \in ℕ_{0}$
44		nn0gcdid0	$⊢ A \in ℕ_{0} \to A \gcd 0 = A$
45	43 44	syl	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A \gcd 0 = A$
46	40 41 45	3eqtr3rd	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A = 1$
47	46	oveq1d	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A^{N} = 1^{N}$
48	26	3ad2ant2	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to N \in ℤ$
49	48 28	syl	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to 1^{N} = 1$
50	47 49	eqtrd	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A^{N} = 1$
51	39	oveq1d	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to B^{N} = 0^{N}$
52	8	3ad2ant2	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to 0^{N} = 0$
53	51 52	eqtrd	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to B^{N} = 0$
54	50 53	oveq12d	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A^{N} \gcd B^{N} = 1 \gcd 0$
55		1nn0	$⊢ 1 \in ℕ_{0}$
56		nn0gcdid0	$⊢ 1 \in ℕ_{0} \to 1 \gcd 0 = 1$
57	55 56	mp1i	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to 1 \gcd 0 = 1$
58	54 57	eqtrd	$⊢ ((A \in ℕ \land B = 0) \land N \in ℕ \land A \gcd B = 1) \to A^{N} \gcd B^{N} = 1$
59	58	3exp	$⊢ (A \in ℕ \land B = 0) \to (N \in ℕ \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1))$
60		oveq12	$⊢ (A = 0 \land B = 0) \to A \gcd B = 0 \gcd 0$
61		gcd0val	$⊢ 0 \gcd 0 = 0$
62		0ne1	$⊢ 0 \neq 1$
63	61 62	eqnetri	$⊢ 0 \gcd 0 \neq 1$
64	63	a1i	$⊢ (A = 0 \land B = 0) \to 0 \gcd 0 \neq 1$
65	60 64	eqnetrd	$⊢ (A = 0 \land B = 0) \to A \gcd B \neq 1$
66	65	neneqd	$⊢ (A = 0 \land B = 0) \to \neg A \gcd B = 1$
67	66	pm2.21d	$⊢ (A = 0 \land B = 0) \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1)$
68	67	a1d	$⊢ (A = 0 \land B = 0) \to (N \in ℕ \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1))$
69	5 38 59 68	ccase	$⊢ ((A \in ℕ \lor A = 0) \land (B \in ℕ \lor B = 0)) \to (N \in ℕ \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1))$
70	2 3 69	syl2anb	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (N \in ℕ \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1))$
71		oveq2	$⊢ N = 0 \to A^{N} = A^{0}$
72	71	3ad2ant3	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to A^{N} = A^{0}$
73		nn0cn	$⊢ A \in ℕ_{0} \to A \in ℂ$
74	73	3ad2ant1	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to A \in ℂ$
75	74	exp0d	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to A^{0} = 1$
76	72 75	eqtrd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to A^{N} = 1$
77		oveq2	$⊢ N = 0 \to B^{N} = B^{0}$
78	77	3ad2ant3	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to B^{N} = B^{0}$
79		nn0cn	$⊢ B \in ℕ_{0} \to B \in ℂ$
80	79	3ad2ant2	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to B \in ℂ$
81	80	exp0d	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to B^{0} = 1$
82	78 81	eqtrd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to B^{N} = 1$
83	76 82	oveq12d	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to A^{N} \gcd B^{N} = 1 \gcd 1$
84		1gcd	$⊢ 1 \in ℤ \to 1 \gcd 1 = 1$
85	32 84	mp1i	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to 1 \gcd 1 = 1$
86	83 85	eqtrd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N = 0) \to A^{N} \gcd B^{N} = 1$
87	86	3expia	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (N = 0 \to A^{N} \gcd B^{N} = 1)$
88	87	a1dd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (N = 0 \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1))$
89	70 88	jaod	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to ((N \in ℕ \lor N = 0) \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1))$
90	89	3impia	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land (N \in ℕ \lor N = 0)) \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1)$
91	1 90	syl3an3b	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N \in ℕ_{0}) \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1)$

Metamath Proof Explorer

Theorem nn0rppwr

Proof