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

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 ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ0 ( 𝑛 ≤ 𝑁 ∧ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) ) )

Proof

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