Metamath Proof Explorer

Theorem factwoffsmonot

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

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