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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) )
pcmpt.2 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ 𝐴 ∈ ℕ0 )
pcmpt.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
pcmptdvds.3 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
Assertion pcmptdvds ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ∥ ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) )

Proof

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