Theorem exp11d

Description: sq11d for positive real bases and nonzero exponents. (Contributed by Steven Nguyen, 6-Apr-2023)

	Ref	Expression
Hypotheses	exp11d.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	exp11d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
	exp11d.3	$$⊢\phi \to N\in \mathbb{Z}$$
	exp11d.4	$$⊢\phi \to N\ne 0$$
	exp11d.5	$$⊢\phi \to A^N=B^N$$
Assertion	exp11d	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		exp11d.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		exp11d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
3		exp11d.3	$$⊢\phi \to N\in \mathbb{Z}$$
4		exp11d.4	$$⊢\phi \to N\ne 0$$
5		exp11d.5	$$⊢\phi \to A^N=B^N$$
6	1	rpcnd	$$⊢\phi \to A\in ℂ$$
7	1	rpne0d	$$⊢\phi \to A\ne 0$$
8	6 7 3	cxpexpzd	$$⊢\phi \to A^N=A^N$$
9	2	rpcnd	$$⊢\phi \to B\in ℂ$$
10	2	rpne0d	$$⊢\phi \to B\ne 0$$
11	9 10 3	cxpexpzd	$$⊢\phi \to B^N=B^N$$
12	5 8 11	3eqtr4d	$$⊢\phi \to A^N=B^N$$
13	12	oveq1d	$$⊢\phi \to {\left(A^N\right)}^{\frac{1}{N}}={\left(B^N\right)}^{\frac{1}{N}}$$
14	3	zcnd	$$⊢\phi \to N\in ℂ$$
15	14 4	recidd	$$⊢\phi \to N\left(\frac{1}{N}\right)=1$$
16	15	oveq2d	$$⊢\phi \to A^{N\left(\frac{1}{N}\right)}=A^1$$
17	3	zred	$$⊢\phi \to N\in ℝ$$
18	14 4	reccld	$$⊢\phi \to \frac{1}{N}\in ℂ$$
19	1 17 18	cxpmuld	$$⊢\phi \to A^{N\left(\frac{1}{N}\right)}={\left(A^N\right)}^{\frac{1}{N}}$$
20	6	cxp1d	$$⊢\phi \to A^1=A$$
21	16 19 20	3eqtr3d	$$⊢\phi \to {\left(A^N\right)}^{\frac{1}{N}}=A$$
22	15	oveq2d	$$⊢\phi \to B^{N\left(\frac{1}{N}\right)}=B^1$$
23	2 17 18	cxpmuld	$$⊢\phi \to B^{N\left(\frac{1}{N}\right)}={\left(B^N\right)}^{\frac{1}{N}}$$
24	9	cxp1d	$$⊢\phi \to B^1=B$$
25	22 23 24	3eqtr3d	$$⊢\phi \to {\left(B^N\right)}^{\frac{1}{N}}=B$$
26	13 21 25	3eqtr3d	$$⊢\phi \to A=B$$