Theorem 7nn 12351

Description: 7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)

Assertion

Ref	Expression
7nn	⊢ 7 ∈ ℕ

Proof of Theorem 7nn

Step	Hyp	Ref	Expression
1		df-7 12327	. 2 ⊢ 7 = (6 + 1)
2		6nn 12348	. . 3 ⊢ 6 ∈ ℕ
3		peano2nn 12271	. . 3 ⊢ (6 ∈ ℕ → (6 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (6 + 1) ∈ ℕ
5	1, 4	eqeltri 2821	1 ⊢ 7 ∈ ℕ

Syntax hints:   ∈ wcel 2098  (class class class)co 7423  1c1 11155   + caddc 11157  ℕcn 12259  6c6 12318  7c7 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432  ax-un 7745  ax-1cn 11212

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7426  df-om 7876  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-nn 12260  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327

This theorem is referenced by:  8nn  12354  7nn0  12541  7prm  17108  17prm  17114  prmlem2  17117  37prm  17118  43prm  17119  83prm  17120  139prm  17121  163prm  17122  317prm  17123  631prm  17124  1259prm  17133  mcubic  26867  cubic2  26868  cubic  26869  quartlem1  26877  quartlem2  26878  log2ublem1  26966  log2ublem2  26967  log2ub  26969  lgsdir2lem3  27348  lngndx  28357  lngid  28359  slotslnbpsd  28361  lngndxnitvndx  28362  ttgvalOLD  28795  ttglemOLD  28797  eengstr  28906  ex-xp  30361  ex-mod  30374  ex-prmo  30384  hgt750lem2  34454  60gcd7e1  41652  60lcm7e420  41657  lcm7un  41666  lcmineqlem  41699  3lexlogpow5ineq2  41702  3lexlogpow2ineq1  41705  3lexlogpow2ineq2  41706  rmydioph  42609  expdiophlem2  42617  257prm  47070  fmtno5nprm  47092  139prmALT  47105  127prm  47108  8exp8mod9  47245  nnsum3primesle9  47303  bgoldbtbndlem1  47314  tgoldbach  47326