![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 9p1e10 | Structured version Visualization version 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 11905 | . 2 ⊢ ;10 = (((9 + 1) · 1) + 0) | |
2 | 9nn 11537 | . . . . . 6 ⊢ 9 ∈ ℕ | |
3 | 1nn 11444 | . . . . . 6 ⊢ 1 ∈ ℕ | |
4 | nnaddcl 11455 | . . . . . 6 ⊢ ((9 ∈ ℕ ∧ 1 ∈ ℕ) → (9 + 1) ∈ ℕ) | |
5 | 2, 3, 4 | mp2an 679 | . . . . 5 ⊢ (9 + 1) ∈ ℕ |
6 | 5 | nncni 11442 | . . . 4 ⊢ (9 + 1) ∈ ℂ |
7 | 6 | mulid1i 10436 | . . 3 ⊢ ((9 + 1) · 1) = (9 + 1) |
8 | 7 | oveq1i 6980 | . 2 ⊢ (((9 + 1) · 1) + 0) = ((9 + 1) + 0) |
9 | 6 | addid1i 10619 | . 2 ⊢ ((9 + 1) + 0) = (9 + 1) |
10 | 1, 8, 9 | 3eqtrri 2801 | 1 ⊢ (9 + 1) = ;10 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ∈ wcel 2048 (class class class)co 6970 0cc0 10327 1c1 10328 + caddc 10330 · cmul 10332 ℕcn 11431 9c9 11495 ;cdc 11904 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-ov 6973 df-om 7391 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-er 8081 df-en 8299 df-dom 8300 df-sdom 8301 df-pnf 10468 df-mnf 10469 df-ltxr 10471 df-nn 11432 df-2 11496 df-3 11497 df-4 11498 df-5 11499 df-6 11500 df-7 11501 df-8 11502 df-9 11503 df-dec 11905 |
This theorem is referenced by: dfdec10 11907 10nn 11920 le9lt10 11932 decsucc 11946 5p5e10 11977 6p4e10 11978 7p3e10 11981 8p2e10 11986 9p2e11 11993 10m1e9 12002 9lt10 12037 sq10e99m1 13433 3dvds 15530 3dvdsdec 15531 3dvds2dec 15532 1259lem2 16311 1259lem3 16312 1259lem4 16313 2503lem2 16317 4001lem1 16320 4001lem2 16321 4001lem4 16323 bposlem4 25555 bposlem5 25556 dp2lt10 30295 1mhdrd 30327 hgt750lem2 31532 sqdeccom12 38552 rmydioph 38952 127prm 43071 2exp340mod341 43206 bgoldbtbndlem1 43278 |
Copyright terms: Public domain | W3C validator |