This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ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 ) → ( 𝑃 ∥ ( 𝑄 ↑ 𝑁 ) → 𝑃 = 𝑄 ) )