Theorem exp11nnd

Description: 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	|- ( ph -> A e. RR+ )
	exp11nnd.2	|- ( ph -> B e. RR+ )
	exp11nnd.3	|- ( ph -> N e. NN )
	exp11nnd.4	|- ( ph -> ( A ^ N ) = ( B ^ N ) )
Assertion	exp11nnd	|- ( ph -> A = B )

Proof

Step	Hyp	Ref	Expression
1		exp11nnd.1	|- ( ph -> A e. RR+ )
2		exp11nnd.2	|- ( ph -> B e. RR+ )
3		exp11nnd.3	|- ( ph -> N e. NN )
4		exp11nnd.4	|- ( ph -> ( A ^ N ) = ( B ^ N ) )
5	1	rpred	|- ( ph -> A e. RR )
6	3	nnnn0d	|- ( ph -> N e. NN0 )
7	5 6	reexpcld	|- ( ph -> ( A ^ N ) e. RR )
8	2	rpred	|- ( ph -> B e. RR )
9	8 6	reexpcld	|- ( ph -> ( B ^ N ) e. RR )
10	7 9	lttri3d	|- ( ph -> ( ( A ^ N ) = ( B ^ N ) <-> ( -. ( A ^ N ) < ( B ^ N ) /\ -. ( B ^ N ) < ( A ^ N ) ) ) )
11	4 10	mpbid	|- ( ph -> ( -. ( A ^ N ) < ( B ^ N ) /\ -. ( B ^ N ) < ( A ^ N ) ) )
12	1 2 3	ltexp1d	|- ( ph -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) )
13	12	notbid	|- ( ph -> ( -. A < B <-> -. ( A ^ N ) < ( B ^ N ) ) )
14	2 1 3	ltexp1d	|- ( ph -> ( B < A <-> ( B ^ N ) < ( A ^ N ) ) )
15	14	notbid	|- ( ph -> ( -. B < A <-> -. ( B ^ N ) < ( A ^ N ) ) )
16	13 15	anbi12d	|- ( ph -> ( ( -. A < B /\ -. B < A ) <-> ( -. ( A ^ N ) < ( B ^ N ) /\ -. ( B ^ N ) < ( A ^ N ) ) ) )
17	11 16	mpbird	|- ( ph -> ( -. A < B /\ -. B < A ) )
18	5 8	lttri3d	|- ( ph -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
19	17 18	mpbird	|- ( ph -> A = B )