| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 9p1e10 | GIF version | ||
| Description: 9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 1-Aug-2021.) |
| Ref | Expression |
|---|---|
| 9p1e10 | ⊢ (9 + 1) = ;10 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-dec 9487 | . 2 ⊢ ;10 = (((9 + 1) · 1) + 0) | |
| 2 | 9nn 9187 | . . . . . 6 ⊢ 9 ∈ ℕ | |
| 3 | 1nn 9029 | . . . . . 6 ⊢ 1 ∈ ℕ | |
| 4 | nnaddcl 9038 | . . . . . 6 ⊢ ((9 ∈ ℕ ∧ 1 ∈ ℕ) → (9 + 1) ∈ ℕ) | |
| 5 | 2, 3, 4 | mp2an 426 | . . . . 5 ⊢ (9 + 1) ∈ ℕ |
| 6 | 5 | nncni 9028 | . . . 4 ⊢ (9 + 1) ∈ ℂ |
| 7 | 6 | mulridi 8056 | . . 3 ⊢ ((9 + 1) · 1) = (9 + 1) |
| 8 | 7 | oveq1i 5944 | . 2 ⊢ (((9 + 1) · 1) + 0) = ((9 + 1) + 0) |
| 9 | 6 | addridi 8196 | . 2 ⊢ ((9 + 1) + 0) = (9 + 1) |
| 10 | 1, 8, 9 | 3eqtrri 2230 | 1 ⊢ (9 + 1) = ;10 |
| Colors of variables: wff set class |
| Syntax hints: = wceq 1372 ∈ wcel 2175 (class class class)co 5934 0cc0 7907 1c1 7908 + caddc 7910 · cmul 7912 ℕcn 9018 9c9 9076 ;cdc 9486 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 ax-sep 4161 ax-cnex 7998 ax-resscn 7999 ax-1cn 8000 ax-1re 8001 ax-icn 8002 ax-addcl 8003 ax-addrcl 8004 ax-mulcl 8005 ax-mulcom 8008 ax-addass 8009 ax-mulass 8010 ax-distr 8011 ax-1rid 8014 ax-0id 8015 ax-cnre 8018 |
| This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ral 2488 df-rex 2489 df-rab 2492 df-v 2773 df-un 3169 df-in 3171 df-ss 3178 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-br 4044 df-iota 5229 df-fv 5276 df-ov 5937 df-inn 9019 df-2 9077 df-3 9078 df-4 9079 df-5 9080 df-6 9081 df-7 9082 df-8 9083 df-9 9084 df-dec 9487 |
| This theorem is referenced by: dfdec10 9489 10nn 9501 le9lt10 9512 decsucc 9526 5p5e10 9556 6p4e10 9557 7p3e10 9560 8p2e10 9565 9p2e11 9572 10m1e9 9581 9lt10 9616 sq10e99m1 10839 3dvds 12094 3dvdsdec 12095 3dvds2dec 12096 |
| Copyright terms: Public domain | W3C validator |