Theorem pcprendvds

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

	Ref	Expression
Hypotheses	pclem.1	$$⊢A=\left\{n\in {\mathbb{N}}_0|P^n\parallel N\right\}$$
	pclem.2	$$⊢S=sup\left(A,ℝ,<\right)$$
Assertion	pcprendvds	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \neg P^{S+1}\parallel N$$

Proof

Step	Hyp	Ref	Expression
1		pclem.1	$$⊢A=\left\{n\in {\mathbb{N}}_0|P^n\parallel N\right\}$$
2		pclem.2	$$⊢S=sup\left(A,ℝ,<\right)$$
3	1 2	pcprecl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \left(S\in {\mathbb{N}}_0\wedge P^S\parallel N\right)$$
4	3	simpld	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to S\in {\mathbb{N}}_0$$
5		nn0re	$$⊢S\in {\mathbb{N}}_0\to S\in ℝ$$
6		ltp1	$$⊢S\in ℝ\to S<S+1$$
7		peano2re	$$⊢S\in ℝ\to S+1\in ℝ$$
8		ltnle	$$⊢\left(S\in ℝ\wedge S+1\in ℝ\right)\to \left(S<S+1\leftrightarrow \neg S+1\le S\right)$$
9	7 8	mpdan	$$⊢S\in ℝ\to \left(S<S+1\leftrightarrow \neg S+1\le S\right)$$
10	6 9	mpbid	$$⊢S\in ℝ\to \neg S+1\le S$$
11	4 5 10	3syl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \neg S+1\le S$$
12	1	pclem	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \left(A\subseteq \mathbb{Z}\wedge A\ne \varnothing \wedge \exists x\in \mathbb{Z}\forall y\in Ay\le x\right)$$
13		peano2nn0	$$⊢S\in {\mathbb{N}}_0\to S+1\in {\mathbb{N}}_0$$
14		oveq2	$$⊢x=S+1\to P^x=P^{S+1}$$
15	14	breq1d	$$⊢x=S+1\to \left(P^x\parallel N\leftrightarrow P^{S+1}\parallel N\right)$$
16		oveq2	$$⊢n=x\to P^n=P^x$$
17	16	breq1d	$$⊢n=x\to \left(P^n\parallel N\leftrightarrow P^x\parallel N\right)$$
18	17	cbvrabv	$$⊢\left\{n\in {\mathbb{N}}_0|P^n\parallel N\right\}=\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\}$$
19	1 18	eqtri	$$⊢A=\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\}$$
20	15 19	elrab2	$$⊢S+1\in A\leftrightarrow \left(S+1\in {\mathbb{N}}_0\wedge P^{S+1}\parallel N\right)$$
21	20	simplbi2	$$⊢S+1\in {\mathbb{N}}_0\to \left(P^{S+1}\parallel N\to S+1\in A\right)$$
22	4 13 21	3syl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \left(P^{S+1}\parallel N\to S+1\in A\right)$$
23		suprzub	$$⊢\left(A\subseteq \mathbb{Z}\wedge \exists x\in \mathbb{Z}\forall y\in Ay\le x\wedge S+1\in A\right)\to S+1\le sup\left(A,ℝ,<\right)$$
24	23 2	breqtrrdi	$$⊢\left(A\subseteq \mathbb{Z}\wedge \exists x\in \mathbb{Z}\forall y\in Ay\le x\wedge S+1\in A\right)\to S+1\le S$$
25	24	3expia	$$⊢\left(A\subseteq \mathbb{Z}\wedge \exists x\in \mathbb{Z}\forall y\in Ay\le x\right)\to \left(S+1\in A\to S+1\le S\right)$$
26	25	3adant2	$$⊢\left(A\subseteq \mathbb{Z}\wedge A\ne \varnothing \wedge \exists x\in \mathbb{Z}\forall y\in Ay\le x\right)\to \left(S+1\in A\to S+1\le S\right)$$
27	12 22 26	sylsyld	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \left(P^{S+1}\parallel N\to S+1\le S\right)$$
28	11 27	mtod	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \neg P^{S+1}\parallel N$$