# Metamath Proof Explorer

## Theorem dvdsprmpweqle

Description: If a positive integer divides a prime power, it is a prime power with a smaller exponent. (Contributed by AV, 25-Jul-2021)

Ref Expression
Assertion dvdsprmpweqle ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({n}\le {N}\wedge {A}={{P}}^{{n}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 dvdsprmpweq ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
2 1 imp ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}$
3 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
4 3 3ad2ant3 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℝ$
5 4 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to {N}\in ℝ$
6 nn0re ${⊢}{n}\in {ℕ}_{0}\to {n}\in ℝ$
7 5 6 anim12ci ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({n}\in ℝ\wedge {N}\in ℝ\right)$
8 7 adantr ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to \left({n}\in ℝ\wedge {N}\in ℝ\right)$
9 lelttric ${⊢}\left({n}\in ℝ\wedge {N}\in ℝ\right)\to \left({n}\le {N}\vee {N}<{n}\right)$
10 8 9 syl ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to \left({n}\le {N}\vee {N}<{n}\right)$
11 breq1 ${⊢}{A}={{P}}^{{n}}\to \left({A}\parallel {{P}}^{{N}}↔{{P}}^{{n}}\parallel {{P}}^{{N}}\right)$
12 11 adantl ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to \left({A}\parallel {{P}}^{{N}}↔{{P}}^{{n}}\parallel {{P}}^{{N}}\right)$
13 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
14 13 nnnn0d ${⊢}{P}\in ℙ\to {P}\in {ℕ}_{0}$
15 14 3ad2ant1 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {P}\in {ℕ}_{0}$
16 15 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {P}\in {ℕ}_{0}$
17 simpr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {n}\in {ℕ}_{0}$
18 16 17 nn0expcld ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {{P}}^{{n}}\in {ℕ}_{0}$
19 18 nn0zd ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {{P}}^{{n}}\in ℤ$
20 13 nncnd ${⊢}{P}\in ℙ\to {P}\in ℂ$
21 20 3ad2ant1 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {P}\in ℂ$
22 21 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {P}\in ℂ$
23 13 nnne0d ${⊢}{P}\in ℙ\to {P}\ne 0$
24 23 3ad2ant1 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {P}\ne 0$
25 24 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {P}\ne 0$
26 nn0z ${⊢}{n}\in {ℕ}_{0}\to {n}\in ℤ$
27 26 adantl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {n}\in ℤ$
28 22 25 27 expne0d ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {{P}}^{{n}}\ne 0$
29 simp3 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in {ℕ}_{0}$
30 29 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {N}\in {ℕ}_{0}$
31 16 30 nn0expcld ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {{P}}^{{N}}\in {ℕ}_{0}$
32 31 nn0zd ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {{P}}^{{N}}\in ℤ$
33 dvdsval2 ${⊢}\left({{P}}^{{n}}\in ℤ\wedge {{P}}^{{n}}\ne 0\wedge {{P}}^{{N}}\in ℤ\right)\to \left({{P}}^{{n}}\parallel {{P}}^{{N}}↔\frac{{{P}}^{{N}}}{{{P}}^{{n}}}\in ℤ\right)$
34 19 28 32 33 syl3anc ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({{P}}^{{n}}\parallel {{P}}^{{N}}↔\frac{{{P}}^{{N}}}{{{P}}^{{n}}}\in ℤ\right)$
35 20 23 jca ${⊢}{P}\in ℙ\to \left({P}\in ℂ\wedge {P}\ne 0\right)$
36 35 3ad2ant1 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to \left({P}\in ℂ\wedge {P}\ne 0\right)$
37 nn0z ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℤ$
38 37 3ad2ant3 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℤ$
39 38 26 anim12i ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({N}\in ℤ\wedge {n}\in ℤ\right)$
40 expsub ${⊢}\left(\left({P}\in ℂ\wedge {P}\ne 0\right)\wedge \left({N}\in ℤ\wedge {n}\in ℤ\right)\right)\to {{P}}^{{N}-{n}}=\frac{{{P}}^{{N}}}{{{P}}^{{n}}}$
41 40 eqcomd ${⊢}\left(\left({P}\in ℂ\wedge {P}\ne 0\right)\wedge \left({N}\in ℤ\wedge {n}\in ℤ\right)\right)\to \frac{{{P}}^{{N}}}{{{P}}^{{n}}}={{P}}^{{N}-{n}}$
42 36 39 41 syl2an2r ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \frac{{{P}}^{{N}}}{{{P}}^{{n}}}={{P}}^{{N}-{n}}$
43 42 eleq1d ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left(\frac{{{P}}^{{N}}}{{{P}}^{{n}}}\in ℤ↔{{P}}^{{N}-{n}}\in ℤ\right)$
44 22 adantr ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to {P}\in ℂ$
45 nn0cn ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℂ$
46 45 3ad2ant3 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℂ$
47 46 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {N}\in ℂ$
48 nn0cn ${⊢}{n}\in {ℕ}_{0}\to {n}\in ℂ$
49 48 adantl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {n}\in ℂ$
50 47 49 subcld ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {N}-{n}\in ℂ$
51 50 adantr ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to {N}-{n}\in ℂ$
52 46 48 anim12i ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({N}\in ℂ\wedge {n}\in ℂ\right)$
53 52 adantr ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to \left({N}\in ℂ\wedge {n}\in ℂ\right)$
54 negsubdi2 ${⊢}\left({N}\in ℂ\wedge {n}\in ℂ\right)\to -\left({N}-{n}\right)={n}-{N}$
55 53 54 syl ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to -\left({N}-{n}\right)={n}-{N}$
56 29 anim1ci ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)$
57 ltsubnn0 ${⊢}\left({n}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({N}<{n}\to {n}-{N}\in {ℕ}_{0}\right)$
58 56 57 syl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({N}<{n}\to {n}-{N}\in {ℕ}_{0}\right)$
59 58 imp ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to {n}-{N}\in {ℕ}_{0}$
60 55 59 eqeltrd ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to -\left({N}-{n}\right)\in {ℕ}_{0}$
61 expneg2 ${⊢}\left({P}\in ℂ\wedge {N}-{n}\in ℂ\wedge -\left({N}-{n}\right)\in {ℕ}_{0}\right)\to {{P}}^{{N}-{n}}=\frac{1}{{{P}}^{-\left({N}-{n}\right)}}$
62 44 51 60 61 syl3anc ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to {{P}}^{{N}-{n}}=\frac{1}{{{P}}^{-\left({N}-{n}\right)}}$
63 62 eleq1d ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to \left({{P}}^{{N}-{n}}\in ℤ↔\frac{1}{{{P}}^{-\left({N}-{n}\right)}}\in ℤ\right)$
64 13 nnred ${⊢}{P}\in ℙ\to {P}\in ℝ$
65 64 3ad2ant1 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {P}\in ℝ$
66 65 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to {P}\in ℝ$
67 66 adantr ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to {P}\in ℝ$
68 67 59 reexpcld ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to {{P}}^{{n}-{N}}\in ℝ$
69 znnsub ${⊢}\left({N}\in ℤ\wedge {n}\in ℤ\right)\to \left({N}<{n}↔{n}-{N}\in ℕ\right)$
70 39 69 syl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({N}<{n}↔{n}-{N}\in ℕ\right)$
71 70 biimpa ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to {n}-{N}\in ℕ$
72 prmgt1 ${⊢}{P}\in ℙ\to 1<{P}$
73 72 3ad2ant1 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to 1<{P}$
74 73 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to 1<{P}$
75 74 adantr ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to 1<{P}$
76 expgt1 ${⊢}\left({P}\in ℝ\wedge {n}-{N}\in ℕ\wedge 1<{P}\right)\to 1<{{P}}^{{n}-{N}}$
77 67 71 75 76 syl3anc ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to 1<{{P}}^{{n}-{N}}$
78 68 77 jca ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to \left({{P}}^{{n}-{N}}\in ℝ\wedge 1<{{P}}^{{n}-{N}}\right)$
79 oveq2 ${⊢}-\left({N}-{n}\right)={n}-{N}\to {{P}}^{-\left({N}-{n}\right)}={{P}}^{{n}-{N}}$
80 79 eleq1d ${⊢}-\left({N}-{n}\right)={n}-{N}\to \left({{P}}^{-\left({N}-{n}\right)}\in ℝ↔{{P}}^{{n}-{N}}\in ℝ\right)$
81 79 breq2d ${⊢}-\left({N}-{n}\right)={n}-{N}\to \left(1<{{P}}^{-\left({N}-{n}\right)}↔1<{{P}}^{{n}-{N}}\right)$
82 80 81 anbi12d ${⊢}-\left({N}-{n}\right)={n}-{N}\to \left(\left({{P}}^{-\left({N}-{n}\right)}\in ℝ\wedge 1<{{P}}^{-\left({N}-{n}\right)}\right)↔\left({{P}}^{{n}-{N}}\in ℝ\wedge 1<{{P}}^{{n}-{N}}\right)\right)$
83 78 82 syl5ibrcom ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to \left(-\left({N}-{n}\right)={n}-{N}\to \left({{P}}^{-\left({N}-{n}\right)}\in ℝ\wedge 1<{{P}}^{-\left({N}-{n}\right)}\right)\right)$
84 55 83 mpd ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to \left({{P}}^{-\left({N}-{n}\right)}\in ℝ\wedge 1<{{P}}^{-\left({N}-{n}\right)}\right)$
85 recnz ${⊢}\left({{P}}^{-\left({N}-{n}\right)}\in ℝ\wedge 1<{{P}}^{-\left({N}-{n}\right)}\right)\to ¬\frac{1}{{{P}}^{-\left({N}-{n}\right)}}\in ℤ$
86 84 85 syl ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to ¬\frac{1}{{{P}}^{-\left({N}-{n}\right)}}\in ℤ$
87 86 pm2.21d ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to \left(\frac{1}{{{P}}^{-\left({N}-{n}\right)}}\in ℤ\to {n}\le {N}\right)$
88 63 87 sylbid ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {N}<{n}\right)\to \left({{P}}^{{N}-{n}}\in ℤ\to {n}\le {N}\right)$
89 88 ex ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({N}<{n}\to \left({{P}}^{{N}-{n}}\in ℤ\to {n}\le {N}\right)\right)$
90 89 com23 ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({{P}}^{{N}-{n}}\in ℤ\to \left({N}<{n}\to {n}\le {N}\right)\right)$
91 43 90 sylbid ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left(\frac{{{P}}^{{N}}}{{{P}}^{{n}}}\in ℤ\to \left({N}<{n}\to {n}\le {N}\right)\right)$
92 34 91 sylbid ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({{P}}^{{n}}\parallel {{P}}^{{N}}\to \left({N}<{n}\to {n}\le {N}\right)\right)$
93 92 adantr ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to \left({{P}}^{{n}}\parallel {{P}}^{{N}}\to \left({N}<{n}\to {n}\le {N}\right)\right)$
94 12 93 sylbid ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to \left({A}\parallel {{P}}^{{N}}\to \left({N}<{n}\to {n}\le {N}\right)\right)$
95 94 ex ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({A}={{P}}^{{n}}\to \left({A}\parallel {{P}}^{{N}}\to \left({N}<{n}\to {n}\le {N}\right)\right)\right)$
96 95 com23 ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \left({A}={{P}}^{{n}}\to \left({N}<{n}\to {n}\le {N}\right)\right)\right)$
97 96 ex ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}\to \left({A}\parallel {{P}}^{{N}}\to \left({A}={{P}}^{{n}}\to \left({N}<{n}\to {n}\le {N}\right)\right)\right)\right)$
98 97 com23 ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \left({n}\in {ℕ}_{0}\to \left({A}={{P}}^{{n}}\to \left({N}<{n}\to {n}\le {N}\right)\right)\right)\right)$
99 98 imp41 ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to \left({N}<{n}\to {n}\le {N}\right)$
100 99 com12 ${⊢}{N}<{n}\to \left(\left(\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to {n}\le {N}\right)$
101 100 jao1i ${⊢}\left({n}\le {N}\vee {N}<{n}\right)\to \left(\left(\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to {n}\le {N}\right)$
102 10 101 mpcom ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to {n}\le {N}$
103 simpr ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to {A}={{P}}^{{n}}$
104 102 103 jca ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {A}={{P}}^{{n}}\right)\to \left({n}\le {N}\wedge {A}={{P}}^{{n}}\right)$
105 104 ex ${⊢}\left(\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({A}={{P}}^{{n}}\to \left({n}\le {N}\wedge {A}={{P}}^{{n}}\right)\right)$
106 105 reximdva ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({n}\le {N}\wedge {A}={{P}}^{{n}}\right)\right)$
107 2 106 mpd ${⊢}\left(\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({n}\le {N}\wedge {A}={{P}}^{{n}}\right)$
108 107 ex ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({n}\le {N}\wedge {A}={{P}}^{{n}}\right)\right)$