This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐹 = ( 𝑛 ∈ ( 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→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑃 ↑ 𝐴 ) } )