Theorem facdivt 6908

Description: A natural number divides the factorial of an equal or larger number.

Assertion

Ref	Expression
facdivt	|- ((M e. NN0 /\ N e. NN /\ N <_ M) -> ((!` M) / N) e. NN)

Proof of Theorem facdivt

Step	Hyp	Ref	Expression
1		breq2 2620	. . . . 5 |- (j = 0 -> (N <_ j <-> N <_ 0))
2		fveq2 3721	. . . . . . 7 |- (j = 0 -> (!` j) = (!` 0))
3	2	opreq1d 3972	. . . . . 6 |- (j = 0 -> ((!` j) / N) = ((!` 0) / N))
4	3	eleq1d 1539	. . . . 5 |- (j = 0 -> (((!` j) / N) e. NN <-> ((!` 0) / N) e. NN))
5	1, 4	imbi12d 625	. . . 4 |- (j = 0 -> ((N <_ j -> ((!` j) / N) e. NN) <-> (N <_ 0 -> ((!` 0) / N) e. NN)))
6	5	imbi2d 611	. . 3 |- (j = 0 -> ((N e. NN -> (N <_ j -> ((!` j) / N) e. NN)) <-> (N e. NN -> (N <_ 0 -> ((!` 0) / N) e. NN))))
7		breq2 2620	. . . . 5 |- (j = k -> (N <_ j <-> N <_ k))
8		fveq2 3721	. . . . . . 7 |- (j = k -> (!` j) = (!` k))
9	8	opreq1d 3972	. . . . . 6 |- (j = k -> ((!` j) / N) = ((!` k) / N))
10	9	eleq1d 1539	. . . . 5 |- (j = k -> (((!` j) / N) e. NN <-> ((!` k) / N) e. NN))
11	7, 10	imbi12d 625	. . . 4 |- (j = k -> ((N <_ j -> ((!` j) / N) e. NN) <-> (N <_ k -> ((!` k) / N) e. NN)))
12	11	imbi2d 611	. . 3 |- (j = k -> ((N e. NN -> (N <_ j -> ((!` j) / N) e. NN)) <-> (N e. NN -> (N <_ k -> ((!` k) / N) e. NN))))
13		breq2 2620	. . . . 5 |- (j = (k + 1) -> (N <_ j <-> N <_ (k + 1)))
14		fveq2 3721	. . . . . . 7 |- (j = (k + 1) -> (!` j) = (!` (k + 1)))
15	14	opreq1d 3972	. . . . . 6 |- (j = (k + 1) -> ((!` j) / N) = ((!` (k + 1)) / N))
16	15	eleq1d 1539	. . . . 5 |- (j = (k + 1) -> (((!` j) / N) e. NN <-> ((!` (k + 1)) / N) e. NN))
17	13, 16	imbi12d 625	. . . 4 |- (j = (k + 1) -> ((N <_ j -> ((!` j) / N) e. NN) <-> (N <_ (k + 1) -> ((!` (k + 1)) / N) e. NN)))
18	17	imbi2d 611	. . 3 |- (j = (k + 1) -> ((N e. NN -> (N <_ j -> ((!` j) / N) e. NN)) <-> (N e. NN -> (N <_ (k + 1) -> ((!` (k + 1)) / N) e. NN))))
19		breq2 2620	. . . . 5 |- (j = M -> (N <_ j <-> N <_ M))
20		fveq2 3721	. . . . . . 7 |- (j = M -> (!` j) = (!` M))
21	20	opreq1d 3972	. . . . . 6 |- (j = M -> ((!` j) / N) = ((!` M) / N))
22	21	eleq1d 1539	. . . . 5 |- (j = M -> (((!` j) / N) e. NN <-> ((!` M) / N) e. NN))
23	19, 22	imbi12d 625	. . . 4 |- (j = M -> ((N <_ j -> ((!` j) / N) e. NN) <-> (N <_ M -> ((!` M) / N) e. NN)))
24	23	imbi2d 611	. . 3 |- (j = M -> ((N e. NN -> (N <_ j -> ((!` j) / N) e. NN)) <-> (N e. NN -> (N <_ M -> ((!` M) / N) e. NN))))
25		nngt0t 5908	. . . . 5 |- (N e. NN -> 0 < N)
26		nnret 5891	. . . . . 6 |- (N e. NN -> N e. RR)
27		0re 5427	. . . . . . 7 |- 0 e. RR
28		ltnlet 5498	. . . . . . 7 |- ((0 e. RR /\ N e. RR) -> (0 < N <-> -. N <_ 0))
29	27, 28	mpan 694	. . . . . 6 |- (N e. RR -> (0 < N <-> -. N <_ 0))
30	26, 29	syl 10	. . . . 5 |- (N e. NN -> (0 < N <-> -. N <_ 0))
31	25, 30	mpbid 195	. . . 4 |- (N e. NN -> -. N <_ 0)
32	31	pm2.21d 78	. . 3 |- (N e. NN -> (N <_ 0 -> ((!` 0) / N) e. NN))
33		leloet 5505	. . . . . . . . . . . 12 |- ((N e. RR /\ (k + 1) e. RR) -> (N <_ (k + 1) <-> (N < (k + 1) \/ N = (k + 1))))
34		peano2nn0 6085	. . . . . . . . . . . . 13 |- (k e. NN0 -> (k + 1) e. NN0)
35		nn0ret 6069	. . . . . . . . . . . . 13 |- ((k + 1) e. NN0 -> (k + 1) e. RR)
36	34, 35	syl 10	. . . . . . . . . . . 12 |- (k e. NN0 -> (k + 1) e. RR)
37	33, 26, 36	syl2an 454	. . . . . . . . . . 11 |- ((N e. NN /\ k e. NN0) -> (N <_ (k + 1) <-> (N < (k + 1) \/ N = (k + 1))))
38		nn0leltp1t 6089	. . . . . . . . . . . . . 14 |- ((N e. NN0 /\ k e. NN0) -> (N <_ k <-> N < (k + 1)))
39		nnnn0t 6067	. . . . . . . . . . . . . 14 |- (N e. NN -> N e. NN0)
40	38, 39	sylan 448	. . . . . . . . . . . . 13 |- ((N e. NN /\ k e. NN0) -> (N <_ k <-> N < (k + 1)))
41		nnmulclt 5903	. . . . . . . . . . . . . . . . . . 19 |- ((((!` k) / N) e. NN /\ (k + 1) e. NN) -> (((!` k) / N) x. (k + 1)) e. NN)
42		nn0p1nnt 6136	. . . . . . . . . . . . . . . . . . 19 |- (k e. NN0 -> (k + 1) e. NN)
43	41, 42	sylan2 451	. . . . . . . . . . . . . . . . . 18 |- ((((!` k) / N) e. NN /\ k e. NN0) -> (((!` k) / N) x. (k + 1)) e. NN)
44	43	expcom 374	. . . . . . . . . . . . . . . . 17 |- (k e. NN0 -> (((!` k) / N) e. NN -> (((!` k) / N) x. (k + 1)) e. NN))
45	44	adantl 388	. . . . . . . . . . . . . . . 16 |- ((N e. NN /\ k e. NN0) -> (((!` k) / N) e. NN -> (((!` k) / N) x. (k + 1)) e. NN))
46		div23t 5719	. . . . . . . . . . . . . . . . . 18 |- ((((!` k) e. CC /\ (k + 1) e. CC /\ N e. CC) /\ N =/= 0) -> (((!` k) x. (k + 1)) / N) = (((!` k) / N) x. (k + 1)))
47		facclt 6906	. . . . . . . . . . . . . . . . . . . . 21 |- (k e. NN0 -> (!` k) e. NN)
48		nncnt 5892	. . . . . . . . . . . . . . . . . . . . 21 |- ((!` k) e. NN -> (!` k) e. CC)
49	47, 48	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (k e. NN0 -> (!` k) e. CC)
50	49	adantl 388	. . . . . . . . . . . . . . . . . . 19 |- ((N e. NN /\ k e. NN0) -> (!` k) e. CC)
51	36	recnd 5302	. . . . . . . . . . . . . . . . . . . 20 |- (k e. NN0 -> (k + 1) e. CC)
52	51	adantl 388	. . . . . . . . . . . . . . . . . . 19 |- ((N e. NN /\ k e. NN0) -> (k + 1) e. CC)
53		nncnt 5892	. . . . . . . . . . . . . . . . . . . 20 |- (N e. NN -> N e. CC)
54	53	adantr 389	. . . . . . . . . . . . . . . . . . 19 |- ((N e. NN /\ k e. NN0) -> N e. CC)
55	50, 52, 54	3jca 818	. . . . . . . . . . . . . . . . . 18 |- ((N e. NN /\ k e. NN0) -> ((!` k) e. CC /\ (k + 1) e. CC /\ N e. CC))
56		nnne0t 5911	. . . . . . . . . . . . . . . . . . 19 |- (N e. NN -> N =/= 0)
57	56	adantr 389	. . . . . . . . . . . . . . . . . 18 |- ((N e. NN /\ k e. NN0) -> N =/= 0)
58	46, 55, 57	sylanc 471	. . . . . . . . . . . . . . . . 17 |- ((N e. NN /\ k e. NN0) -> (((!` k) x. (k + 1)) / N) = (((!` k) / N) x. (k + 1)))
59	58	eleq1d 1539	. . . . . . . . . . . . . . . 16 |- ((N e. NN /\ k e. NN0) -> ((((!` k) x. (k + 1)) / N) e. NN <-> (((!` k) / N) x. (k + 1)) e. NN))
60	45, 59	sylibrd 204	. . . . . . . . . . . . . . 15 |- ((N e. NN /\ k e. NN0) -> (((!` k) / N) e. NN -> (((!` k) x. (k + 1)) / N) e. NN))
61	60	imim2d 25	. . . . . . . . . . . . . 14 |- ((N e. NN /\ k e. NN0) -> ((N <_ k -> ((!` k) / N) e. NN) -> (N <_ k -> (((!` k) x. (k + 1)) / N) e. NN)))
62	61	com23 32	. . . . . . . . . . . . 13 |- ((N e. NN /\ k e. NN0) -> (N <_ k -> ((N <_ k -> ((!` k) / N) e. NN) -> (((!` k) x. (k + 1)) / N) e. NN)))
63	40, 62	sylbird 205	. . . . . . . . . . . 12 |- ((N e. NN /\ k e. NN0) -> (N < (k + 1) -> ((N <_ k -> ((!` k) / N) e. NN) -> (((!` k) x. (k + 1)) / N) e. NN)))
64		opreq2 3966	. . . . . . . . . . . . . . . 16 |- (N = (k + 1) -> ((!` k) x. N) = ((!` k) x. (k + 1)))
65	64	opreq1d 3972	. . . . . . . . . . . . . . 15 |- (N = (k + 1) -> (((!` k) x. N) / N) = (((!` k)