Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem facwordit 6889

Description: Ordering property of factorial.

Assertion

Ref	Expression
facwordit

---

Proof of Theorem facwordit

Step	Hyp	Ref	Expression
1		breq2 2618	. . . . . 6
2	1	anbi2d 615	. . . . 5
3		fveq2 3715	. . . . . 6
4	3	breq2d 2625	. . . . 5
5	2, 4	imbi12d 625	. . . 4
6		breq2 2618	. . . . . 6
7	6	anbi2d 615	. . . . 5
8		fveq2 3715	. . . . . 6
9	8	breq2d 2625	. . . . 5
10	7, 9	imbi12d 625	. . . 4
11		breq2 2618	. . . . . 6
12	11	anbi2d 615	. . . . 5
13		fveq2 3715	. . . . . 6
14	13	breq2d 2625	. . . . 5
15	12, 14	imbi12d 625	. . . 4
16		breq2 2618	. . . . . 6
17	16	anbi2d 615	. . . . 5
18		fveq2 3715	. . . . . 6
19	18	breq2d 2625	. . . . 5
20	17, 19	imbi12d 625	. . . 4
21		nn0le0eq0t 6074	. . . . . . 7
22	21	biimpa 416	. . . . . 6
23	22	fveq2d 3719	. . . . 5
24		fac0 6879	. . . . . . 7
25		1re 5415	. . . . . . 7
26	24, 25	eqeltr 1541	. . . . . 6
27	26	leid 5592	. . . . 5
28	23, 27	syl6eqbr 2647	. . . 4
29		leloet 5499	. . . . . . . . . . . 12
30		nn0ret 6063	. . . . . . . . . . . 12
31		nn0ret 6063	. . . . . . . . . . . . 13
32		peano2re 5416	. . . . . . . . . . . . 13
33	31, 32	syl 10	. . . . . . . . . . . 12
34	29, 30, 33	syl2an 454	. . . . . . . . . . 11
35		nn0leltp1t 6083	. . . . . . . . . . . . 13
36		facclt 6885	. . . . . . . . . . . . . . . . . . . 20
37		nncnt 5886	. . . . . . . . . . . . . . . . . . . 20
38		ax1id 5262	. . . . . . . . . . . . . . . . . . . 20
39	36, 37, 38	3syl 20	. . . . . . . . . . . . . . . . . . 19
40		lemul2itOLD 5804	. . . . . . . . . . . . . . . . . . . . 21
41	25, 40	mp3anl1 908	. . . . . . . . . . . . . . . . . . . 20
42		nnret 5885	. . . . . . . . . . . . . . . . . . . . 21
43	36, 42	syl 10	. . . . . . . . . . . . . . . . . . . 20
44		nnnn0t 6061	. . . . . . . . . . . . . . . . . . . . 21
45		nn0ge0t 6072	. . . . . . . . . . . . . . . . . . . . 21
46	36, 44, 45	3syl 20	. . . . . . . . . . . . . . . . . . . 20
47		nn0ge0t 6072	. . . . . . . . . . . . . . . . . . . . . 22
48		0re 5420	. . . . . . . . . . . . . . . . . . . . . . . 24
49		leadd1t 5607	. . . . . . . . . . . . . . . . . . . . . . . 24
50	48, 25, 49	mp3an13 905	. . . . . . . . . . . . . . . . . . . . . . 23
51	31, 50	syl 10	. . . . . . . . . . . . . . . . . . . . . 22
52	47, 51	mpbid 195	. . . . . . . . . . . . . . . . . . . . 21
53		ax1cn 5249	. . . . . . . . . . . . . . . . . . . . . 22
54	53	addid2 5311	. . . . . . . . . . . . . . . . . . . . 21
55	52, 54	syl5eqbrr 2644	. . . . . . . . . . . . . . . . . . . 20
56	41, 33, 43, 46, 55	syl2anc 472	. . . . . . . . . . . . . . . . . . 19
57	39, 56	eqbrtrrd 2632	. . . . . . . . . . . . . . . . . 18
58		facp1t 6881	. . . . . . . . . . . . . . . . . 18
59	57, 58	breqtrrd 2636	. . . . . . . . . . . . . . . . 17
60	59	adantl 388	. . . . . . . . . . . . . . . 16
61		letrt 5506	. . . . . . . . . . . . . . . . 17
62		facclt 6885	. . . . . . . . . . . . . . . . . . 19
63		nnret 5885	. . . . . . . . . . . . . . . . . . 19
64	62, 63	syl 10	. . . . . . . . . . . . . . . . . 18
65	64	adantr 389	. . . . . . . . . . . . . . . . 17
66	43	adantl 388	. . . . . . . . . . . . . . . . 17
67		peano2nn0 6079	. . . . . . . . . . . . . . . . . . 19
68		facclt 6885	. . . . . . . . . . . . . . . . . . 19
69		nnret 5885	. . . . . . . . . . . . . . . . . . 19
70	67, 68, 69	3syl 20	. . . . . . . . . . . . . . . . . 18
71	70	adantl 388	. . . . . . . . . . . . . . . . 17
72	61, 65, 66, 71	syl3anc 857	. . . . . . . . . . . . . . . 16
73	60, 72	mpan2d 701	. . . . . . . . . . . . . . 15
74	73	imim2d 25	. . . . . . . . . . . . . 14