Theorem factwoffsmonot

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

	Ref	Expression
Assertion	factwoffsmonot	$$⊢\left(\left(X\in {\mathbb{N}}_0\wedge Y\in {\mathbb{N}}_0\wedge X\le Y\right)\wedge N\in {\mathbb{N}}_0\right)\to \left(X+N\right)!\le \left(Y+N\right)!$$

Proof

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