Metamath Proof Explorer

Theorem bcle2d

Description: Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025)

Ref Expression
Hypotheses bcle2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
bcle2d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
bcle2d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
bcle2d.4 ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
bcle2d.5 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
bcle2d.6 ⊢ ( 𝜑 → 𝐷 ≤ 𝐶 )
Assertion bcle2d ( 𝜑 → ( ( 𝐴 + 𝐶 ) C ( 𝐴 + 𝐷 ) ) ≤ ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 bcle2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
2 bcle2d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
3 bcle2d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
4 bcle2d.4 ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
5 bcle2d.5 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
6 bcle2d.6 ⊢ ( 𝜑 → 𝐷 ≤ 𝐶 )
7 bcval2 ⊢ ( ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) → ( ( 𝐴 + 𝐶 ) C ( 𝐴 + 𝐷 ) ) = ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) · ( ! ‘ ( 𝐴 + 𝐷 ) ) ) ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) C ( 𝐴 + 𝐷 ) ) = ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) · ( ! ‘ ( 𝐴 + 𝐷 ) ) ) ) )
9 1 3 nn0addcld ⊢ ( 𝜑 → ( 𝐴 + 𝐶 ) ∈ ℕ0 )
10 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐶 ) ∈ ℕ0 )
11 10 faccld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐶 ) ) ∈ ℕ )
12 11 nncnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐶 ) ) ∈ ℂ )
13 1 nn0zd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
14 13 4 zaddcld ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ℤ )
15 elfzle1 ⊢ ( ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) → 0 ≤ ( 𝐴 + 𝐷 ) )
16 14 15 anim12i ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐷 ) ∈ ℤ ∧ 0 ≤ ( 𝐴 + 𝐷 ) ) )
17 elnn0z ⊢ ( ( 𝐴 + 𝐷 ) ∈ ℕ0 ↔ ( ( 𝐴 + 𝐷 ) ∈ ℤ ∧ 0 ≤ ( 𝐴 + 𝐷 ) ) )
18 16 17 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐷 ) ∈ ℕ0 )
19 18 faccld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐷 ) ) ∈ ℕ )
20 19 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐷 ) ) ∈ ℕ0 )
21 20 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐷 ) ) ∈ ℂ )
22 1 nn0red ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐴 ∈ ℝ )
24 23 recnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐴 ∈ ℂ )
25 3 nn0cnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐶 ∈ ℂ )
27 4 zred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐷 ∈ ℝ )
29 28 recnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐷 ∈ ℂ )
30 24 26 24 29 addsub4d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) = ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐷 ) ) )
31 24 subidd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 − 𝐴 ) = 0 )
32 31 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐷 ) ) = ( 0 + ( 𝐶 − 𝐷 ) ) )
33 26 29 subcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) ∈ ℂ )
34 33 addlidd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 0 + ( 𝐶 − 𝐷 ) ) = ( 𝐶 − 𝐷 ) )
35 32 34 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐷 ) ) = ( 𝐶 − 𝐷 ) )
36 30 35 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) = ( 𝐶 − 𝐷 ) )
37 3 nn0zd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐶 ∈ ℤ )
39 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐷 ∈ ℤ )
40 38 39 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) ∈ ℤ )
41 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐷 ≤ 𝐶 )
42 38 zred ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐶 ∈ ℝ )
43 42 28 subge0d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 0 ≤ ( 𝐶 − 𝐷 ) ↔ 𝐷 ≤ 𝐶 ) )
44 41 43 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 0 ≤ ( 𝐶 − 𝐷 ) )
45 40 44 jca ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐶 − 𝐷 ) ∈ ℤ ∧ 0 ≤ ( 𝐶 − 𝐷 ) ) )
46 elnn0z ⊢ ( ( 𝐶 − 𝐷 ) ∈ ℕ0 ↔ ( ( 𝐶 − 𝐷 ) ∈ ℤ ∧ 0 ≤ ( 𝐶 − 𝐷 ) ) )
47 45 46 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) ∈ ℕ0 )
48 36 47 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ∈ ℕ0 )
49 48 faccld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ∈ ℕ )
50 49 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ∈ ℕ0 )
51 50 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ∈ ℂ )
52 19 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐷 ) ) ≠ 0 )
53 49 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ≠ 0 )
54 12 21 51 52 53 divdiv1d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) / ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) = ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( 𝐴 + 𝐷 ) ) · ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) ) )
55 54 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( 𝐴 + 𝐷 ) ) · ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) ) = ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) / ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) )
56 0zd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 0 ∈ ℤ )
57 10 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐶 ) ∈ ℤ )
58 28 renegcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → - 𝐷 ∈ ℝ )
59 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐶 ∈ ℕ0 )
60 59 nn0red ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐶 ∈ ℝ )
61 df-neg ⊢ - 𝐷 = ( 0 − 𝐷 )
62 61 a1i ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → - 𝐷 = ( 0 − 𝐷 ) )
63 15 adantl ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 0 ≤ ( 𝐴 + 𝐷 ) )
64 0red ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 0 ∈ ℝ )
65 64 28 23 lesubaddd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 0 − 𝐷 ) ≤ 𝐴 ↔ 0 ≤ ( 𝐴 + 𝐷 ) ) )
66 63 65 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 0 − 𝐷 ) ≤ 𝐴 )
67 62 66 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → - 𝐷 ≤ 𝐴 )
68 58 23 60 67 leadd2dd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 + - 𝐷 ) ≤ ( 𝐶 + 𝐴 ) )
69 26 29 negsubd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 + - 𝐷 ) = ( 𝐶 − 𝐷 ) )
70 26 24 addcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 + 𝐴 ) = ( 𝐴 + 𝐶 ) )
71 68 69 70 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) ≤ ( 𝐴 + 𝐶 ) )
72 56 57 40 44 71 elfzd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) )
73 fallfacval4 ⊢ ( ( 𝐶 − 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) → ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) ) ) )
74 72 73 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) ) ) )
75 9 nn0cnd ⊢ ( 𝜑 → ( 𝐴 + 𝐶 ) ∈ ℂ )
76 27 recnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
77 75 25 76 subsubd ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 + 𝐶 ) − 𝐶 ) + 𝐷 ) )
78 22 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
79 78 25 pncand ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) − 𝐶 ) = 𝐴 )
80 79 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐶 ) − 𝐶 ) + 𝐷 ) = ( 𝐴 + 𝐷 ) )
81 77 80 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) = ( 𝐴 + 𝐷 ) )
82 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) = ( 𝐴 + 𝐷 ) )
83 82 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) ) = ( ! ‘ ( 𝐴 + 𝐷 ) ) )
84 83 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) ) ) = ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) )
85 74 84 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) )
86 85 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) = ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) )
87 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) )
88 fzfid ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ∈ Fin )
89 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 𝐴 ∈ ℝ )
90 3 nn0red ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐶 ∈ ℝ )
92 91 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 𝐶 ∈ ℝ )
93 89 92 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 𝐴 + 𝐶 ) ∈ ℝ )
94 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) → 𝑘 ∈ ℤ )
95 94 zred ⊢ ( 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) → 𝑘 ∈ ℝ )
96 95 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 𝑘 ∈ ℝ )
97 93 96 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( ( 𝐴 + 𝐶 ) − 𝑘 ) ∈ ℝ )
98 0red ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 0 ∈ ℝ )
99 98 96 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 0 + 𝑘 ) ∈ ℝ )
100 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 𝐷 ∈ ℝ )
101 92 100 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 𝐶 − 𝐷 ) ∈ ℝ )
102 1red ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 1 ∈ ℝ )
103 101 102 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( ( 𝐶 − 𝐷 ) − 1 ) ∈ ℝ )
104 96 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 𝑘 ∈ ℂ )
105 104 addlidd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 0 + 𝑘 ) = 𝑘 )
106 elfzle2 ⊢ ( 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) → 𝑘 ≤ ( ( 𝐶 − 𝐷 ) − 1 ) )
107 106 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 𝑘 ≤ ( ( 𝐶 − 𝐷 ) − 1 ) )
108 105 107 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 0 + 𝑘 ) ≤ ( ( 𝐶 − 𝐷 ) − 1 ) )
109 101 lem1d ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( ( 𝐶 − 𝐷 ) − 1 ) ≤ ( 𝐶 − 𝐷 ) )
110 71 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 𝐶 − 𝐷 ) ≤ ( 𝐴 + 𝐶 ) )
111 103 101 93 109 110 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( ( 𝐶 − 𝐷 ) − 1 ) ≤ ( 𝐴 + 𝐶 ) )
112 99 103 93 108 111 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 0 + 𝑘 ) ≤ ( 𝐴 + 𝐶 ) )
113 64 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 0 ∈ ℝ )
114 leaddsub ⊢ ( ( 0 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 𝐴 + 𝐶 ) ∈ ℝ ) → ( ( 0 + 𝑘 ) ≤ ( 𝐴 + 𝐶 ) ↔ 0 ≤ ( ( 𝐴 + 𝐶 ) − 𝑘 ) ) )
115 113 96 93 114 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( ( 0 + 𝑘 ) ≤ ( 𝐴 + 𝐶 ) ↔ 0 ≤ ( ( 𝐴 + 𝐶 ) − 𝑘 ) ) )
116 112 115 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 0 ≤ ( ( 𝐴 + 𝐶 ) − 𝑘 ) )
117 2 nn0red ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
118 117 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐵 ∈ ℝ )
119 118 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 𝐵 ∈ ℝ )
120 119 92 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
121 120 96 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( ( 𝐵 + 𝐶 ) − 𝑘 ) ∈ ℝ )
122 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐴 ≤ 𝐵 )
123 122 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → 𝐴 ≤ 𝐵 )
124 89 119 92 123 leadd1dd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( 𝐴 + 𝐶 ) ≤ ( 𝐵 + 𝐶 ) )
125 93 120 96 124 lesub1dd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ) → ( ( 𝐴 + 𝐶 ) − 𝑘 ) ≤ ( ( 𝐵 + 𝐶 ) − 𝑘 ) )
126 87 88 97 116 121 125 fprodle ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ∏ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ( ( 𝐴 + 𝐶 ) − 𝑘 ) ≤ ∏ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ( ( 𝐵 + 𝐶 ) − 𝑘 ) )
127 75 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐶 ) ∈ ℂ )
128 fallfacval ⊢ ( ( ( 𝐴 + 𝐶 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℕ0 ) → ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ∏ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ( ( 𝐴 + 𝐶 ) − 𝑘 ) )
129 127 47 128 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ∏ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ( ( 𝐴 + 𝐶 ) − 𝑘 ) )
130 129 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ∏ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ( ( 𝐴 + 𝐶 ) − 𝑘 ) = ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) )
131 118 recnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐵 ∈ ℂ )
132 131 26 addcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
133 fallfacval ⊢ ( ( ( 𝐵 + 𝐶 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℕ0 ) → ( ( 𝐵 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ∏ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ( ( 𝐵 + 𝐶 ) − 𝑘 ) )
134 132 47 133 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ∏ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ( ( 𝐵 + 𝐶 ) − 𝑘 ) )
135 134 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ∏ 𝑘 ∈ ( 0 ... ( ( 𝐶 − 𝐷 ) − 1 ) ) ( ( 𝐵 + 𝐶 ) − 𝑘 ) = ( ( 𝐵 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) )
136 126 130 135 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) ≤ ( ( 𝐵 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) )
137 2 nn0zd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
138 137 37 zaddcld ⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) ∈ ℤ )
139 138 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐶 ) ∈ ℤ )
140 23 28 readdcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐷 ) ∈ ℝ )
141 137 4 zaddcld ⊢ ( 𝜑 → ( 𝐵 + 𝐷 ) ∈ ℤ )
142 141 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐷 ) ∈ ℤ )
143 142 zred ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐷 ) ∈ ℝ )
144 23 118 28 122 leadd1dd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐷 ) )
145 64 140 143 63 144 letrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 0 ≤ ( 𝐵 + 𝐷 ) )
146 64 28 118 lesubaddd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 0 − 𝐷 ) ≤ 𝐵 ↔ 0 ≤ ( 𝐵 + 𝐷 ) ) )
147 145 146 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 0 − 𝐷 ) ≤ 𝐵 )
148 62 147 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → - 𝐷 ≤ 𝐵 )
149 58 118 60 148 leadd2dd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 + - 𝐷 ) ≤ ( 𝐶 + 𝐵 ) )
150 26 131 addcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 ) )
151 149 69 150 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) ≤ ( 𝐵 + 𝐶 ) )
152 56 139 40 44 151 elfzd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) )
153 fallfacval4 ⊢ ( ( 𝐶 − 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) → ( ( 𝐵 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) ) ) )
154 152 153 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) ) ) )
155 132 26 29 subsubd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐵 + 𝐶 ) − 𝐶 ) + 𝐷 ) )
156 131 26 pncand ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) − 𝐶 ) = 𝐵 )
157 156 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( 𝐵 + 𝐶 ) − 𝐶 ) + 𝐷 ) = ( 𝐵 + 𝐷 ) )
158 155 157 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) = ( 𝐵 + 𝐷 ) )
159 158 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) ) = ( ! ‘ ( 𝐵 + 𝐷 ) ) )
160 159 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐶 − 𝐷 ) ) ) ) = ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) )
161 154 160 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) = ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) )
162 136 161 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) FallFac ( 𝐶 − 𝐷 ) ) ≤ ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) )
163 86 162 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) ≤ ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) )
164 11 nnred ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐶 ) ) ∈ ℝ )
165 19 nnred ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐷 ) ) ∈ ℝ )
166 164 165 52 redivcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) ∈ ℝ )
167 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐵 ∈ ℕ0 )
168 167 59 nn0addcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐶 ) ∈ ℕ0 )
169 168 faccld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐵 + 𝐶 ) ) ∈ ℕ )
170 169 nnred ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐵 + 𝐶 ) ) ∈ ℝ )
171 142 145 jca ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐷 ) ∈ ℤ ∧ 0 ≤ ( 𝐵 + 𝐷 ) ) )
172 elnn0z ⊢ ( ( 𝐵 + 𝐷 ) ∈ ℕ0 ↔ ( ( 𝐵 + 𝐷 ) ∈ ℤ ∧ 0 ≤ ( 𝐵 + 𝐷 ) ) )
173 171 172 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐷 ) ∈ ℕ0 )
174 173 faccld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐵 + 𝐷 ) ) ∈ ℕ )
175 174 nnred ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐵 + 𝐷 ) ) ∈ ℝ )
176 174 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐵 + 𝐷 ) ) ≠ 0 )
177 170 175 176 redivcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) ∈ ℝ )
178 35 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) = ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐷 ) ) )
179 30 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) )
180 178 179 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) = ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) )
181 180 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐶 − 𝐷 ) ) = ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) )
182 181 49 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐶 − 𝐷 ) ) ∈ ℕ )
183 182 nnrpd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐶 − 𝐷 ) ) ∈ ℝ+ )
184 166 177 183 lediv1d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) ≤ ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) ↔ ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) / ( ! ‘ ( 𝐶 − 𝐷 ) ) ) ≤ ( ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) / ( ! ‘ ( 𝐶 − 𝐷 ) ) ) ) )
185 163 184 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) / ( ! ‘ ( 𝐶 − 𝐷 ) ) ) ≤ ( ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) / ( ! ‘ ( 𝐶 − 𝐷 ) ) ) )
186 181 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) / ( ! ‘ ( 𝐶 − 𝐷 ) ) ) = ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) / ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) )
187 131 26 pncan2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) − 𝐵 ) = 𝐶 )
188 187 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 𝐶 = ( ( 𝐵 + 𝐶 ) − 𝐵 ) )
189 188 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) − 𝐵 ) − 𝐷 ) )
190 132 131 29 subsub4d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( 𝐵 + 𝐶 ) − 𝐵 ) − 𝐷 ) = ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) )
191 189 190 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐶 − 𝐷 ) = ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) )
192 191 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐶 − 𝐷 ) ) = ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) )
193 192 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) / ( ! ‘ ( 𝐶 − 𝐷 ) ) ) = ( ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) / ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ) )
194 185 186 193 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) / ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) ≤ ( ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) / ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ) )
195 169 nncnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐵 + 𝐶 ) ) ∈ ℂ )
196 174 nncnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐵 + 𝐷 ) ) ∈ ℂ )
197 131 26 29 pnpcand ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) = ( 𝐶 − 𝐷 ) )
198 197 47 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ∈ ℕ0 )
199 198 faccld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ∈ ℕ )
200 199 nncnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ∈ ℂ )
201 199 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ≠ 0 )
202 195 196 200 176 201 divdiv1d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ! ‘ ( 𝐵 + 𝐷 ) ) ) / ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ) = ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( 𝐵 + 𝐷 ) ) · ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ) ) )
203 194 202 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ! ‘ ( 𝐴 + 𝐷 ) ) ) / ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) ≤ ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( 𝐵 + 𝐷 ) ) · ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ) ) )
204 55 203 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( 𝐴 + 𝐷 ) ) · ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) ) ≤ ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( 𝐵 + 𝐷 ) ) · ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ) ) )
205 19 nncnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( 𝐴 + 𝐷 ) ) ∈ ℂ )
206 49 nncnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ∈ ℂ )
207 205 206 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐷 ) ) · ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) = ( ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) · ( ! ‘ ( 𝐴 + 𝐷 ) ) ) )
208 207 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( 𝐴 + 𝐷 ) ) · ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) ) ) = ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) · ( ! ‘ ( 𝐴 + 𝐷 ) ) ) ) )
209 196 200 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐵 + 𝐷 ) ) · ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ) = ( ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) · ( ! ‘ ( 𝐵 + 𝐷 ) ) ) )
210 209 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( 𝐵 + 𝐷 ) ) · ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) ) ) = ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) · ( ! ‘ ( 𝐵 + 𝐷 ) ) ) ) )
211 204 208 210 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) · ( ! ‘ ( 𝐴 + 𝐷 ) ) ) ) ≤ ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) · ( ! ‘ ( 𝐵 + 𝐷 ) ) ) ) )
212 elfzle2 ⊢ ( ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) → ( 𝐴 + 𝐷 ) ≤ ( 𝐴 + 𝐶 ) )
213 212 adantl ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐷 ) ≤ ( 𝐴 + 𝐶 ) )
214 131 29 addcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐷 ) = ( 𝐷 + 𝐵 ) )
215 214 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐷 ) + ( 𝐴 − 𝐵 ) ) = ( ( 𝐷 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) )
216 29 131 addcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐷 + 𝐵 ) ∈ ℂ )
217 23 118 resubcld ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
218 217 recnd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
219 216 218 addcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐷 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐷 + 𝐵 ) ) )
220 215 219 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐷 ) + ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐷 + 𝐵 ) ) )
221 218 29 131 addassd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( 𝐴 − 𝐵 ) + 𝐷 ) + 𝐵 ) = ( ( 𝐴 − 𝐵 ) + ( 𝐷 + 𝐵 ) ) )
222 221 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 − 𝐵 ) + ( 𝐷 + 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) + 𝐷 ) + 𝐵 ) )
223 220 222 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐷 ) + ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) + 𝐷 ) + 𝐵 ) )
224 24 131 29 nppcand ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( 𝐴 − 𝐵 ) + 𝐷 ) + 𝐵 ) = ( 𝐴 + 𝐷 ) )
225 223 224 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐷 ) = ( ( 𝐵 + 𝐷 ) + ( 𝐴 − 𝐵 ) ) )
226 132 218 addcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) + ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐵 + 𝐶 ) ) )
227 131 26 addcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐶 ) = ( 𝐶 + 𝐵 ) )
228 227 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 − 𝐵 ) + ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐶 + 𝐵 ) ) )
229 226 228 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) + ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐶 + 𝐵 ) ) )
230 218 26 131 addassd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) + 𝐵 ) = ( ( 𝐴 − 𝐵 ) + ( 𝐶 + 𝐵 ) ) )
231 230 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 − 𝐵 ) + ( 𝐶 + 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) + 𝐵 ) )
232 229 231 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) + ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) + 𝐵 ) )
233 24 131 26 nppcand ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) + 𝐵 ) = ( 𝐴 + 𝐶 ) )
234 232 233 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐶 ) = ( ( 𝐵 + 𝐶 ) + ( 𝐴 − 𝐵 ) ) )
235 213 225 234 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐷 ) + ( 𝐴 − 𝐵 ) ) ≤ ( ( 𝐵 + 𝐶 ) + ( 𝐴 − 𝐵 ) ) )
236 139 zred ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
237 143 236 217 leadd1d ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) ↔ ( ( 𝐵 + 𝐷 ) + ( 𝐴 − 𝐵 ) ) ≤ ( ( 𝐵 + 𝐶 ) + ( 𝐴 − 𝐵 ) ) ) )
238 235 237 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) )
239 56 139 142 145 238 elfzd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) )
240 bcval2 ⊢ ( ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) → ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) = ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) · ( ! ‘ ( 𝐵 + 𝐷 ) ) ) ) )
241 239 240 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) = ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) · ( ! ‘ ( 𝐵 + 𝐷 ) ) ) ) )
242 241 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐵 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐵 + 𝐶 ) − ( 𝐵 + 𝐷 ) ) ) · ( ! ‘ ( 𝐵 + 𝐷 ) ) ) ) = ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )
243 211 242 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( ! ‘ ( 𝐴 + 𝐶 ) ) / ( ( ! ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 + 𝐷 ) ) ) · ( ! ‘ ( 𝐴 + 𝐷 ) ) ) ) ≤ ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )
244 8 243 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) C ( 𝐴 + 𝐷 ) ) ≤ ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )
245 9 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐶 ) ∈ ℕ0 )
246 14 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐴 + 𝐷 ) ∈ ℤ )
247 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) )
248 bcval3 ⊢ ( ( ( 𝐴 + 𝐶 ) ∈ ℕ0 ∧ ( 𝐴 + 𝐷 ) ∈ ℤ ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) C ( 𝐴 + 𝐷 ) ) = 0 )
249 245 246 247 248 syl3anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) C ( 𝐴 + 𝐷 ) ) = 0 )
250 bccl2 ⊢ ( ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) → ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) ∈ ℕ )
251 250 adantl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) ∈ ℕ )
252 251 nnnn0d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) ∈ ℕ0 )
253 252 nn0ge0d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → 0 ≤ ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )
254 0le0 ⊢ 0 ≤ 0
255 254 a1i ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → 0 ≤ 0 )
256 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → 𝐵 ∈ ℕ0 )
257 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → 𝐶 ∈ ℕ0 )
258 256 257 nn0addcld ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → ( 𝐵 + 𝐶 ) ∈ ℕ0 )
259 141 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( 𝐵 + 𝐷 ) ∈ ℤ )
260 259 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → ( 𝐵 + 𝐷 ) ∈ ℤ )
261 simpr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) )
262 bcval3 ⊢ ( ( ( 𝐵 + 𝐶 ) ∈ ℕ0 ∧ ( 𝐵 + 𝐷 ) ∈ ℤ ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) = 0 )
263 258 260 261 262 syl3anc ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) = 0 )
264 263 eqcomd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → 0 = ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )
265 255 264 breqtrd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) ∧ ¬ ( 𝐵 + 𝐷 ) ∈ ( 0 ... ( 𝐵 + 𝐶 ) ) ) → 0 ≤ ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )
266 253 265 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → 0 ≤ ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )
267 249 266 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 + 𝐷 ) ∈ ( 0 ... ( 𝐴 + 𝐶 ) ) ) → ( ( 𝐴 + 𝐶 ) C ( 𝐴 + 𝐷 ) ) ≤ ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )
268 244 267 pm2.61dan ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) C ( 𝐴 + 𝐷 ) ) ≤ ( ( 𝐵 + 𝐶 ) C ( 𝐵 + 𝐷 ) ) )