Theorem 9re 12367

Description: The number 9 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
9re	⊢ 9 ∈ ℝ

Proof of Theorem 9re

Step	Hyp	Ref	Expression
1		df-9 12337	. 2 ⊢ 9 = (8 + 1)
2		8re 12364	. . 3 ⊢ 8 ∈ ℝ
3		1re 11235	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11251	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2856	1 ⊢ 9 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℝcr 11126  1c1 11128   + caddc 11130  8c8 12328  9c9 12329

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337

This theorem is used by:  7lt9  12470  6lt9  12471  5lt9  12472  4lt9  12473  3lt9  12474  2lt9  12475  1lt9  12476  10re  12762  9lt10  12876  8lt10  12877  7lt10  12878  6lt10  12879  5lt10  12880  4lt10  12881  3lt10  12882  2lt10  12883  1lt10  12884  0.999...  15973  cos2bnd  16279  sincos2sgn  16285  slotsdifplendx  17463  dsndxntsetndx  17481  unifndxntsetndx  17488  2logb9irr  27035  sqrt2cxp2logb9e3  27039  log2tlbnd  27185  bposlem4  27526  bposlem5  27527  bposlem7  27529  bposlem8  27530  bposlem9  27531  ex-fv  30926  dp2lt10  33332  hgt750lem  35162  hgt750lem2  35163  hgt750leme  35169  problem5  36251  60gcd7e1  42874  lcmineqlem23  42920  3lexlogpow5ineq1  42923  3lexlogpow5ineq2  42924  3lexlogpow5ineq4  42925  3lexlogpow5ineq3  42926  3lexlogpow2ineq2  42928  3lexlogpow5ineq5  42929  aks4d1lem1  42931  aks4d1p1  42945  aks4d1p6  42950  aks4d1p7d1  42951  aks4d1p7  42952  aks4d1p8  42956  9rp  43182  31prm  48503  2exp340mod341  48652  341fppr2  48653  9fppr8  48656  nfermltl8rev  48661  nfermltl2rev  48662  wtgoldbnnsum4prm  48721  bgoldbnnsum3prm  48723  bgoldbtbndlem1  48724  ackval42  49629