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

Metamath Proof Explorer

Theorem pcprendvds2

Description: Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Hypotheses pclem.1 ⊢ 𝐴 = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
pclem.2 ⊢ 𝑆 = sup ( 𝐴 , ℝ , < )
Assertion pcprendvds2 ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 pclem.1 ⊢ 𝐴 = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
2 pclem.2 ⊢ 𝑆 = sup ( 𝐴 , ℝ , < )
3 1 2 pcprendvds ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 )
4 eluz2nn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ )
5 4 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℕ )
6 5 nnzd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℤ )
7 1 2 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )
8 7 simprd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 )
9 7 simpld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑆 ∈ ℕ0 )
10 5 9 nnexpcld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ∈ ℕ )
11 10 nnzd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ∈ ℤ )
12 10 nnne0d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ≠ 0 )
13 simprl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℤ )
14 dvdsval2 ⊢ ( ( ( 𝑃 ↑ 𝑆 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑆 ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) ∈ ℤ ) )
15 11 12 13 14 syl3anc ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) ∈ ℤ ) )
16 8 15 mpbid ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) ∈ ℤ )
17 dvdscmul ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑆 ) ∈ ℤ ) → ( 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) → ( ( 𝑃 ↑ 𝑆 ) · 𝑃 ) ∥ ( ( 𝑃 ↑ 𝑆 ) · ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) ) ) )
18 6 16 11 17 syl3anc ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) → ( ( 𝑃 ↑ 𝑆 ) · 𝑃 ) ∥ ( ( 𝑃 ↑ 𝑆 ) · ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) ) ) )
19 5 nncnd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℂ )
20 19 9 expp1d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑆 + 1 ) ) = ( ( 𝑃 ↑ 𝑆 ) · 𝑃 ) )
21 20 eqcomd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑆 ) · 𝑃 ) = ( 𝑃 ↑ ( 𝑆 + 1 ) ) )
22 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
23 22 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℂ )
24 10 nncnd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ∈ ℂ )
25 23 24 12 divcan2d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑆 ) · ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) ) = 𝑁 )
26 21 25 breq12d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( ( 𝑃 ↑ 𝑆 ) · 𝑃 ) ∥ ( ( 𝑃 ↑ 𝑆 ) · ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) ) ↔ ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 ) )
27 18 26 sylibd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) → ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 ) )
28 3 27 mtod ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑆 ) ) )