Theorem prmdvdsexpr

Description: If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Assertion	prmdvdsexpr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2		prmdvdsexpb	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) ↔ 𝑃 = 𝑄 ) )
3	2	biimpd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) )
4	3	3expia	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑁 ∈ ℕ → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) ) )
5		prmnn	⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℕ )
6	5	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → 𝑄 ∈ ℕ )
7	6	nncnd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → 𝑄 ∈ ℂ )
8	7	exp0d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑄 ↑ 0 ) = 1 )
9	8	breq2d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑃 ∥ ( 𝑄 ↑ 0 ) ↔ 𝑃 ∥ 1 ) )
10		nprmdvds1	⊢ ( 𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1 )
11	10	pm2.21d	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∥ 1 → 𝑃 = 𝑄 ) )
12	11	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑃 ∥ 1 → 𝑃 = 𝑄 ) )
13	9 12	sylbid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑃 ∥ ( 𝑄 ↑ 0 ) → 𝑃 = 𝑄 ) )
14		oveq2	⊢ ( 𝑁 = 0 → ( 𝑄 ↑ 𝑁 ) = ( 𝑄 ↑ 0 ) )
15	14	breq2d	⊢ ( 𝑁 = 0 → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) ↔ 𝑃 ∥ ( 𝑄 ↑ 0 ) ) )
16	15	imbi1d	⊢ ( 𝑁 = 0 → ( ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) ↔ ( 𝑃 ∥ ( 𝑄 ↑ 0 ) → 𝑃 = 𝑄 ) ) )
17	13 16	syl5ibrcom	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑁 = 0 → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) ) )
18	4 17	jaod	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) ) )
19	1 18	biimtrid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑁 ∈ ℕ0 → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) ) )
20	19	3impia	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) )