pcprendvds2

Description: Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Hypotheses	pclem.1	$⊢ A = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
	pclem.2	$⊢ S = sup (A ℝ <)$
Assertion	pcprendvds2	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{N}{P^{S}})$

Proof

Step	Hyp	Ref	Expression
1		pclem.1	$⊢ A = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
2		pclem.2	$⊢ S = sup (A ℝ <)$
3	1 2	pcprendvds	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \neg P^{S + 1} ∥ N$
4		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
5	4	adantr	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P \in ℕ$
6	5	nnzd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P \in ℤ$
7	1 2	pcprecl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (S \in ℕ_{0} \land P^{S} ∥ N)$
8	7	simprd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{S} ∥ N$
9	7	simpld	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to S \in ℕ_{0}$
10	5 9	nnexpcld	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℕ$
11	10	nnzd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℤ$
12	10	nnne0d	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{S} \neq 0$
13		simprl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to N \in ℤ$
14		dvdsval2	$⊢ (P^{S} \in ℤ \land P^{S} \neq 0 \land N \in ℤ) \to (P^{S} ∥ N \leftrightarrow \frac{N}{P^{S}} \in ℤ)$
15	11 12 13 14	syl3anc	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (P^{S} ∥ N \leftrightarrow \frac{N}{P^{S}} \in ℤ)$
16	8 15	mpbid	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \frac{N}{P^{S}} \in ℤ$
17		dvdscmul	$⊢ (P \in ℤ \land \frac{N}{P^{S}} \in ℤ \land P^{S} \in ℤ) \to (P ∥ (\frac{N}{P^{S}}) \to P^{S} P ∥ P^{S} (\frac{N}{P^{S}}))$
18	6 16 11 17	syl3anc	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (P ∥ (\frac{N}{P^{S}}) \to P^{S} P ∥ P^{S} (\frac{N}{P^{S}}))$
19	5	nncnd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P \in ℂ$
20	19 9	expp1d	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{S + 1} = P^{S} P$
21	20	eqcomd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{S} P = P^{S + 1}$
22		zcn	$⊢ N \in ℤ \to N \in ℂ$
23	22	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to N \in ℂ$
24	10	nncnd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℂ$
25	23 24 12	divcan2d	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{S} (\frac{N}{P^{S}}) = N$
26	21 25	breq12d	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (P^{S} P ∥ P^{S} (\frac{N}{P^{S}}) \leftrightarrow P^{S + 1} ∥ N)$
27	18 26	sylibd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (P ∥ (\frac{N}{P^{S}}) \to P^{S + 1} ∥ N)$
28	3 27	mtod	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{N}{P^{S}})$

Metamath Proof Explorer

Theorem pcprendvds2

Proof