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 biimtrid ⊢ ( 𝑘 ∈ ℕ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 ∧ 𝑀 ≤ 𝑁 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑁 ) )