Metamath Proof Explorer


Theorem facwordi

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

Ref Expression
Assertion facwordi ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑀𝑁 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑁 ) )

Proof

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