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

Metamath Proof Explorer

Theorem pcprendvds

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 pcprendvds ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 )

Proof

Step Hyp Ref Expression
1 pclem.1 ⊢ 𝐴 = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
2 pclem.2 ⊢ 𝑆 = sup ( 𝐴 , ℝ , < )
3 1 2 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )
4 3 simpld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑆 ∈ ℕ0 )
5 nn0re ⊢ ( 𝑆 ∈ ℕ0 → 𝑆 ∈ ℝ )
6 ltp1 ⊢ ( 𝑆 ∈ ℝ → 𝑆 < ( 𝑆 + 1 ) )
7 peano2re ⊢ ( 𝑆 ∈ ℝ → ( 𝑆 + 1 ) ∈ ℝ )
8 ltnle ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝑆 + 1 ) ∈ ℝ ) → ( 𝑆 < ( 𝑆 + 1 ) ↔ ¬ ( 𝑆 + 1 ) ≤ 𝑆 ) )
9 7 8 mpdan ⊢ ( 𝑆 ∈ ℝ → ( 𝑆 < ( 𝑆 + 1 ) ↔ ¬ ( 𝑆 + 1 ) ≤ 𝑆 ) )
10 6 9 mpbid ⊢ ( 𝑆 ∈ ℝ → ¬ ( 𝑆 + 1 ) ≤ 𝑆 )
11 4 5 10 3syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ ( 𝑆 + 1 ) ≤ 𝑆 )
12 1 pclem ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
13 peano2nn0 ⊢ ( 𝑆 ∈ ℕ0 → ( 𝑆 + 1 ) ∈ ℕ0 )
14 oveq2 ⊢ ( 𝑥 = ( 𝑆 + 1 ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( 𝑆 + 1 ) ) )
15 14 breq1d ⊢ ( 𝑥 = ( 𝑆 + 1 ) → ( ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 ↔ ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 ) )
16 oveq2 ⊢ ( 𝑛 = 𝑥 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑥 ) )
17 16 breq1d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 ↔ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 ) )
18 17 cbvrabv ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } = { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 }
19 1 18 eqtri ⊢ 𝐴 = { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 }
20 15 19 elrab2 ⊢ ( ( 𝑆 + 1 ) ∈ 𝐴 ↔ ( ( 𝑆 + 1 ) ∈ ℕ0 ∧ ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 ) )
21 20 simplbi2 ⊢ ( ( 𝑆 + 1 ) ∈ ℕ0 → ( ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 → ( 𝑆 + 1 ) ∈ 𝐴 ) )
22 4 13 21 3syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 → ( 𝑆 + 1 ) ∈ 𝐴 ) )
23 suprzub ⊢ ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ( 𝑆 + 1 ) ∈ 𝐴 ) → ( 𝑆 + 1 ) ≤ sup ( 𝐴 , ℝ , < ) )
24 23 2 breqtrrdi ⊢ ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ( 𝑆 + 1 ) ∈ 𝐴 ) → ( 𝑆 + 1 ) ≤ 𝑆 )
25 24 3expia ⊢ ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ( ( 𝑆 + 1 ) ∈ 𝐴 → ( 𝑆 + 1 ) ≤ 𝑆 ) )
26 25 3adant2 ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ( ( 𝑆 + 1 ) ∈ 𝐴 → ( 𝑆 + 1 ) ≤ 𝑆 ) )
27 12 22 26 sylsyld ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 → ( 𝑆 + 1 ) ≤ 𝑆 ) )
28 11 27 mtod ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ ( 𝑃 ↑ ( 𝑆 + 1 ) ) ∥ 𝑁 )