Metamath Proof Explorer

Theorem pcmptdvds

Description: The partial products of the prime power map form a divisibility chain. (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Hypotheses pcmpt.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ n A 1
pcmpt.2 ⊢ φ → ∀ n ∈ ℙ A ∈ ℕ 0
pcmpt.3 ⊢ φ → N ∈ ℕ
pcmptdvds.3 ⊢ φ → M ∈ ℤ ≥ N
Assertion pcmptdvds ⊢ φ → seq 1 × F ⁡ N ∥ seq 1 × F ⁡ M

Proof

Step Hyp Ref Expression
1 pcmpt.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ n A 1
2 pcmpt.2 ⊢ φ → ∀ n ∈ ℙ A ∈ ℕ 0
3 pcmpt.3 ⊢ φ → N ∈ ℕ
4 pcmptdvds.3 ⊢ φ → M ∈ ℤ ≥ N
5 nfv ⊢ Ⅎ m A ∈ ℕ 0
6 nfcsb1v ⊢ Ⅎ _ n ⦋ m / n⦌ A
7 6 nfel1 ⊢ Ⅎ n ⦋ m / n⦌ A ∈ ℕ 0
8 csbeq1a ⊢ n = m → A = ⦋ m / n⦌ A
9 8 eleq1d ⊢ n = m → A ∈ ℕ 0 ↔ ⦋ m / n⦌ A ∈ ℕ 0
10 5 7 9 cbvralw ⊢ ∀ n ∈ ℙ A ∈ ℕ 0 ↔ ∀ m ∈ ℙ ⦋ m / n⦌ A ∈ ℕ 0
11 2 10 sylib ⊢ φ → ∀ m ∈ ℙ ⦋ m / n⦌ A ∈ ℕ 0
12 csbeq1 ⊢ m = p → ⦋ m / n⦌ A = ⦋ p / n⦌ A
13 12 eleq1d ⊢ m = p → ⦋ m / n⦌ A ∈ ℕ 0 ↔ ⦋ p / n⦌ A ∈ ℕ 0
14 13 rspcv ⊢ p ∈ ℙ → ∀ m ∈ ℙ ⦋ m / n⦌ A ∈ ℕ 0 → ⦋ p / n⦌ A ∈ ℕ 0
15 11 14 mpan9 ⊢ φ ∧ p ∈ ℙ → ⦋ p / n⦌ A ∈ ℕ 0
16 15 nn0ge0d ⊢ φ ∧ p ∈ ℙ → 0 ≤ ⦋ p / n⦌ A
17 0le0 ⊢ 0 ≤ 0
18 breq2 ⊢ ⦋ p / n⦌ A = if p ≤ M ∧ ¬ p ≤ N ⦋ p / n⦌ A 0 → 0 ≤ ⦋ p / n⦌ A ↔ 0 ≤ if p ≤ M ∧ ¬ p ≤ N ⦋ p / n⦌ A 0
19 breq2 ⊢ 0 = if p ≤ M ∧ ¬ p ≤ N ⦋ p / n⦌ A 0 → 0 ≤ 0 ↔ 0 ≤ if p ≤ M ∧ ¬ p ≤ N ⦋ p / n⦌ A 0
20 18 19 ifboth ⊢ 0 ≤ ⦋ p / n⦌ A ∧ 0 ≤ 0 → 0 ≤ if p ≤ M ∧ ¬ p ≤ N ⦋ p / n⦌ A 0
21 16 17 20 sylancl ⊢ φ ∧ p ∈ ℙ → 0 ≤ if p ≤ M ∧ ¬ p ≤ N ⦋ p / n⦌ A 0
22 nfcv ⊢ Ⅎ _ m if n ∈ ℙ n A 1
23 nfv ⊢ Ⅎ n m ∈ ℙ
24 nfcv ⊢ Ⅎ _ n m
25 nfcv ⊢ Ⅎ _ n ^
26 24 25 6 nfov ⊢ Ⅎ _ n m ⦋ m / n⦌ A
27 nfcv ⊢ Ⅎ _ n 1
28 23 26 27 nfif ⊢ Ⅎ _ n if m ∈ ℙ m ⦋ m / n⦌ A 1
29 eleq1w ⊢ n = m → n ∈ ℙ ↔ m ∈ ℙ
30 id ⊢ n = m → n = m
31 30 8 oveq12d ⊢ n = m → n A = m ⦋ m / n⦌ A
32 29 31 ifbieq1d ⊢ n = m → if n ∈ ℙ n A 1 = if m ∈ ℙ m ⦋ m / n⦌ A 1
33 22 28 32 cbvmpt ⊢ n ∈ ℕ ⟼ if n ∈ ℙ n A 1 = m ∈ ℕ ⟼ if m ∈ ℙ m ⦋ m / n⦌ A 1
34 1 33 eqtri ⊢ F = m ∈ ℕ ⟼ if m ∈ ℙ m ⦋ m / n⦌ A 1
35 11 adantr ⊢ φ ∧ p ∈ ℙ → ∀ m ∈ ℙ ⦋ m / n⦌ A ∈ ℕ 0
36 3 adantr ⊢ φ ∧ p ∈ ℙ → N ∈ ℕ
37 simpr ⊢ φ ∧ p ∈ ℙ → p ∈ ℙ
38 4 adantr ⊢ φ ∧ p ∈ ℙ → M ∈ ℤ ≥ N
39 34 35 36 37 12 38 pcmpt2 ⊢ φ ∧ p ∈ ℙ → p pCnt seq 1 × F ⁡ M seq 1 × F ⁡ N = if p ≤ M ∧ ¬ p ≤ N ⦋ p / n⦌ A 0
40 21 39 breqtrrd ⊢ φ ∧ p ∈ ℙ → 0 ≤ p pCnt seq 1 × F ⁡ M seq 1 × F ⁡ N
41 40 ralrimiva ⊢ φ → ∀ p ∈ ℙ 0 ≤ p pCnt seq 1 × F ⁡ M seq 1 × F ⁡ N
42 1 2 pcmptcl ⊢ φ → F : ℕ ⟶ ℕ ∧ seq 1 × F : ℕ ⟶ ℕ
43 42 simprd ⊢ φ → seq 1 × F : ℕ ⟶ ℕ
44 eluznn ⊢ N ∈ ℕ ∧ M ∈ ℤ ≥ N → M ∈ ℕ
45 3 4 44 syl2anc ⊢ φ → M ∈ ℕ
46 43 45 ffvelrnd ⊢ φ → seq 1 × F ⁡ M ∈ ℕ
47 46 nnzd ⊢ φ → seq 1 × F ⁡ M ∈ ℤ
48 43 3 ffvelrnd ⊢ φ → seq 1 × F ⁡ N ∈ ℕ
49 znq ⊢ seq 1 × F ⁡ M ∈ ℤ ∧ seq 1 × F ⁡ N ∈ ℕ → seq 1 × F ⁡ M seq 1 × F ⁡ N ∈ ℚ
50 47 48 49 syl2anc ⊢ φ → seq 1 × F ⁡ M seq 1 × F ⁡ N ∈ ℚ
51 pcz ⊢ seq 1 × F ⁡ M seq 1 × F ⁡ N ∈ ℚ → seq 1 × F ⁡ M seq 1 × F ⁡ N ∈ ℤ ↔ ∀ p ∈ ℙ 0 ≤ p pCnt seq 1 × F ⁡ M seq 1 × F ⁡ N
52 50 51 syl ⊢ φ → seq 1 × F ⁡ M seq 1 × F ⁡ N ∈ ℤ ↔ ∀ p ∈ ℙ 0 ≤ p pCnt seq 1 × F ⁡ M seq 1 × F ⁡ N
53 41 52 mpbird ⊢ φ → seq 1 × F ⁡ M seq 1 × F ⁡ N ∈ ℤ
54 48 nnzd ⊢ φ → seq 1 × F ⁡ N ∈ ℤ
55 48 nnne0d ⊢ φ → seq 1 × F ⁡ N ≠ 0
56 dvdsval2 ⊢ seq 1 × F ⁡ N ∈ ℤ ∧ seq 1 × F ⁡ N ≠ 0 ∧ seq 1 × F ⁡ M ∈ ℤ → seq 1 × F ⁡ N ∥ seq 1 × F ⁡ M ↔ seq 1 × F ⁡ M seq 1 × F ⁡ N ∈ ℤ
57 54 55 47 56 syl3anc ⊢ φ → seq 1 × F ⁡ N ∥ seq 1 × F ⁡ M ↔ seq 1 × F ⁡ M seq 1 × F ⁡ N ∈ ℤ
58 53 57 mpbird ⊢ φ → seq 1 × F ⁡ N ∥ seq 1 × F ⁡ M