Metamath Proof Explorer


Theorem factwoffsmonot

Description: A factorial with offset is monotonely increasing. (Contributed by metakunt, 20-Apr-2024)

Ref Expression
Assertion factwoffsmonot X 0 Y 0 X Y N 0 X + N ! Y + N !

Proof

Step Hyp Ref Expression
1 oveq2 x = 0 X + x = X + 0
2 1 fveq2d x = 0 X + x ! = X + 0 !
3 oveq2 x = 0 Y + x = Y + 0
4 3 fveq2d x = 0 Y + x ! = Y + 0 !
5 2 4 breq12d x = 0 X + x ! Y + x ! X + 0 ! Y + 0 !
6 oveq2 x = y X + x = X + y
7 6 fveq2d x = y X + x ! = X + y !
8 oveq2 x = y Y + x = Y + y
9 8 fveq2d x = y Y + x ! = Y + y !
10 7 9 breq12d x = y X + x ! Y + x ! X + y ! Y + y !
11 oveq2 x = y + 1 X + x = X + y + 1
12 11 fveq2d x = y + 1 X + x ! = X + y + 1 !
13 oveq2 x = y + 1 Y + x = Y + y + 1
14 13 fveq2d x = y + 1 Y + x ! = Y + y + 1 !
15 12 14 breq12d x = y + 1 X + x ! Y + x ! X + y + 1 ! Y + y + 1 !
16 oveq2 x = N X + x = X + N
17 16 fveq2d x = N X + x ! = X + N !
18 oveq2 x = N Y + x = Y + N
19 18 fveq2d x = N Y + x ! = Y + N !
20 17 19 breq12d x = N X + x ! Y + x ! X + N ! Y + N !
21 facwordi X 0 Y 0 X Y X ! Y !
22 nn0cn X 0 X
23 addid1 X X + 0 = X
24 22 23 syl X 0 X + 0 = X
25 24 fveq2d X 0 X + 0 ! = X !
26 25 3ad2ant1 X 0 Y 0 X Y X + 0 ! = X !
27 nn0cn Y 0 Y
28 addid1 Y Y + 0 = Y
29 27 28 syl Y 0 Y + 0 = Y
30 29 fveq2d Y 0 Y + 0 ! = Y !
31 30 3ad2ant2 X 0 Y 0 X Y Y + 0 ! = Y !
32 21 26 31 3brtr4d X 0 Y 0 X Y X + 0 ! Y + 0 !
33 nn0cn y 0 y
34 ax-1cn 1
35 addass X y 1 X + y + 1 = X + y + 1
36 34 35 mp3an3 X y X + y + 1 = X + y + 1
37 22 33 36 syl2an X 0 y 0 X + y + 1 = X + y + 1
38 37 fveq2d X 0 y 0 X + y + 1 ! = X + y + 1 !
39 38 3ad2antl1 X 0 Y 0 X Y y 0 X + y + 1 ! = X + y + 1 !
40 39 adantr X 0 Y 0 X Y y 0 X + y ! Y + y ! X + y + 1 ! = X + y + 1 !
41 nn0addcl X 0 y 0 X + y 0
42 41 3adant2 X 0 Y 0 y 0 X + y 0
43 42 adantr X 0 Y 0 y 0 X Y X + y 0
44 nn0addcl Y 0 y 0 Y + y 0
45 44 3adant1 X 0 Y 0 y 0 Y + y 0
46 45 adantr X 0 Y 0 y 0 X Y Y + y 0
47 nn0re X 0 X
48 nn0re Y 0 Y
49 nn0re y 0 y
50 leadd1 X Y y X Y X + y Y + y
51 47 48 49 50 syl3an X 0 Y 0 y 0 X Y X + y Y + y
52 51 biimpa X 0 Y 0 y 0 X Y X + y Y + y
53 facwordi X + y 0 Y + y 0 X + y Y + y X + y ! Y + y !
54 43 46 52 53 syl3anc X 0 Y 0 y 0 X Y X + y ! Y + y !
55 54 3an1rs X 0 Y 0 X Y y 0 X + y ! Y + y !
56 nn0re X + y 0 X + y
57 43 56 syl X 0 Y 0 y 0 X Y X + y
58 nn0re Y + y 0 Y + y
59 46 58 syl X 0 Y 0 y 0 X Y Y + y
60 57 59 jca X 0 Y 0 y 0 X Y X + y Y + y
61 1re 1
62 leadd1 X + y Y + y 1 X + y Y + y X + y + 1 Y + y + 1
63 61 62 mp3an3 X + y Y + y X + y Y + y X + y + 1 Y + y + 1
64 60 63 syl X 0 Y 0 y 0 X Y X + y Y + y X + y + 1 Y + y + 1
65 52 64 mpbid X 0 Y 0 y 0 X Y X + y + 1 Y + y + 1
66 65 3an1rs X 0 Y 0 X Y y 0 X + y + 1 Y + y + 1
67 55 66 jca X 0 Y 0 X Y y 0 X + y ! Y + y ! X + y + 1 Y + y + 1
68 faccl X + y 0 X + y !
69 nnre X + y ! X + y !
70 41 68 69 3syl X 0 y 0 X + y !
71 70 3adant2 X 0 Y 0 y 0 X + y !
72 nngt0 X + y ! 0 < X + y !
73 41 68 72 3syl X 0 y 0 0 < X + y !
74 0re 0
75 ltle 0 X + y ! 0 < X + y ! 0 X + y !
76 74 75 mpan X + y ! 0 < X + y ! 0 X + y !
77 70 76 syl X 0 y 0 0 < X + y ! 0 X + y !
78 73 77 mpd X 0 y 0 0 X + y !
79 78 3adant2 X 0 Y 0 y 0 0 X + y !
80 71 79 jca X 0 Y 0 y 0 X + y ! 0 X + y !
81 faccl Y + y 0 Y + y !
82 nnre Y + y ! Y + y !
83 44 81 82 3syl Y 0 y 0 Y + y !
84 83 3adant1 X 0 Y 0 y 0 Y + y !
85 80 84 jca X 0 Y 0 y 0 X + y ! 0 X + y ! Y + y !
86 1nn0 1 0
87 nn0addcl X + y 0 1 0 X + y + 1 0
88 86 87 mpan2 X + y 0 X + y + 1 0
89 41 88 syl X 0 y 0 X + y + 1 0
90 nn0re X + y + 1 0 X + y + 1
91 89 90 syl X 0 y 0 X + y + 1
92 91 3adant2 X 0 Y 0 y 0 X + y + 1
93 nn0ge0 X + y + 1 0 0 X + y + 1
94 89 93 syl X 0 y 0 0 X + y + 1
95 94 3adant2 X 0 Y 0 y 0 0 X + y + 1
96 92 95 jca X 0 Y 0 y 0 X + y + 1 0 X + y + 1
97 nn0readdcl Y 0 y 0 Y + y
98 1red Y 0 y 0 1
99 97 98 readdcld Y 0 y 0 Y + y + 1
100 99 3adant1 X 0 Y 0 y 0 Y + y + 1
101 96 100 jca X 0 Y 0 y 0 X + y + 1 0 X + y + 1 Y + y + 1
102 85 101 jca X 0 Y 0 y 0 X + y ! 0 X + y ! Y + y ! X + y + 1 0 X + y + 1 Y + y + 1
103 lemul12a X + y ! 0 X + y ! Y + y ! X + y + 1 0 X + y + 1 Y + y + 1 X + y ! Y + y ! X + y + 1 Y + y + 1 X + y ! X + y + 1 Y + y ! Y + y + 1
104 102 103 syl X 0 Y 0 y 0 X + y ! Y + y ! X + y + 1 Y + y + 1 X + y ! X + y + 1 Y + y ! Y + y + 1
105 104 3expa X 0 Y 0 y 0 X + y ! Y + y ! X + y + 1 Y + y + 1 X + y ! X + y + 1 Y + y ! Y + y + 1
106 105 3adantl3 X 0 Y 0 X Y y 0 X + y ! Y + y ! X + y + 1 Y + y + 1 X + y ! X + y + 1 Y + y ! Y + y + 1
107 67 106 mpd X 0 Y 0 X Y y 0 X + y ! X + y + 1 Y + y ! Y + y + 1
108 facp1 X + y 0 X + y + 1 ! = X + y ! X + y + 1
109 43 108 syl X 0 Y 0 y 0 X Y X + y + 1 ! = X + y ! X + y + 1
110 facp1 Y + y 0 Y + y + 1 ! = Y + y ! Y + y + 1
111 46 110 syl X 0 Y 0 y 0 X Y Y + y + 1 ! = Y + y ! Y + y + 1
112 109 111 jca X 0 Y 0 y 0 X Y X + y + 1 ! = X + y ! X + y + 1 Y + y + 1 ! = Y + y ! Y + y + 1
113 breq12 X + y + 1 ! = X + y ! X + y + 1 Y + y + 1 ! = Y + y ! Y + y + 1 X + y + 1 ! Y + y + 1 ! X + y ! X + y + 1 Y + y ! Y + y + 1
114 112 113 syl X 0 Y 0 y 0 X Y X + y + 1 ! Y + y + 1 ! X + y ! X + y + 1 Y + y ! Y + y + 1
115 114 3an1rs X 0 Y 0 X Y y 0 X + y + 1 ! Y + y + 1 ! X + y ! X + y + 1 Y + y ! Y + y + 1
116 107 115 mpbird X 0 Y 0 X Y y 0 X + y + 1 ! Y + y + 1 !
117 116 adantr X 0 Y 0 X Y y 0 X + y ! Y + y ! X + y + 1 ! Y + y + 1 !
118 addass Y y 1 Y + y + 1 = Y + y + 1
119 34 118 mp3an3 Y y Y + y + 1 = Y + y + 1
120 27 33 119 syl2an Y 0 y 0 Y + y + 1 = Y + y + 1
121 120 fveq2d Y 0 y 0 Y + y + 1 ! = Y + y + 1 !
122 121 3ad2antl2 X 0 Y 0 X Y y 0 Y + y + 1 ! = Y + y + 1 !
123 122 adantr X 0 Y 0 X Y y 0 X + y ! Y + y ! Y + y + 1 ! = Y + y + 1 !
124 117 123 breqtrd X 0 Y 0 X Y y 0 X + y ! Y + y ! X + y + 1 ! Y + y + 1 !
125 40 124 eqbrtrrd X 0 Y 0 X Y y 0 X + y ! Y + y ! X + y + 1 ! Y + y + 1 !
126 5 10 15 20 32 125 nn0indd X 0 Y 0 X Y N 0 X + N ! Y + N !