nn0expgcd

Description: Exponentiation distributes over GCD. nn0gcdsq extended to nonnegative exponents. expgcd extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ A \in ℕ_{0} \leftrightarrow (A \in ℕ \lor A = 0)$
2		elnn0	$⊢ B \in ℕ_{0} \leftrightarrow (B \in ℕ \lor B = 0)$
3		expgcd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
4	3	3expia	$⊢ (A \in ℕ \land B \in ℕ) \to (N \in ℕ_{0} \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
5		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
6		0exp	$⊢ N \in ℕ \to 0^{N} = 0$
7	6	3ad2ant3	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to 0^{N} = 0$
8	7	oveq1d	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to 0^{N} \gcd B^{N} = 0 \gcd B^{N}$
9		simp2	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to B \in ℕ$
10		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
11	10	3ad2ant3	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to N \in ℕ_{0}$
12	9 11	nnexpcld	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to B^{N} \in ℕ$
13	12	nnzd	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to B^{N} \in ℤ$
14		gcd0id	$⊢ B^{N} \in ℤ \to 0 \gcd B^{N} = \|B^{N}\|$
15	13 14	syl	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to 0 \gcd B^{N} = \|B^{N}\|$
16	12	nnred	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to B^{N} \in ℝ$
17		0red	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to 0 \in ℝ$
18	12	nngt0d	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to 0 < B^{N}$
19	17 16 18	ltled	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to 0 \leq B^{N}$
20	16 19	absidd	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to \|B^{N}\| = B^{N}$
21	8 15 20	3eqtrrd	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to B^{N} = 0^{N} \gcd B^{N}$
22		oveq1	$⊢ A = 0 \to A \gcd B = 0 \gcd B$
23	22	3ad2ant1	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to A \gcd B = 0 \gcd B$
24		nnz	$⊢ B \in ℕ \to B \in ℤ$
25	24	3ad2ant2	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to B \in ℤ$
26		gcd0id	$⊢ B \in ℤ \to 0 \gcd B = \|B\|$
27	25 26	syl	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to 0 \gcd B = \|B\|$
28		nnre	$⊢ B \in ℕ \to B \in ℝ$
29		0red	$⊢ B \in ℕ \to 0 \in ℝ$
30		nngt0	$⊢ B \in ℕ \to 0 < B$
31	29 28 30	ltled	$⊢ B \in ℕ \to 0 \leq B$
32	28 31	absidd	$⊢ B \in ℕ \to \|B\| = B$
33	32	3ad2ant2	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to \|B\| = B$
34	23 27 33	3eqtrd	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to A \gcd B = B$
35	34	oveq1d	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to {(A \gcd B)}^{N} = B^{N}$
36		oveq1	$⊢ A = 0 \to A^{N} = 0^{N}$
37	36	3ad2ant1	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to A^{N} = 0^{N}$
38	37	oveq1d	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to A^{N} \gcd B^{N} = 0^{N} \gcd B^{N}$
39	21 35 38	3eqtr4d	$⊢ (A = 0 \land B \in ℕ \land N \in ℕ) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
40	39	3expia	$⊢ (A = 0 \land B \in ℕ) \to (N \in ℕ \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
41		1z	$⊢ 1 \in ℤ$
42		gcd1	$⊢ 1 \in ℤ \to 1 \gcd 1 = 1$
43	41 42	ax-mp	$⊢ 1 \gcd 1 = 1$
44	43	eqcomi	$⊢ 1 = 1 \gcd 1$
45		simp1	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to A = 0$
46	45	oveq1d	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to A \gcd B = 0 \gcd B$
47		simp2	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to B \in ℕ$
48	47	nnzd	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to B \in ℤ$
49	48 26	syl	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to 0 \gcd B = \|B\|$
50	32	3ad2ant2	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to \|B\| = B$
51	46 49 50	3eqtrd	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to A \gcd B = B$
52		simp3	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to N = 0$
53	51 52	oveq12d	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to {(A \gcd B)}^{N} = B^{0}$
54	47	nncnd	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to B \in ℂ$
55	54	exp0d	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to B^{0} = 1$
56	53 55	eqtrd	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to {(A \gcd B)}^{N} = 1$
57	45 52	oveq12d	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to A^{N} = 0^{0}$
58		0exp0e1	$⊢ 0^{0} = 1$
59	58	a1i	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to 0^{0} = 1$
60	57 59	eqtrd	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to A^{N} = 1$
61	52	oveq2d	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to B^{N} = B^{0}$
62	61 55	eqtrd	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to B^{N} = 1$
63	60 62	oveq12d	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to A^{N} \gcd B^{N} = 1 \gcd 1$
64	44 56 63	3eqtr4a	$⊢ (A = 0 \land B \in ℕ \land N = 0) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
65	64	3expia	$⊢ (A = 0 \land B \in ℕ) \to (N = 0 \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
66	40 65	jaod	$⊢ (A = 0 \land B \in ℕ) \to ((N \in ℕ \lor N = 0) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
67	5 66	syl5bi	$⊢ (A = 0 \land B \in ℕ) \to (N \in ℕ_{0} \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
68		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
69	68	3ad2ant1	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to A \in ℕ_{0}$
70	10	3ad2ant3	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to N \in ℕ_{0}$
71	69 70	nn0expcld	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to A^{N} \in ℕ_{0}$
72		nn0gcdid0	$⊢ A^{N} \in ℕ_{0} \to A^{N} \gcd 0 = A^{N}$
73	71 72	syl	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to A^{N} \gcd 0 = A^{N}$
74		simp2	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to B = 0$
75	74	oveq1d	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to B^{N} = 0^{N}$
76	6	3ad2ant3	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to 0^{N} = 0$
77	75 76	eqtrd	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to B^{N} = 0$
78	77	oveq2d	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to A^{N} \gcd B^{N} = A^{N} \gcd 0$
79	74	oveq2d	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to A \gcd B = A \gcd 0$
80		nn0gcdid0	$⊢ A \in ℕ_{0} \to A \gcd 0 = A$
81	68 80	syl	$⊢ A \in ℕ \to A \gcd 0 = A$
82	81	3ad2ant1	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to A \gcd 0 = A$
83	79 82	eqtrd	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to A \gcd B = A$
84	83	oveq1d	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to {(A \gcd B)}^{N} = A^{N}$
85	73 78 84	3eqtr4rd	$⊢ (A \in ℕ \land B = 0 \land N \in ℕ) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
86	85	3expia	$⊢ (A \in ℕ \land B = 0) \to (N \in ℕ \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
87		nncn	$⊢ A \in ℕ \to A \in ℂ$
88	87	exp0d	$⊢ A \in ℕ \to A^{0} = 1$
89	88 43	eqtr4di	$⊢ A \in ℕ \to A^{0} = 1 \gcd 1$
90	81	oveq1d	$⊢ A \in ℕ \to {(A \gcd 0)}^{0} = A^{0}$
91	58	a1i	$⊢ A \in ℕ \to 0^{0} = 1$
92	88 91	oveq12d	$⊢ A \in ℕ \to A^{0} \gcd 0^{0} = 1 \gcd 1$
93	89 90 92	3eqtr4d	$⊢ A \in ℕ \to {(A \gcd 0)}^{0} = A^{0} \gcd 0^{0}$
94	93	3ad2ant1	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to {(A \gcd 0)}^{0} = A^{0} \gcd 0^{0}$
95		simp2	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to B = 0$
96	95	oveq2d	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to A \gcd B = A \gcd 0$
97		simp3	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to N = 0$
98	96 97	oveq12d	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to {(A \gcd B)}^{N} = {(A \gcd 0)}^{0}$
99	97	oveq2d	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to A^{N} = A^{0}$
100	95 97	oveq12d	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to B^{N} = 0^{0}$
101	99 100	oveq12d	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to A^{N} \gcd B^{N} = A^{0} \gcd 0^{0}$
102	94 98 101	3eqtr4d	$⊢ (A \in ℕ \land B = 0 \land N = 0) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
103	102	3expia	$⊢ (A \in ℕ \land B = 0) \to (N = 0 \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
104	86 103	jaod	$⊢ (A \in ℕ \land B = 0) \to ((N \in ℕ \lor N = 0) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
105	5 104	syl5bi	$⊢ (A \in ℕ \land B = 0) \to (N \in ℕ_{0} \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
106		gcd0val	$⊢ 0 \gcd 0 = 0$
107	6 106	eqtr4di	$⊢ N \in ℕ \to 0^{N} = 0 \gcd 0$
108	106	a1i	$⊢ N \in ℕ \to 0 \gcd 0 = 0$
109	108	oveq1d	$⊢ N \in ℕ \to {(0 \gcd 0)}^{N} = 0^{N}$
110	6 6	oveq12d	$⊢ N \in ℕ \to 0^{N} \gcd 0^{N} = 0 \gcd 0$
111	107 109 110	3eqtr4d	$⊢ N \in ℕ \to {(0 \gcd 0)}^{N} = 0^{N} \gcd 0^{N}$
112	111	3ad2ant3	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to {(0 \gcd 0)}^{N} = 0^{N} \gcd 0^{N}$
113		simp1	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to A = 0$
114		simp2	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to B = 0$
115	113 114	oveq12d	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to A \gcd B = 0 \gcd 0$
116	115	oveq1d	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to {(A \gcd B)}^{N} = {(0 \gcd 0)}^{N}$
117	113	oveq1d	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to A^{N} = 0^{N}$
118	114	oveq1d	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to B^{N} = 0^{N}$
119	117 118	oveq12d	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to A^{N} \gcd B^{N} = 0^{N} \gcd 0^{N}$
120	112 116 119	3eqtr4d	$⊢ (A = 0 \land B = 0 \land N \in ℕ) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
121	120	3expia	$⊢ (A = 0 \land B = 0) \to (N \in ℕ \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
122	58 43	eqtr4i	$⊢ 0^{0} = 1 \gcd 1$
123	106	oveq1i	$⊢ {(0 \gcd 0)}^{0} = 0^{0}$
124	58 58	oveq12i	$⊢ 0^{0} \gcd 0^{0} = 1 \gcd 1$
125	122 123 124	3eqtr4i	$⊢ {(0 \gcd 0)}^{0} = 0^{0} \gcd 0^{0}$
126		simp1	$⊢ (A = 0 \land B = 0 \land N = 0) \to A = 0$
127		simp2	$⊢ (A = 0 \land B = 0 \land N = 0) \to B = 0$
128	126 127	oveq12d	$⊢ (A = 0 \land B = 0 \land N = 0) \to A \gcd B = 0 \gcd 0$
129		simp3	$⊢ (A = 0 \land B = 0 \land N = 0) \to N = 0$
130	128 129	oveq12d	$⊢ (A = 0 \land B = 0 \land N = 0) \to {(A \gcd B)}^{N} = {(0 \gcd 0)}^{0}$
131	126 129	oveq12d	$⊢ (A = 0 \land B = 0 \land N = 0) \to A^{N} = 0^{0}$
132	127 129	oveq12d	$⊢ (A = 0 \land B = 0 \land N = 0) \to B^{N} = 0^{0}$
133	131 132	oveq12d	$⊢ (A = 0 \land B = 0 \land N = 0) \to A^{N} \gcd B^{N} = 0^{0} \gcd 0^{0}$
134	125 130 133	3eqtr4a	$⊢ (A = 0 \land B = 0 \land N = 0) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$
135	134	3expia	$⊢ (A = 0 \land B = 0) \to (N = 0 \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
136	121 135	jaod	$⊢ (A = 0 \land B = 0) \to ((N \in ℕ \lor N = 0) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
137	5 136	syl5bi	$⊢ (A = 0 \land B = 0) \to (N \in ℕ_{0} \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
138	4 67 105 137	ccase	$⊢ ((A \in ℕ \lor A = 0) \land (B \in ℕ \lor B = 0)) \to (N \in ℕ_{0} \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
139	1 2 138	syl2anb	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (N \in ℕ_{0} \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N})$
140	139	3impia	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land N \in ℕ_{0}) \to {(A \gcd B)}^{N} = A^{N} \gcd B^{N}$

Metamath Proof Explorer

Theorem nn0expgcd

Proof