Theorem facwordi

Description: Ordering property of factorial. (Contributed by NM, 9-Dec-2005)

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

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢j=0\to \left(M\le j\leftrightarrow M\le 0\right)$$
2	1	anbi2d	$$⊢j=0\to \left(\left(M\in {\mathbb{N}}_0\wedge M\le j\right)\leftrightarrow \left(M\in {\mathbb{N}}_0\wedge M\le 0\right)\right)$$
3		fveq2	$$⊢j=0\to j!=0!$$
4	3	breq2d	$$⊢j=0\to \left(M!\le j!\leftrightarrow M!\le 0!\right)$$
5	2 4	imbi12d	$$⊢j=0\to \left(\left(\left(M\in {\mathbb{N}}_0\wedge M\le j\right)\to M!\le j!\right)\leftrightarrow \left(\left(M\in {\mathbb{N}}_0\wedge M\le 0\right)\to M!\le 0!\right)\right)$$
6		breq2	$$⊢j=k\to \left(M\le j\leftrightarrow M\le k\right)$$
7	6	anbi2d	$$⊢j=k\to \left(\left(M\in {\mathbb{N}}_0\wedge M\le j\right)\leftrightarrow \left(M\in {\mathbb{N}}_0\wedge M\le k\right)\right)$$
8		fveq2	$$⊢j=k\to j!=k!$$
9	8	breq2d	$$⊢j=k\to \left(M!\le j!\leftrightarrow M!\le k!\right)$$
10	7 9	imbi12d	$$⊢j=k\to \left(\left(\left(M\in {\mathbb{N}}_0\wedge M\le j\right)\to M!\le j!\right)\leftrightarrow \left(\left(M\in {\mathbb{N}}_0\wedge M\le k\right)\to M!\le k!\right)\right)$$
11		breq2	$$⊢j=k+1\to \left(M\le j\leftrightarrow M\le k+1\right)$$
12	11	anbi2d	$$⊢j=k+1\to \left(\left(M\in {\mathbb{N}}_0\wedge M\le j\right)\leftrightarrow \left(M\in {\mathbb{N}}_0\wedge M\le k+1\right)\right)$$
13		fveq2	$$⊢j=k+1\to j!=\left(k+1\right)!$$
14	13	breq2d	$$⊢j=k+1\to \left(M!\le j!\leftrightarrow M!\le \left(k+1\right)!\right)$$
15	12 14	imbi12d	$$⊢j=k+1\to \left(\left(\left(M\in {\mathbb{N}}_0\wedge M\le j\right)\to M!\le j!\right)\leftrightarrow \left(\left(M\in {\mathbb{N}}_0\wedge M\le k+1\right)\to M!\le \left(k+1\right)!\right)\right)$$
16		breq2	$$⊢j=N\to \left(M\le j\leftrightarrow M\le N\right)$$
17	16	anbi2d	$$⊢j=N\to \left(\left(M\in {\mathbb{N}}_0\wedge M\le j\right)\leftrightarrow \left(M\in {\mathbb{N}}_0\wedge M\le N\right)\right)$$
18		fveq2	$$⊢j=N\to j!=N!$$
19	18	breq2d	$$⊢j=N\to \left(M!\le j!\leftrightarrow M!\le N!\right)$$
20	17 19	imbi12d	$$⊢j=N\to \left(\left(\left(M\in {\mathbb{N}}_0\wedge M\le j\right)\to M!\le j!\right)\leftrightarrow \left(\left(M\in {\mathbb{N}}_0\wedge M\le N\right)\to M!\le N!\right)\right)$$
21		nn0le0eq0	$$⊢M\in {\mathbb{N}}_0\to \left(M\le 0\leftrightarrow M=0\right)$$
22	21	biimpa	$$⊢\left(M\in {\mathbb{N}}_0\wedge M\le 0\right)\to M=0$$
23	22	fveq2d	$$⊢\left(M\in {\mathbb{N}}_0\wedge M\le 0\right)\to M!=0!$$
24		fac0	$$⊢0!=1$$
25		1re	$$⊢1\in ℝ$$
26	24 25	eqeltri	$$⊢0!\in ℝ$$
27	26	leidi	$$⊢0!\le 0!$$
28	23 27	eqbrtrdi	$$⊢\left(M\in {\mathbb{N}}_0\wedge M\le 0\right)\to M!\le 0!$$
29		impexp	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge M\le k\right)\to M!\le k!\right)\leftrightarrow \left(M\in {\mathbb{N}}_0\to \left(M\le k\to M!\le k!\right)\right)$$
30		nn0re	$$⊢M\in {\mathbb{N}}_0\to M\in ℝ$$
31		nn0re	$$⊢k\in {\mathbb{N}}_0\to k\in ℝ$$
32		peano2re	$$⊢k\in ℝ\to k+1\in ℝ$$
33	31 32	syl	$$⊢k\in {\mathbb{N}}_0\to k+1\in ℝ$$
34		leloe	$$⊢\left(M\in ℝ\wedge k+1\in ℝ\right)\to \left(M\le k+1\leftrightarrow \left(M<k+1\vee M=k+1\right)\right)$$
35	30 33 34	syl2an	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(M\le k+1\leftrightarrow \left(M<k+1\vee M=k+1\right)\right)$$
36		nn0leltp1	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(M\le k\leftrightarrow M<k+1\right)$$
37		faccl	$$⊢k\in {\mathbb{N}}_0\to k!\in \mathbb{N}$$
38	37	nnred	$$⊢k\in {\mathbb{N}}_0\to k!\in ℝ$$
39	37	nnnn0d	$$⊢k\in {\mathbb{N}}_0\to k!\in {\mathbb{N}}_0$$
40	39	nn0ge0d	$$⊢k\in {\mathbb{N}}_0\to 0\le k!$$
41		nn0p1nn	$$⊢k\in {\mathbb{N}}_0\to k+1\in \mathbb{N}$$
42	41	nnge1d	$$⊢k\in {\mathbb{N}}_0\to 1\le k+1$$
43	38 33 40 42	lemulge11d	$$⊢k\in {\mathbb{N}}_0\to k!\le k!\left(k+1\right)$$
44		facp1	$$⊢k\in {\mathbb{N}}_0\to \left(k+1\right)!=k!\left(k+1\right)$$
45	43 44	breqtrrd	$$⊢k\in {\mathbb{N}}_0\to k!\le \left(k+1\right)!$$
46	45	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to k!\le \left(k+1\right)!$$
47		faccl	$$⊢M\in {\mathbb{N}}_0\to M!\in \mathbb{N}$$
48	47	nnred	$$⊢M\in {\mathbb{N}}_0\to M!\in ℝ$$
49	48	adantr	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to M!\in ℝ$$
50	38	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to k!\in ℝ$$
51		peano2nn0	$$⊢k\in {\mathbb{N}}_0\to k+1\in {\mathbb{N}}_0$$
52	51	faccld	$$⊢k\in {\mathbb{N}}_0\to \left(k+1\right)!\in \mathbb{N}$$
53	52	nnred	$$⊢k\in {\mathbb{N}}_0\to \left(k+1\right)!\in ℝ$$
54	53	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(k+1\right)!\in ℝ$$
55		letr	$$⊢\left(M!\in ℝ\wedge k!\in ℝ\wedge \left(k+1\right)!\in ℝ\right)\to \left(\left(M!\le k!\wedge k!\le \left(k+1\right)!\right)\to M!\le \left(k+1\right)!\right)$$
56	49 50 54 55	syl3anc	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(\left(M!\le k!\wedge k!\le \left(k+1\right)!\right)\to M!\le \left(k+1\right)!\right)$$
57	46 56	mpan2d	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(M!\le k!\to M!\le \left(k+1\right)!\right)$$
58	57	imim2d	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(\left(M\le k\to M!\le k!\right)\to \left(M\le k\to M!\le \left(k+1\right)!\right)\right)$$
59	58	com23	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(M\le k\to \left(\left(M\le k\to M!\le k!\right)\to M!\le \left(k+1\right)!\right)\right)$$
60	36 59	sylbird	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(M<k+1\to \left(\left(M\le k\to M!\le k!\right)\to M!\le \left(k+1\right)!\right)\right)$$
61		fveq2	$$⊢M=k+1\to M!=\left(k+1\right)!$$
62	48	leidd	$$⊢M\in {\mathbb{N}}_0\to M!\le M!$$
63		breq2	$$⊢M!=\left(k+1\right)!\to \left(M!\le M!\leftrightarrow M!\le \left(k+1\right)!\right)$$
64	62 63	syl5ibcom	$$⊢M\in {\mathbb{N}}_0\to \left(M!=\left(k+1\right)!\to M!\le \left(k+1\right)!\right)$$
65	61 64	syl5	$$⊢M\in {\mathbb{N}}_0\to \left(M=k+1\to M!\le \left(k+1\right)!\right)$$
66	65	adantr	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(M=k+1\to M!\le \left(k+1\right)!\right)$$
67	66	a1dd	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(M=k+1\to \left(\left(M\le k\to M!\le k!\right)\to M!\le \left(k+1\right)!\right)\right)$$
68	60 67	jaod	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(\left(M<k+1\vee M=k+1\right)\to \left(\left(M\le k\to M!\le k!\right)\to M!\le \left(k+1\right)!\right)\right)$$
69	35 68	sylbid	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to \left(M\le k+1\to \left(\left(M\le k\to M!\le k!\right)\to M!\le \left(k+1\right)!\right)\right)$$
70	69	ex	$$⊢M\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0\to \left(M\le k+1\to \left(\left(M\le k\to M!\le k!\right)\to M!\le \left(k+1\right)!\right)\right)\right)$$
71	70	com13	$$⊢M\le k+1\to \left(k\in {\mathbb{N}}_0\to \left(M\in {\mathbb{N}}_0\to \left(\left(M\le k\to M!\le k!\right)\to M!\le \left(k+1\right)!\right)\right)\right)$$
72	71	com4l	$$⊢k\in {\mathbb{N}}_0\to \left(M\in {\mathbb{N}}_0\to \left(\left(M\le k\to M!\le k!\right)\to \left(M\le k+1\to M!\le \left(k+1\right)!\right)\right)\right)$$
73	72	a2d	$$⊢k\in {\mathbb{N}}_0\to \left(\left(M\in {\mathbb{N}}_0\to \left(M\le k\to M!\le k!\right)\right)\to \left(M\in {\mathbb{N}}_0\to \left(M\le k+1\to M!\le \left(k+1\right)!\right)\right)\right)$$
74	73	imp4a	$$⊢k\in {\mathbb{N}}_0\to \left(\left(M\in {\mathbb{N}}_0\to \left(M\le k\to M!\le k!\right)\right)\to \left(\left(M\in {\mathbb{N}}_0\wedge M\le k+1\right)\to M!\le \left(k+1\right)!\right)\right)$$
75	29 74	syl5bi	$$⊢k\in {\mathbb{N}}_0\to \left(\left(\left(M\in {\mathbb{N}}_0\wedge M\le k\right)\to M!\le k!\right)\to \left(\left(M\in {\mathbb{N}}_0\wedge M\le k+1\right)\to M!\le \left(k+1\right)!\right)\right)$$
76	5 10 15 20 28 75	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(\left(M\in {\mathbb{N}}_0\wedge M\le N\right)\to M!\le N!\right)$$
77	76	3impib	$$⊢\left(N\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\wedge M\le N\right)\to M!\le N!$$
78	77	3com12	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\wedge M\le N\right)\to M!\le N!$$