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	$⊢ (P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \to (A ∥ P^{N} \to \exists n \in ℕ_{0} (n \leq N \land A = P^{n}))$

Proof

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

Metamath Proof Explorer

Theorem dvdsprmpweqle

Proof