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