Metamath Proof Explorer

Theorem factwoffsmonot

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

Ref Expression
Assertion factwoffsmonot ( ( ( 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℕ0 ∧ 𝑋 ≤ 𝑌 ) ∧ 𝑁 ∈ ℕ0 ) → ( ! ‘ ( 𝑋 + 𝑁 ) ) ≤ ( ! ‘ ( 𝑌 + 𝑁 ) ) )

Proof

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