expcan

Description: Cancellation law for integer exponentiation of reals. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	expcan	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (A^{M} = A^{N} \leftrightarrow M = N)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = y \to A^{x} = A^{y}$
2		oveq2	$⊢ x = M \to A^{x} = A^{M}$
3		oveq2	$⊢ x = N \to A^{x} = A^{N}$
4		zssre	$⊢ ℤ \subseteq ℝ$
5		simpl	$⊢ (A \in ℝ \land 1 < A) \to A \in ℝ$
6		0red	$⊢ (A \in ℝ \land 1 < A) \to 0 \in ℝ$
7		1red	$⊢ (A \in ℝ \land 1 < A) \to 1 \in ℝ$
8		0lt1	$⊢ 0 < 1$
9	8	a1i	$⊢ (A \in ℝ \land 1 < A) \to 0 < 1$
10		simpr	$⊢ (A \in ℝ \land 1 < A) \to 1 < A$
11	6 7 5 9 10	lttrd	$⊢ (A \in ℝ \land 1 < A) \to 0 < A$
12	5 11	elrpd	$⊢ (A \in ℝ \land 1 < A) \to A \in ℝ^{+}$
13		rpexpcl	$⊢ (A \in ℝ^{+} \land x \in ℤ) \to A^{x} \in ℝ^{+}$
14	12 13	sylan	$⊢ ((A \in ℝ \land 1 < A) \land x \in ℤ) \to A^{x} \in ℝ^{+}$
15	14	rpred	$⊢ ((A \in ℝ \land 1 < A) \land x \in ℤ) \to A^{x} \in ℝ$
16		simpll	$⊢ ((A \in ℝ \land 1 < A) \land (x \in ℤ \land y \in ℤ)) \to A \in ℝ$
17		simprl	$⊢ ((A \in ℝ \land 1 < A) \land (x \in ℤ \land y \in ℤ)) \to x \in ℤ$
18		simprr	$⊢ ((A \in ℝ \land 1 < A) \land (x \in ℤ \land y \in ℤ)) \to y \in ℤ$
19		simplr	$⊢ ((A \in ℝ \land 1 < A) \land (x \in ℤ \land y \in ℤ)) \to 1 < A$
20		ltexp2a	$⊢ ((A \in ℝ \land x \in ℤ \land y \in ℤ) \land (1 < A \land x < y)) \to A^{x} < A^{y}$
21	20	expr	$⊢ ((A \in ℝ \land x \in ℤ \land y \in ℤ) \land 1 < A) \to (x < y \to A^{x} < A^{y})$
22	16 17 18 19 21	syl31anc	$⊢ ((A \in ℝ \land 1 < A) \land (x \in ℤ \land y \in ℤ)) \to (x < y \to A^{x} < A^{y})$
23	1 2 3 4 15 22	eqord1	$⊢ ((A \in ℝ \land 1 < A) \land (M \in ℤ \land N \in ℤ)) \to (M = N \leftrightarrow A^{M} = A^{N})$
24	23	ancom2s	$⊢ ((A \in ℝ \land 1 < A) \land (N \in ℤ \land M \in ℤ)) \to (M = N \leftrightarrow A^{M} = A^{N})$
25	24	exp43	$⊢ A \in ℝ \to (1 < A \to (N \in ℤ \to (M \in ℤ \to (M = N \leftrightarrow A^{M} = A^{N}))))$
26	25	com24	$⊢ A \in ℝ \to (M \in ℤ \to (N \in ℤ \to (1 < A \to (M = N \leftrightarrow A^{M} = A^{N}))))$
27	26	3imp1	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (M = N \leftrightarrow A^{M} = A^{N})$
28	27	bicomd	$⊢ ((A \in ℝ \land M \in ℤ \land N \in ℤ) \land 1 < A) \to (A^{M} = A^{N} \leftrightarrow M = N)$

Metamath Proof Explorer

Theorem expcan

Proof