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	ffvelcdmd	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ )
47	46	nnzd	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℤ )
48	43 3	ffvelcdmd	⊢ ( 𝜑 → ( 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 ( · , 𝐹 ) ‘ 𝑀 ) )