Metamath Proof Explorer

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	$⊢ φ \to A \in ℝ^{+}$
		exp11nnd.2	$⊢ φ \to B \in ℝ^{+}$
		exp11nnd.3	$⊢ φ \to N \in ℕ$
		exp11nnd.4	$⊢ φ \to A^{N} = B^{N}$
	Assertion	exp11nnd	$⊢ φ \to A = B$

Proof

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