Theorem prmfac1

Description: The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014)

	Ref	Expression
Assertion	prmfac1	$$⊢\left(N\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\wedge P\parallel N!\right)\to P\le N$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢x=0\to x!=0!$$
2	1	breq2d	$$⊢x=0\to \left(P\parallel x!\leftrightarrow P\parallel 0!\right)$$
3		breq2	$$⊢x=0\to \left(P\le x\leftrightarrow P\le 0\right)$$
4	2 3	imbi12d	$$⊢x=0\to \left(\left(P\parallel x!\to P\le x\right)\leftrightarrow \left(P\parallel 0!\to P\le 0\right)\right)$$
5	4	imbi2d	$$⊢x=0\to \left(\left(P\in \mathbb{P}\to \left(P\parallel x!\to P\le x\right)\right)\leftrightarrow \left(P\in \mathbb{P}\to \left(P\parallel 0!\to P\le 0\right)\right)\right)$$
6		fveq2	$$⊢x=k\to x!=k!$$
7	6	breq2d	$$⊢x=k\to \left(P\parallel x!\leftrightarrow P\parallel k!\right)$$
8		breq2	$$⊢x=k\to \left(P\le x\leftrightarrow P\le k\right)$$
9	7 8	imbi12d	$$⊢x=k\to \left(\left(P\parallel x!\to P\le x\right)\leftrightarrow \left(P\parallel k!\to P\le k\right)\right)$$
10	9	imbi2d	$$⊢x=k\to \left(\left(P\in \mathbb{P}\to \left(P\parallel x!\to P\le x\right)\right)\leftrightarrow \left(P\in \mathbb{P}\to \left(P\parallel k!\to P\le k\right)\right)\right)$$
11		fveq2	$$⊢x=k+1\to x!=\left(k+1\right)!$$
12	11	breq2d	$$⊢x=k+1\to \left(P\parallel x!\leftrightarrow P\parallel \left(k+1\right)!\right)$$
13		breq2	$$⊢x=k+1\to \left(P\le x\leftrightarrow P\le k+1\right)$$
14	12 13	imbi12d	$$⊢x=k+1\to \left(\left(P\parallel x!\to P\le x\right)\leftrightarrow \left(P\parallel \left(k+1\right)!\to P\le k+1\right)\right)$$
15	14	imbi2d	$$⊢x=k+1\to \left(\left(P\in \mathbb{P}\to \left(P\parallel x!\to P\le x\right)\right)\leftrightarrow \left(P\in \mathbb{P}\to \left(P\parallel \left(k+1\right)!\to P\le k+1\right)\right)\right)$$
16		fveq2	$$⊢x=N\to x!=N!$$
17	16	breq2d	$$⊢x=N\to \left(P\parallel x!\leftrightarrow P\parallel N!\right)$$
18		breq2	$$⊢x=N\to \left(P\le x\leftrightarrow P\le N\right)$$
19	17 18	imbi12d	$$⊢x=N\to \left(\left(P\parallel x!\to P\le x\right)\leftrightarrow \left(P\parallel N!\to P\le N\right)\right)$$
20	19	imbi2d	$$⊢x=N\to \left(\left(P\in \mathbb{P}\to \left(P\parallel x!\to P\le x\right)\right)\leftrightarrow \left(P\in \mathbb{P}\to \left(P\parallel N!\to P\le N\right)\right)\right)$$
21		fac0	$$⊢0!=1$$
22	21	breq2i	$$⊢P\parallel 0!\leftrightarrow P\parallel 1$$
23		nprmdvds1	$$⊢P\in \mathbb{P}\to \neg P\parallel 1$$
24	23	pm2.21d	$$⊢P\in \mathbb{P}\to \left(P\parallel 1\to P\le 0\right)$$
25	22 24	biimtrid	$$⊢P\in \mathbb{P}\to \left(P\parallel 0!\to P\le 0\right)$$
26		facp1	$$⊢k\in {\mathbb{N}}_0\to \left(k+1\right)!=k!\left(k+1\right)$$
27	26	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(k+1\right)!=k!\left(k+1\right)$$
28	27	breq2d	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(P\parallel \left(k+1\right)!\leftrightarrow P\parallel k!\left(k+1\right)\right)$$
29		simpr	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to P\in \mathbb{P}$$
30		faccl	$$⊢k\in {\mathbb{N}}_0\to k!\in \mathbb{N}$$
31	30	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to k!\in \mathbb{N}$$
32	31	nnzd	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to k!\in \mathbb{Z}$$
33		nn0p1nn	$$⊢k\in {\mathbb{N}}_0\to k+1\in \mathbb{N}$$
34	33	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to k+1\in \mathbb{N}$$
35	34	nnzd	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to k+1\in \mathbb{Z}$$
36		euclemma	$$⊢\left(P\in \mathbb{P}\wedge k!\in \mathbb{Z}\wedge k+1\in \mathbb{Z}\right)\to \left(P\parallel k!\left(k+1\right)\leftrightarrow \left(P\parallel k!\vee P\parallel \left(k+1\right)\right)\right)$$
37	29 32 35 36	syl3anc	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(P\parallel k!\left(k+1\right)\leftrightarrow \left(P\parallel k!\vee P\parallel \left(k+1\right)\right)\right)$$
38	28 37	bitrd	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(P\parallel \left(k+1\right)!\leftrightarrow \left(P\parallel k!\vee P\parallel \left(k+1\right)\right)\right)$$
39		nn0re	$$⊢k\in {\mathbb{N}}_0\to k\in ℝ$$
40	39	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to k\in ℝ$$
41	40	lep1d	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to k\le k+1$$
42		prmz	$$⊢P\in \mathbb{P}\to P\in \mathbb{Z}$$
43	42	adantl	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to P\in \mathbb{Z}$$
44	43	zred	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to P\in ℝ$$
45	34	nnred	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to k+1\in ℝ$$
46		letr	$$⊢\left(P\in ℝ\wedge k\in ℝ\wedge k+1\in ℝ\right)\to \left(\left(P\le k\wedge k\le k+1\right)\to P\le k+1\right)$$
47	44 40 45 46	syl3anc	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(\left(P\le k\wedge k\le k+1\right)\to P\le k+1\right)$$
48	41 47	mpan2d	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(P\le k\to P\le k+1\right)$$
49	48	imim2d	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(\left(P\parallel k!\to P\le k\right)\to \left(P\parallel k!\to P\le k+1\right)\right)$$
50	49	com23	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(P\parallel k!\to \left(\left(P\parallel k!\to P\le k\right)\to P\le k+1\right)\right)$$
51		dvdsle	$$⊢\left(P\in \mathbb{Z}\wedge k+1\in \mathbb{N}\right)\to \left(P\parallel \left(k+1\right)\to P\le k+1\right)$$
52	43 34 51	syl2anc	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(P\parallel \left(k+1\right)\to P\le k+1\right)$$
53	52	a1dd	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(P\parallel \left(k+1\right)\to \left(\left(P\parallel k!\to P\le k\right)\to P\le k+1\right)\right)$$
54	50 53	jaod	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(\left(P\parallel k!\vee P\parallel \left(k+1\right)\right)\to \left(\left(P\parallel k!\to P\le k\right)\to P\le k+1\right)\right)$$
55	38 54	sylbid	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(P\parallel \left(k+1\right)!\to \left(\left(P\parallel k!\to P\le k\right)\to P\le k+1\right)\right)$$
56	55	com23	$$⊢\left(k\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\right)\to \left(\left(P\parallel k!\to P\le k\right)\to \left(P\parallel \left(k+1\right)!\to P\le k+1\right)\right)$$
57	56	ex	$$⊢k\in {\mathbb{N}}_0\to \left(P\in \mathbb{P}\to \left(\left(P\parallel k!\to P\le k\right)\to \left(P\parallel \left(k+1\right)!\to P\le k+1\right)\right)\right)$$
58	57	a2d	$$⊢k\in {\mathbb{N}}_0\to \left(\left(P\in \mathbb{P}\to \left(P\parallel k!\to P\le k\right)\right)\to \left(P\in \mathbb{P}\to \left(P\parallel \left(k+1\right)!\to P\le k+1\right)\right)\right)$$
59	5 10 15 20 25 58	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(P\in \mathbb{P}\to \left(P\parallel N!\to P\le N\right)\right)$$
60	59	3imp	$$⊢\left(N\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\wedge P\parallel N!\right)\to P\le N$$