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	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	exp11nnd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	exp11nnd.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	exp11nnd.4	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
Assertion	exp11nnd	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		exp11nnd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		exp11nnd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3		exp11nnd.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		exp11nnd.4	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
5	1	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6	3	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7	5 6	reexpcld	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
8	2	rpred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
9	8 6	reexpcld	⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℝ )
10	7 9	lttri3d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) ↔ ( ¬ ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ∧ ¬ ( 𝐵 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑁 ) ) ) )
11	4 10	mpbid	⊢ ( 𝜑 → ( ¬ ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ∧ ¬ ( 𝐵 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑁 ) ) )
12	1 2 3	ltexp1d	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ) )
13	12	notbid	⊢ ( 𝜑 → ( ¬ 𝐴 < 𝐵 ↔ ¬ ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ) )
14	2 1 3	ltexp1d	⊢ ( 𝜑 → ( 𝐵 < 𝐴 ↔ ( 𝐵 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑁 ) ) )
15	14	notbid	⊢ ( 𝜑 → ( ¬ 𝐵 < 𝐴 ↔ ¬ ( 𝐵 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑁 ) ) )
16	13 15	anbi12d	⊢ ( 𝜑 → ( ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) ↔ ( ¬ ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ∧ ¬ ( 𝐵 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑁 ) ) ) )
17	11 16	mpbird	⊢ ( 𝜑 → ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) )
18	5 8	lttri3d	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ↔ ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) ) )
19	17 18	mpbird	⊢ ( 𝜑 → 𝐴 = 𝐵 )