Metamath Proof Explorer

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 ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ N ∈ ℕ 0 → P ∥ Q N → P = Q

Proof

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