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 ⊢ A = n ∈ ℕ 0 | P n ∥ N
pclem.2 ⊢ S = sup A ℝ <
Assertion pcprendvds ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → ¬ P S + 1 ∥ N

Proof

Step Hyp Ref Expression
1 pclem.1 ⊢ A = n ∈ ℕ 0 | P n ∥ N
2 pclem.2 ⊢ S = sup A ℝ <
3 1 2 pcprecl ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → S ∈ ℕ 0 ∧ P S ∥ N
4 3 simpld ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → S ∈ ℕ 0
5 nn0re ⊢ S ∈ ℕ 0 → S ∈ ℝ
6 ltp1 ⊢ S ∈ ℝ → S < S + 1
7 peano2re ⊢ S ∈ ℝ → S + 1 ∈ ℝ
8 ltnle ⊢ S ∈ ℝ ∧ S + 1 ∈ ℝ → S < S + 1 ↔ ¬ S + 1 ≤ S
9 7 8 mpdan ⊢ S ∈ ℝ → S < S + 1 ↔ ¬ S + 1 ≤ S
10 6 9 mpbid ⊢ S ∈ ℝ → ¬ S + 1 ≤ S
11 4 5 10 3syl ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → ¬ S + 1 ≤ S
12 1 pclem ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → A ⊆ ℤ ∧ A ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x
13 peano2nn0 ⊢ S ∈ ℕ 0 → S + 1 ∈ ℕ 0
14 oveq2 ⊢ x = S + 1 → P x = P S + 1
15 14 breq1d ⊢ x = S + 1 → P x ∥ N ↔ P S + 1 ∥ N
16 oveq2 ⊢ n = x → P n = P x
17 16 breq1d ⊢ n = x → P n ∥ N ↔ P x ∥ N
18 17 cbvrabv ⊢ n ∈ ℕ 0 | P n ∥ N = x ∈ ℕ 0 | P x ∥ N
19 1 18 eqtri ⊢ A = x ∈ ℕ 0 | P x ∥ N
20 15 19 elrab2 ⊢ S + 1 ∈ A ↔ S + 1 ∈ ℕ 0 ∧ P S + 1 ∥ N
21 20 simplbi2 ⊢ S + 1 ∈ ℕ 0 → P S + 1 ∥ N → S + 1 ∈ A
22 4 13 21 3syl ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → P S + 1 ∥ N → S + 1 ∈ A
23 suprzub ⊢ A ⊆ ℤ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x ∧ S + 1 ∈ A → S + 1 ≤ sup A ℝ <
24 23 2 breqtrrdi ⊢ A ⊆ ℤ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x ∧ S + 1 ∈ A → S + 1 ≤ S
25 24 3expia ⊢ A ⊆ ℤ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → S + 1 ∈ A → S + 1 ≤ S
26 25 3adant2 ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → S + 1 ∈ A → S + 1 ≤ S
27 12 22 26 sylsyld ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → P S + 1 ∥ N → S + 1 ≤ S
28 11 27 mtod ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → ¬ P S + 1 ∥ N