**Description:** 2 - 1 = 1. The result is on the right-hand-side to be consistent with
similar proofs like 4p4e8 . (Contributed by David A. Wheeler, 4-Jan-2017)

Ref | Expression | ||
---|---|---|---|

Assertion | 2m1e1 | ⊢ ( 2 − 1 ) = 1 |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | 2cn | ⊢ 2 ∈ ℂ | |

2 | ax-1cn | ⊢ 1 ∈ ℂ | |

3 | 1p1e2 | ⊢ ( 1 + 1 ) = 2 | |

4 | 1 2 2 3 | subaddrii | ⊢ ( 2 − 1 ) = 1 |