Theorem dvdsppwf1o

Description: A bijection from the divisors of a prime power to the integers less than the prime count. (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Hypothesis	dvdsppwf1o.f	⊢ 𝐹 = ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑛 ) )
Assertion	dvdsppwf1o	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝐹 : ( 0 ... 𝐴 ) –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } )

Proof

Step	Hyp	Ref	Expression
1		dvdsppwf1o.f	⊢ 𝐹 = ( 𝑛 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑛 ) )
2		breq1	⊢ ( 𝑥 = ( 𝑃 ↑ 𝑛 ) → ( 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) ↔ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑃 ↑ 𝐴 ) ) )
3		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
4	3	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝑃 ∈ ℕ )
5		elfznn0	⊢ ( 𝑛 ∈ ( 0 ... 𝐴 ) → 𝑛 ∈ ℕ0 )
6		nnexpcl	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑛 ) ∈ ℕ )
7	4 5 6	syl2an	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝐴 ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℕ )
8		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
9	8	ad2antrr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝐴 ) ) → 𝑃 ∈ ℤ )
10	5	adantl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝐴 ) ) → 𝑛 ∈ ℕ0 )
11		elfzuz3	⊢ ( 𝑛 ∈ ( 0 ... 𝐴 ) → 𝐴 ∈ ( ℤ≥ ‘ 𝑛 ) )
12	11	adantl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 𝑛 ) )
13		dvdsexp	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑃 ↑ 𝐴 ) )
14	9 10 12 13	syl3anc	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝐴 ) ) → ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑃 ↑ 𝐴 ) )
15	2 7 14	elrabd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝐴 ) ) → ( 𝑃 ↑ 𝑛 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } )
16		simpl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝑃 ∈ ℙ )
17		elrabi	⊢ ( 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } → 𝑚 ∈ ℕ )
18		pccl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑚 ∈ ℕ ) → ( 𝑃 pCnt 𝑚 ) ∈ ℕ0 )
19	16 17 18	syl2an	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑃 pCnt 𝑚 ) ∈ ℕ0 )
20	16	adantr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝑃 ∈ ℙ )
21	17	adantl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝑚 ∈ ℕ )
22	21	nnzd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝑚 ∈ ℤ )
23	8	ad2antrr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝑃 ∈ ℤ )
24		simplr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝐴 ∈ ℕ0 )
25		zexpcl	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∈ ℤ )
26	23 24 25	syl2anc	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑃 ↑ 𝐴 ) ∈ ℤ )
27		breq1	⊢ ( 𝑥 = 𝑚 → ( 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) ↔ 𝑚 ∥ ( 𝑃 ↑ 𝐴 ) ) )
28	27	elrab	⊢ ( 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ∥ ( 𝑃 ↑ 𝐴 ) ) )
29	28	simprbi	⊢ ( 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } → 𝑚 ∥ ( 𝑃 ↑ 𝐴 ) )
30	29	adantl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝑚 ∥ ( 𝑃 ↑ 𝐴 ) )
31		pcdvdstr	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑚 ∈ ℤ ∧ ( 𝑃 ↑ 𝐴 ) ∈ ℤ ∧ 𝑚 ∥ ( 𝑃 ↑ 𝐴 ) ) ) → ( 𝑃 pCnt 𝑚 ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) )
32	20 22 26 30 31	syl13anc	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑃 pCnt 𝑚 ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) )
33		pcidlem	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 )
34	33	adantr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 )
35	32 34	breqtrd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑃 pCnt 𝑚 ) ≤ 𝐴 )
36		fznn0	⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝑃 pCnt 𝑚 ) ∈ ( 0 ... 𝐴 ) ↔ ( ( 𝑃 pCnt 𝑚 ) ∈ ℕ0 ∧ ( 𝑃 pCnt 𝑚 ) ≤ 𝐴 ) ) )
37	24 36	syl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( ( 𝑃 pCnt 𝑚 ) ∈ ( 0 ... 𝐴 ) ↔ ( ( 𝑃 pCnt 𝑚 ) ∈ ℕ0 ∧ ( 𝑃 pCnt 𝑚 ) ≤ 𝐴 ) ) )
38	19 35 37	mpbir2and	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑃 pCnt 𝑚 ) ∈ ( 0 ... 𝐴 ) )
39		oveq2	⊢ ( 𝑛 = 𝐴 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝐴 ) )
40	39	breq2d	⊢ ( 𝑛 = 𝐴 → ( 𝑚 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝑚 ∥ ( 𝑃 ↑ 𝐴 ) ) )
41	40	rspcev	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑚 ∥ ( 𝑃 ↑ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ0 𝑚 ∥ ( 𝑃 ↑ 𝑛 ) )
42	24 30 41	syl2anc	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ∃ 𝑛 ∈ ℕ0 𝑚 ∥ ( 𝑃 ↑ 𝑛 ) )
43		pcprmpw2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝑚 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝑚 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑚 ) ) ) )
44	16 17 43	syl2an	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( ∃ 𝑛 ∈ ℕ0 𝑚 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝑚 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑚 ) ) ) )
45	42 44	mpbid	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝑚 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑚 ) ) )
46	45	adantrl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ( 0 ... 𝐴 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) ) → 𝑚 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑚 ) ) )
47		oveq2	⊢ ( 𝑛 = ( 𝑃 pCnt 𝑚 ) → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ ( 𝑃 pCnt 𝑚 ) ) )
48	47	eqeq2d	⊢ ( 𝑛 = ( 𝑃 pCnt 𝑚 ) → ( 𝑚 = ( 𝑃 ↑ 𝑛 ) ↔ 𝑚 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑚 ) ) ) )
49	46 48	syl5ibrcom	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ( 0 ... 𝐴 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) ) → ( 𝑛 = ( 𝑃 pCnt 𝑚 ) → 𝑚 = ( 𝑃 ↑ 𝑛 ) ) )
50		elfzelz	⊢ ( 𝑛 ∈ ( 0 ... 𝐴 ) → 𝑛 ∈ ℤ )
51		pcid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑛 ) ) = 𝑛 )
52	16 50 51	syl2an	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝐴 ) ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑛 ) ) = 𝑛 )
53	52	eqcomd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝐴 ) ) → 𝑛 = ( 𝑃 pCnt ( 𝑃 ↑ 𝑛 ) ) )
54	53	adantrr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ( 0 ... 𝐴 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) ) → 𝑛 = ( 𝑃 pCnt ( 𝑃 ↑ 𝑛 ) ) )
55		oveq2	⊢ ( 𝑚 = ( 𝑃 ↑ 𝑛 ) → ( 𝑃 pCnt 𝑚 ) = ( 𝑃 pCnt ( 𝑃 ↑ 𝑛 ) ) )
56	55	eqeq2d	⊢ ( 𝑚 = ( 𝑃 ↑ 𝑛 ) → ( 𝑛 = ( 𝑃 pCnt 𝑚 ) ↔ 𝑛 = ( 𝑃 pCnt ( 𝑃 ↑ 𝑛 ) ) ) )
57	54 56	syl5ibrcom	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ( 0 ... 𝐴 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) ) → ( 𝑚 = ( 𝑃 ↑ 𝑛 ) → 𝑛 = ( 𝑃 pCnt 𝑚 ) ) )
58	49 57	impbid	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ( 0 ... 𝐴 ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } ) ) → ( 𝑛 = ( 𝑃 pCnt 𝑚 ) ↔ 𝑚 = ( 𝑃 ↑ 𝑛 ) ) )
59	1 15 38 58	f1o2d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝐹 : ( 0 ... 𝐴 ) –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } )