Metamath Proof Explorer

Theorem bcled

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

Ref Expression
Hypotheses bcled.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
bcled.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
bcled.3 ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
bcled.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
Assertion bcled ( 𝜑 → ( 𝐴 C 𝐶 ) ≤ ( 𝐵 C 𝐶 ) )

Proof

Step Hyp Ref Expression
1 bcled.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
2 bcled.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
3 bcled.3 ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
4 bcled.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 bcval2 ⊢ ( 𝐶 ∈ ( 0 ... 𝐴 ) → ( 𝐴 C 𝐶 ) = ( ( ! ‘ 𝐴 ) / ( ( ! ‘ ( 𝐴 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 C 𝐶 ) = ( ( ! ‘ 𝐴 ) / ( ( ! ‘ ( 𝐴 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℕ0 )
8 7 faccld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℕ )
9 8 nncnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℂ )
10 7 nn0zd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℤ )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ℤ )
12 10 11 zsubcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 𝐶 ) ∈ ℤ )
13 11 zred ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ℝ )
14 7 nn0red ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℝ )
15 0red ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ∈ ℝ )
16 elfzle2 ⊢ ( 𝐶 ∈ ( 0 ... 𝐴 ) → 𝐶 ≤ 𝐴 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ≤ 𝐴 )
18 14 recnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℂ )
19 18 subid1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 0 ) = 𝐴 )
20 19 eqcomd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 = ( 𝐴 − 0 ) )
21 17 20 breqtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ≤ ( 𝐴 − 0 ) )
22 13 14 15 21 lesubd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ≤ ( 𝐴 − 𝐶 ) )
23 12 22 jca ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝐴 − 𝐶 ) ∈ ℤ ∧ 0 ≤ ( 𝐴 − 𝐶 ) ) )
24 elnn0z ⊢ ( ( 𝐴 − 𝐶 ) ∈ ℕ0 ↔ ( ( 𝐴 − 𝐶 ) ∈ ℤ ∧ 0 ≤ ( 𝐴 − 𝐶 ) ) )
25 23 24 sylibr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 𝐶 ) ∈ ℕ0 )
26 25 faccld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ ( 𝐴 − 𝐶 ) ) ∈ ℕ )
27 26 nncnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ ( 𝐴 − 𝐶 ) ) ∈ ℂ )
28 elfznn0 ⊢ ( 𝐶 ∈ ( 0 ... 𝐴 ) → 𝐶 ∈ ℕ0 )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ℕ0 )
30 29 faccld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐶 ) ∈ ℕ )
31 30 nncnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐶 ) ∈ ℂ )
32 26 nnne0d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ ( 𝐴 − 𝐶 ) ) ≠ 0 )
33 30 nnne0d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐶 ) ≠ 0 )
34 9 27 31 32 33 divdiv1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝐶 ) ) ) / ( ! ‘ 𝐶 ) ) = ( ( ! ‘ 𝐴 ) / ( ( ! ‘ ( 𝐴 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) / ( ( ! ‘ ( 𝐴 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) = ( ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝐶 ) ) ) / ( ! ‘ 𝐶 ) ) )
36 8 nnred ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℝ )
37 26 nnred ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
38 36 37 32 redivcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝐶 ) ) ) ∈ ℝ )
39 2 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℕ0 )
40 39 faccld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐵 ) ∈ ℕ )
41 40 nnred ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐵 ) ∈ ℝ )
42 39 nn0zd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℤ )
43 42 11 zsubcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
44 39 nn0red ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℝ )
45 4 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ≤ 𝐵 )
46 13 14 44 17 45 letrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ≤ 𝐵 )
47 44 recnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℂ )
48 47 subid1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − 0 ) = 𝐵 )
49 48 eqcomd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 = ( 𝐵 − 0 ) )
50 46 49 breqtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ≤ ( 𝐵 − 0 ) )
51 13 44 15 50 lesubd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ≤ ( 𝐵 − 𝐶 ) )
52 43 51 jca ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝐵 − 𝐶 ) ∈ ℤ ∧ 0 ≤ ( 𝐵 − 𝐶 ) ) )
53 elnn0z ⊢ ( ( 𝐵 − 𝐶 ) ∈ ℕ0 ↔ ( ( 𝐵 − 𝐶 ) ∈ ℤ ∧ 0 ≤ ( 𝐵 − 𝐶 ) ) )
54 52 53 sylibr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − 𝐶 ) ∈ ℕ0 )
55 54 faccld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ ( 𝐵 − 𝐶 ) ) ∈ ℕ )
56 55 nnred ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
57 55 nnne0d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ ( 𝐵 − 𝐶 ) ) ≠ 0 )
58 41 56 57 redivcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ! ‘ 𝐵 ) / ( ! ‘ ( 𝐵 − 𝐶 ) ) ) ∈ ℝ )
59 30 nnrpd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐶 ) ∈ ℝ+ )
60 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) )
61 fzfid ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 0 ... ( 𝐶 − 1 ) ) ∈ Fin )
62 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝐴 ∈ ℝ )
63 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) → 𝑘 ∈ ℤ )
64 63 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝑘 ∈ ℤ )
65 64 zred ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝑘 ∈ ℝ )
66 62 65 resubcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → ( 𝐴 − 𝑘 ) ∈ ℝ )
67 0red ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 0 ∈ ℝ )
68 29 nn0red ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ℝ )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝐶 ∈ ℝ )
70 1red ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 1 ∈ ℝ )
71 69 70 resubcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → ( 𝐶 − 1 ) ∈ ℝ )
72 62 67 resubcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → ( 𝐴 − 0 ) ∈ ℝ )
73 elfzle2 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) → 𝑘 ≤ ( 𝐶 − 1 ) )
74 73 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝑘 ≤ ( 𝐶 − 1 ) )
75 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝐶 ≤ 𝐴 )
76 0le1 ⊢ 0 ≤ 1
77 76 a1i ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 0 ≤ 1 )
78 69 67 62 70 75 77 le2subd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → ( 𝐶 − 1 ) ≤ ( 𝐴 − 0 ) )
79 65 71 72 74 78 letrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝑘 ≤ ( 𝐴 − 0 ) )
80 65 62 67 79 lesubd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 0 ≤ ( 𝐴 − 𝑘 ) )
81 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝐵 ∈ ℝ )
82 81 65 resubcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → ( 𝐵 − 𝑘 ) ∈ ℝ )
83 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → 𝐴 ≤ 𝐵 )
84 62 81 65 83 lesub1dd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ) → ( 𝐴 − 𝑘 ) ≤ ( 𝐵 − 𝑘 ) )
85 60 61 66 80 82 84 fprodle ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ∏ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ( 𝐴 − 𝑘 ) ≤ ∏ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ( 𝐵 − 𝑘 ) )
86 7 nn0cnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℂ )
87 fallfacval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 FallFac 𝐶 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ( 𝐴 − 𝑘 ) )
88 86 29 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 FallFac 𝐶 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ( 𝐴 − 𝑘 ) )
89 88 eqcomd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ∏ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ( 𝐴 − 𝑘 ) = ( 𝐴 FallFac 𝐶 ) )
90 39 nn0cnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℂ )
91 fallfacval ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐵 FallFac 𝐶 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ( 𝐵 − 𝑘 ) )
92 90 29 91 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 FallFac 𝐶 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ( 𝐵 − 𝑘 ) )
93 92 eqcomd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ∏ 𝑘 ∈ ( 0 ... ( 𝐶 − 1 ) ) ( 𝐵 − 𝑘 ) = ( 𝐵 FallFac 𝐶 ) )
94 85 89 93 3brtr3d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 FallFac 𝐶 ) ≤ ( 𝐵 FallFac 𝐶 ) )
95 fallfacval4 ⊢ ( 𝐶 ∈ ( 0 ... 𝐴 ) → ( 𝐴 FallFac 𝐶 ) = ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝐶 ) ) ) )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 FallFac 𝐶 ) = ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝐶 ) ) ) )
97 0zd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ∈ ℤ )
98 29 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ≤ 𝐶 )
99 68 14 44 17 45 letrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ≤ 𝐵 )
100 97 42 11 98 99 elfzd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ( 0 ... 𝐵 ) )
101 fallfacval4 ⊢ ( 𝐶 ∈ ( 0 ... 𝐵 ) → ( 𝐵 FallFac 𝐶 ) = ( ( ! ‘ 𝐵 ) / ( ! ‘ ( 𝐵 − 𝐶 ) ) ) )
102 100 101 syl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 FallFac 𝐶 ) = ( ( ! ‘ 𝐵 ) / ( ! ‘ ( 𝐵 − 𝐶 ) ) ) )
103 94 96 102 3brtr3d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝐶 ) ) ) ≤ ( ( ! ‘ 𝐵 ) / ( ! ‘ ( 𝐵 − 𝐶 ) ) ) )
104 38 58 59 103 lediv1dd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝐶 ) ) ) / ( ! ‘ 𝐶 ) ) ≤ ( ( ( ! ‘ 𝐵 ) / ( ! ‘ ( 𝐵 − 𝐶 ) ) ) / ( ! ‘ 𝐶 ) ) )
105 40 nncnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ 𝐵 ) ∈ ℂ )
106 55 nncnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ! ‘ ( 𝐵 − 𝐶 ) ) ∈ ℂ )
107 105 106 31 57 33 divdiv1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ( ! ‘ 𝐵 ) / ( ! ‘ ( 𝐵 − 𝐶 ) ) ) / ( ! ‘ 𝐶 ) ) = ( ( ! ‘ 𝐵 ) / ( ( ! ‘ ( 𝐵 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) )
108 104 107 breqtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ( ! ‘ 𝐴 ) / ( ! ‘ ( 𝐴 − 𝐶 ) ) ) / ( ! ‘ 𝐶 ) ) ≤ ( ( ! ‘ 𝐵 ) / ( ( ! ‘ ( 𝐵 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) )
109 35 108 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) / ( ( ! ‘ ( 𝐴 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) ≤ ( ( ! ‘ 𝐵 ) / ( ( ! ‘ ( 𝐵 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) )
110 2 nn0zd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℤ )
112 elfzle1 ⊢ ( 𝐶 ∈ ( 0 ... 𝐴 ) → 0 ≤ 𝐶 )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ≤ 𝐶 )
114 1 nn0red ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℝ )
116 111 zred ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℝ )
117 13 115 116 17 45 letrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ≤ 𝐵 )
118 97 111 11 113 117 elfzd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ( 0 ... 𝐵 ) )
119 bcval2 ⊢ ( 𝐶 ∈ ( 0 ... 𝐵 ) → ( 𝐵 C 𝐶 ) = ( ( ! ‘ 𝐵 ) / ( ( ! ‘ ( 𝐵 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) )
120 118 119 syl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 C 𝐶 ) = ( ( ! ‘ 𝐵 ) / ( ( ! ‘ ( 𝐵 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) )
121 120 eqcomd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ! ‘ 𝐵 ) / ( ( ! ‘ ( 𝐵 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) = ( 𝐵 C 𝐶 ) )
122 109 121 breqtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) / ( ( ! ‘ ( 𝐴 − 𝐶 ) ) · ( ! ‘ 𝐶 ) ) ) ≤ ( 𝐵 C 𝐶 ) )
123 6 122 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 C 𝐶 ) ≤ ( 𝐵 C 𝐶 ) )
124 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℕ0 )
125 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ℤ )
126 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ¬ 𝐶 ∈ ( 0 ... 𝐴 ) )
127 bcval3 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐶 ∈ ℤ ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 C 𝐶 ) = 0 )
128 124 125 126 127 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 C 𝐶 ) = 0 )
129 bccl2 ⊢ ( 𝐶 ∈ ( 0 ... 𝐵 ) → ( 𝐵 C 𝐶 ) ∈ ℕ )
130 129 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝐶 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 C 𝐶 ) ∈ ℕ )
131 130 nnnn0d ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝐶 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 C 𝐶 ) ∈ ℕ0 )
132 131 nn0ge0d ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝐶 ∈ ( 0 ... 𝐵 ) ) → 0 ≤ ( 𝐵 C 𝐶 ) )
133 0le0 ⊢ 0 ≤ 0
134 133 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... 𝐵 ) ) → 0 ≤ 0 )
135 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... 𝐵 ) ) → 𝐵 ∈ ℕ0 )
136 125 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... 𝐵 ) ) → 𝐶 ∈ ℤ )
137 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... 𝐵 ) ) → ¬ 𝐶 ∈ ( 0 ... 𝐵 ) )
138 bcval3 ⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℤ ∧ ¬ 𝐶 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 C 𝐶 ) = 0 )
139 135 136 137 138 syl3anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... 𝐵 ) ) → ( 𝐵 C 𝐶 ) = 0 )
140 139 eqcomd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... 𝐵 ) ) → 0 = ( 𝐵 C 𝐶 ) )
141 134 140 breqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... 𝐵 ) ) → 0 ≤ ( 𝐵 C 𝐶 ) )
142 132 141 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ≤ ( 𝐵 C 𝐶 ) )
143 128 142 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 C 𝐶 ) ≤ ( 𝐵 C 𝐶 ) )
144 123 143 pm2.61dan ⊢ ( 𝜑 → ( 𝐴 C 𝐶 ) ≤ ( 𝐵 C 𝐶 ) )