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 ( 𝑛 ≤ 𝑁 ∧ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) ) )