# Metamath Proof Explorer

## Theorem ex-bc

Description: Example for df-bc . (Contributed by AV, 4-Sep-2021)

Ref Expression
Assertion ex-bc ${⊢}\left(\genfrac{}{}{0}{}{5}{3}\right)=10$

### Proof

Step Hyp Ref Expression
1 df-5 ${⊢}5=4+1$
2 1 oveq1i ${⊢}\left(\genfrac{}{}{0}{}{5}{3}\right)=\left(\genfrac{}{}{0}{}{4+1}{3}\right)$
3 4bc3eq4 ${⊢}\left(\genfrac{}{}{0}{}{4}{3}\right)=4$
4 3m1e2 ${⊢}3-1=2$
5 4 oveq2i ${⊢}\left(\genfrac{}{}{0}{}{4}{3-1}\right)=\left(\genfrac{}{}{0}{}{4}{2}\right)$
6 4bc2eq6 ${⊢}\left(\genfrac{}{}{0}{}{4}{2}\right)=6$
7 5 6 eqtri ${⊢}\left(\genfrac{}{}{0}{}{4}{3-1}\right)=6$
8 3 7 oveq12i ${⊢}\left(\genfrac{}{}{0}{}{4}{3}\right)+\left(\genfrac{}{}{0}{}{4}{3-1}\right)=4+6$
9 4nn0 ${⊢}4\in {ℕ}_{0}$
10 3z ${⊢}3\in ℤ$
11 bcpasc ${⊢}\left(4\in {ℕ}_{0}\wedge 3\in ℤ\right)\to \left(\genfrac{}{}{0}{}{4}{3}\right)+\left(\genfrac{}{}{0}{}{4}{3-1}\right)=\left(\genfrac{}{}{0}{}{4+1}{3}\right)$
12 9 10 11 mp2an ${⊢}\left(\genfrac{}{}{0}{}{4}{3}\right)+\left(\genfrac{}{}{0}{}{4}{3-1}\right)=\left(\genfrac{}{}{0}{}{4+1}{3}\right)$
13 6cn ${⊢}6\in ℂ$
14 4cn ${⊢}4\in ℂ$
15 6p4e10 ${⊢}6+4=10$
16 13 14 15 addcomli ${⊢}4+6=10$
17 8 12 16 3eqtr3i ${⊢}\left(\genfrac{}{}{0}{}{4+1}{3}\right)=10$
18 2 17 eqtri ${⊢}\left(\genfrac{}{}{0}{}{5}{3}\right)=10$