prmexpb

Description: Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012)

		Ref	Expression
	Assertion	prmexpb	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ)) \to (P^{M} = Q^{N} \leftrightarrow (P = Q \land M = N))$

Proof

Step	Hyp	Ref	Expression
1		prmz	$⊢ P \in ℙ \to P \in ℤ$
2	1	adantr	$⊢ (P \in ℙ \land Q \in ℙ) \to P \in ℤ$
3	2	3ad2ant1	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to P \in ℤ$
4		simp2l	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to M \in ℕ$
5		iddvdsexp	$⊢ (P \in ℤ \land M \in ℕ) \to P ∥ P^{M}$
6	3 4 5	syl2anc	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to P ∥ P^{M}$
7		breq2	$⊢ P^{M} = Q^{N} \to (P ∥ P^{M} \leftrightarrow P ∥ Q^{N})$
8	7	3ad2ant3	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to (P ∥ P^{M} \leftrightarrow P ∥ Q^{N})$
9		simp1l	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to P \in ℙ$
10		simp1r	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to Q \in ℙ$
11		simp2r	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to N \in ℕ$
12		prmdvdsexpb	$⊢ (P \in ℙ \land Q \in ℙ \land N \in ℕ) \to (P ∥ Q^{N} \leftrightarrow P = Q)$
13	9 10 11 12	syl3anc	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to (P ∥ Q^{N} \leftrightarrow P = Q)$
14	8 13	bitrd	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to (P ∥ P^{M} \leftrightarrow P = Q)$
15	6 14	mpbid	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to P = Q$
16	3	zred	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to P \in ℝ$
17	4	nnzd	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to M \in ℤ$
18	11	nnzd	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to N \in ℤ$
19		prmgt1	$⊢ P \in ℙ \to 1 < P$
20	19	ad2antrr	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ)) \to 1 < P$
21	20	3adant3	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to 1 < P$
22		simp3	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to P^{M} = Q^{N}$
23	15	oveq1d	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to P^{N} = Q^{N}$
24	22 23	eqtr4d	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to P^{M} = P^{N}$
25	16 17 18 21 24	expcand	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to M = N$
26	15 25	jca	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ) \land P^{M} = Q^{N}) \to (P = Q \land M = N)$
27	26	3expia	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ)) \to (P^{M} = Q^{N} \to (P = Q \land M = N))$
28		oveq12	$⊢ (P = Q \land M = N) \to P^{M} = Q^{N}$
29	27 28	impbid1	$⊢ ((P \in ℙ \land Q \in ℙ) \land (M \in ℕ \land N \in ℕ)) \to (P^{M} = Q^{N} \leftrightarrow (P = Q \land M = N))$

Metamath Proof Explorer

Theorem prmexpb

Proof