| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 7nn | Structured version Visualization version GIF version | ||
| Description: 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
| Ref | Expression |
|---|---|
| 7nn | ⊢ 7 ∈ ℕ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-7 12213 | . 2 ⊢ 7 = (6 + 1) | |
| 2 | 6nn 12234 | . . 3 ⊢ 6 ∈ ℕ | |
| 3 | peano2nn 12157 | . . 3 ⊢ (6 ∈ ℕ → (6 + 1) ∈ ℕ) | |
| 4 | 2, 3 | ax-mp 5 | . 2 ⊢ (6 + 1) ∈ ℕ |
| 5 | 1, 4 | eqeltri 2832 | 1 ⊢ 7 ∈ ℕ |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2113 (class class class)co 7358 1c1 11027 + caddc 11029 ℕcn 12145 6c6 12204 7c7 12205 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 ax-un 7680 ax-1cn 11084 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7361 df-om 7809 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 |
| This theorem is referenced by: 8nn 12240 7nn0 12423 7prm 17038 17prm 17044 prmlem2 17047 37prm 17048 43prm 17049 83prm 17050 139prm 17051 163prm 17052 317prm 17053 631prm 17054 1259prm 17063 mcubic 26813 cubic2 26814 cubic 26815 quartlem1 26823 quartlem2 26824 log2ublem1 26912 log2ublem2 26913 log2ub 26915 lgsdir2lem3 27294 lngndx 28510 lngid 28512 slotslnbpsd 28514 lngndxnitvndx 28515 eengstr 29053 ex-xp 30511 ex-mod 30524 ex-prmo 30534 hgt750lem2 34809 60gcd7e1 42259 60lcm7e420 42264 lcm7un 42273 lcmineqlem 42306 3lexlogpow5ineq2 42309 3lexlogpow2ineq1 42312 3lexlogpow2ineq2 42313 7ne0 42517 rmydioph 43256 expdiophlem2 43264 257prm 47807 fmtno5nprm 47829 139prmALT 47842 127prm 47845 8exp8mod9 47982 nnsum3primesle9 48040 bgoldbtbndlem1 48051 tgoldbach 48063 |
| Copyright terms: Public domain | W3C validator |