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 \in ℕ ⟼ if (n \in ℙ, n^{A}, 1))$
	pcmpt.2	$⊢ φ \to \forall n \in ℙ A \in ℕ_{0}$
	pcmpt.3	$⊢ φ \to N \in ℕ$
	pcmptdvds.3	$⊢ φ \to M \in ℤ_{\geq N}$
Assertion	pcmptdvds	$⊢ φ \to seq 1 (\times F) (N) ∥ seq 1 (\times F) (M)$

Proof

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

Metamath Proof Explorer

Theorem pcmptdvds

Proof