dvdsppwf1o

Description: A bijection between the divisors of a prime power and the integers less than or equal to the exponent. (Contributed by Mario Carneiro, 5-May-2016)

		Ref	Expression
	Hypothesis	dvdsppwf1o.f	$⊢ F = (n \in (0 \dots A) ⟼ P^{n})$
	Assertion	dvdsppwf1o	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to F : (0 \dots A) \underset{1-1 onto}{⟶} \{x \in ℕ \| x ∥ P^{A}\}$

Proof

Step	Hyp	Ref	Expression
1		dvdsppwf1o.f	$⊢ F = (n \in (0 \dots A) ⟼ P^{n})$
2		breq1	$⊢ x = P^{n} \to (x ∥ P^{A} \leftrightarrow P^{n} ∥ P^{A})$
3		prmnn	$⊢ P \in ℙ \to P \in ℕ$
4	3	adantr	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P \in ℕ$
5		elfznn0	$⊢ n \in (0 \dots A) \to n \in ℕ_{0}$
6		nnexpcl	$⊢ (P \in ℕ \land n \in ℕ_{0}) \to P^{n} \in ℕ$
7	4 5 6	syl2an	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land n \in (0 \dots A)) \to P^{n} \in ℕ$
8		prmz	$⊢ P \in ℙ \to P \in ℤ$
9	8	ad2antrr	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land n \in (0 \dots A)) \to P \in ℤ$
10	5	adantl	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land n \in (0 \dots A)) \to n \in ℕ_{0}$
11		elfzuz3	$⊢ n \in (0 \dots A) \to A \in ℤ_{\geq n}$
12	11	adantl	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land n \in (0 \dots A)) \to A \in ℤ_{\geq n}$
13		dvdsexp	$⊢ (P \in ℤ \land n \in ℕ_{0} \land A \in ℤ_{\geq n}) \to P^{n} ∥ P^{A}$
14	9 10 12 13	syl3anc	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land n \in (0 \dots A)) \to P^{n} ∥ P^{A}$
15	2 7 14	elrabd	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land n \in (0 \dots A)) \to P^{n} \in \{x \in ℕ \| x ∥ P^{A}\}$
16		simpl	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P \in ℙ$
17		elrabi	$⊢ m \in \{x \in ℕ \| x ∥ P^{A}\} \to m \in ℕ$
18		pccl	$⊢ (P \in ℙ \land m \in ℕ) \to P pCnt m \in ℕ_{0}$
19	16 17 18	syl2an	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to P pCnt m \in ℕ_{0}$
20	16	adantr	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to P \in ℙ$
21	17	adantl	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to m \in ℕ$
22	21	nnzd	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to m \in ℤ$
23	8	ad2antrr	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to P \in ℤ$
24		simplr	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to A \in ℕ_{0}$
25		zexpcl	$⊢ (P \in ℤ \land A \in ℕ_{0}) \to P^{A} \in ℤ$
26	23 24 25	syl2anc	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to P^{A} \in ℤ$
27		breq1	$⊢ x = m \to (x ∥ P^{A} \leftrightarrow m ∥ P^{A})$
28	27	elrab	$⊢ m \in \{x \in ℕ \| x ∥ P^{A}\} \leftrightarrow (m \in ℕ \land m ∥ P^{A})$
29	28	simprbi	$⊢ m \in \{x \in ℕ \| x ∥ P^{A}\} \to m ∥ P^{A}$
30	29	adantl	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to m ∥ P^{A}$
31		pcdvdstr	$⊢ (P \in ℙ \land (m \in ℤ \land P^{A} \in ℤ \land m ∥ P^{A})) \to P pCnt m \leq P pCnt P^{A}$
32	20 22 26 30 31	syl13anc	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to P pCnt m \leq P pCnt P^{A}$
33		pcidlem	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} = A$
34	33	adantr	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to P pCnt P^{A} = A$
35	32 34	breqtrd	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to P pCnt m \leq A$
36		fznn0	$⊢ A \in ℕ_{0} \to (P pCnt m \in (0 \dots A) \leftrightarrow (P pCnt m \in ℕ_{0} \land P pCnt m \leq A))$
37	24 36	syl	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to (P pCnt m \in (0 \dots A) \leftrightarrow (P pCnt m \in ℕ_{0} \land P pCnt m \leq A))$
38	19 35 37	mpbir2and	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to P pCnt m \in (0 \dots A)$
39		oveq2	$⊢ n = A \to P^{n} = P^{A}$
40	39	breq2d	$⊢ n = A \to (m ∥ P^{n} \leftrightarrow m ∥ P^{A})$
41	40	rspcev	$⊢ (A \in ℕ_{0} \land m ∥ P^{A}) \to \exists n \in ℕ_{0} m ∥ P^{n}$
42	24 30 41	syl2anc	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to \exists n \in ℕ_{0} m ∥ P^{n}$
43		pcprmpw2	$⊢ (P \in ℙ \land m \in ℕ) \to (\exists n \in ℕ_{0} m ∥ P^{n} \leftrightarrow m = P^{P pCnt m})$
44	16 17 43	syl2an	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to (\exists n \in ℕ_{0} m ∥ P^{n} \leftrightarrow m = P^{P pCnt m})$
45	42 44	mpbid	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land m \in \{x \in ℕ \| x ∥ P^{A}\}) \to m = P^{P pCnt m}$
46	45	adantrl	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land (n \in (0 \dots A) \land m \in \{x \in ℕ \| x ∥ P^{A}\})) \to m = P^{P pCnt m}$
47		oveq2	$⊢ n = P pCnt m \to P^{n} = P^{P pCnt m}$
48	47	eqeq2d	$⊢ n = P pCnt m \to (m = P^{n} \leftrightarrow m = P^{P pCnt m})$
49	46 48	syl5ibrcom	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land (n \in (0 \dots A) \land m \in \{x \in ℕ \| x ∥ P^{A}\})) \to (n = P pCnt m \to m = P^{n})$
50		elfzelz	$⊢ n \in (0 \dots A) \to n \in ℤ$
51		pcid	$⊢ (P \in ℙ \land n \in ℤ) \to P pCnt P^{n} = n$
52	16 50 51	syl2an	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land n \in (0 \dots A)) \to P pCnt P^{n} = n$
53	52	eqcomd	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land n \in (0 \dots A)) \to n = P pCnt P^{n}$
54	53	adantrr	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land (n \in (0 \dots A) \land m \in \{x \in ℕ \| x ∥ P^{A}\})) \to n = P pCnt P^{n}$
55		oveq2	$⊢ m = P^{n} \to P pCnt m = P pCnt P^{n}$
56	55	eqeq2d	$⊢ m = P^{n} \to (n = P pCnt m \leftrightarrow n = P pCnt P^{n})$
57	54 56	syl5ibrcom	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land (n \in (0 \dots A) \land m \in \{x \in ℕ \| x ∥ P^{A}\})) \to (m = P^{n} \to n = P pCnt m)$
58	49 57	impbid	$⊢ ((P \in ℙ \land A \in ℕ_{0}) \land (n \in (0 \dots A) \land m \in \{x \in ℕ \| x ∥ P^{A}\})) \to (n = P pCnt m \leftrightarrow m = P^{n})$
59	1 15 38 58	f1o2d	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to F : (0 \dots A) \underset{1-1 onto}{⟶} \{x \in ℕ \| x ∥ P^{A}\}$

Metamath Proof Explorer

Theorem dvdsppwf1o

Proof