Theorem exp11nnd

Description: The function elevating nonnegative reals to a positive integer is one-to-one. Similar to sq11d for positive real bases and positive integer exponents. The base cannot be generalized much further, since if N is even then we have A ^ N = -u A ^ N . (Contributed by SN, 14-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		exp11nnd.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		exp11nnd.2	$$⊢\phi \to B\in {ℝ}^{+}$$
3		exp11nnd.3	$$⊢\phi \to N\in \mathbb{N}$$
4		exp11nnd.4	$$⊢\phi \to A^N=B^N$$
5	1	rpred	$$⊢\phi \to A\in ℝ$$
6	3	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7	5 6	reexpcld	$$⊢\phi \to A^N\in ℝ$$
8	2	rpred	$$⊢\phi \to B\in ℝ$$
9	8 6	reexpcld	$$⊢\phi \to B^N\in ℝ$$
10	7 9	lttri3d	$$⊢\phi \to \left(A^N=B^N\leftrightarrow \left(\neg A^N<B^N\wedge \neg B^N<A^N\right)\right)$$
11	4 10	mpbid	$$⊢\phi \to \left(\neg A^N<B^N\wedge \neg B^N<A^N\right)$$
12	1 2 3	ltexp1d	$$⊢\phi \to \left(A<B\leftrightarrow A^N<B^N\right)$$
13	12	notbid	$$⊢\phi \to \left(\neg A<B\leftrightarrow \neg A^N<B^N\right)$$
14	2 1 3	ltexp1d	$$⊢\phi \to \left(B<A\leftrightarrow B^N<A^N\right)$$
15	14	notbid	$$⊢\phi \to \left(\neg B<A\leftrightarrow \neg B^N<A^N\right)$$
16	13 15	anbi12d	$$⊢\phi \to \left(\left(\neg A<B\wedge \neg B<A\right)\leftrightarrow \left(\neg A^N<B^N\wedge \neg B^N<A^N\right)\right)$$
17	11 16	mpbird	$$⊢\phi \to \left(\neg A<B\wedge \neg B<A\right)$$
18	5 8	lttri3d	$$⊢\phi \to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$
19	17 18	mpbird	$$⊢\phi \to A=B$$