MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2expltfac Structured version   Visualization version   GIF version

Theorem 2expltfac 15972
Description: The factorial grows faster than two to the power 𝑁. (Contributed by Mario Carneiro, 15-Sep-2016.)
Assertion
Ref Expression
2expltfac (𝑁 ∈ (ℤ‘4) → (2↑𝑁) < (!‘𝑁))

Proof of Theorem 2expltfac
Dummy variables 𝑥 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6809 . . . 4 (𝑥 = 4 → (2↑𝑥) = (2↑4))
2 2exp4 15967 . . . 4 (2↑4) = 16
31, 2syl6eq 2798 . . 3 (𝑥 = 4 → (2↑𝑥) = 16)
4 fveq2 6340 . . . 4 (𝑥 = 4 → (!‘𝑥) = (!‘4))
5 fac4 13233 . . . 4 (!‘4) = 24
64, 5syl6eq 2798 . . 3 (𝑥 = 4 → (!‘𝑥) = 24)
73, 6breq12d 4805 . 2 (𝑥 = 4 → ((2↑𝑥) < (!‘𝑥) ↔ 16 < 24))
8 oveq2 6809 . . 3 (𝑥 = 𝑛 → (2↑𝑥) = (2↑𝑛))
9 fveq2 6340 . . 3 (𝑥 = 𝑛 → (!‘𝑥) = (!‘𝑛))
108, 9breq12d 4805 . 2 (𝑥 = 𝑛 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑛) < (!‘𝑛)))
11 oveq2 6809 . . 3 (𝑥 = (𝑛 + 1) → (2↑𝑥) = (2↑(𝑛 + 1)))
12 fveq2 6340 . . 3 (𝑥 = (𝑛 + 1) → (!‘𝑥) = (!‘(𝑛 + 1)))
1311, 12breq12d 4805 . 2 (𝑥 = (𝑛 + 1) → ((2↑𝑥) < (!‘𝑥) ↔ (2↑(𝑛 + 1)) < (!‘(𝑛 + 1))))
14 oveq2 6809 . . 3 (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁))
15 fveq2 6340 . . 3 (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁))
1614, 15breq12d 4805 . 2 (𝑥 = 𝑁 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑁) < (!‘𝑁)))
17 1nn0 11471 . . . 4 1 ∈ ℕ0
18 2nn0 11472 . . . 4 2 ∈ ℕ0
19 6nn0 11476 . . . 4 6 ∈ ℕ0
20 4nn0 11474 . . . 4 4 ∈ ℕ0
21 6lt10 11839 . . . 4 6 < 10
22 1lt2 11357 . . . 4 1 < 2
2317, 18, 19, 20, 21, 22decltc 11695 . . 3 16 < 24
2423a1i 11 . 2 (4 ∈ ℤ → 16 < 24)
25 2nn 11348 . . . . . . . . 9 2 ∈ ℕ
2625a1i 11 . . . . . . . 8 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℕ)
27 4nn 11350 . . . . . . . . . 10 4 ∈ ℕ
28 simpl 474 . . . . . . . . . 10 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ (ℤ‘4))
29 eluznn 11922 . . . . . . . . . 10 ((4 ∈ ℕ ∧ 𝑛 ∈ (ℤ‘4)) → 𝑛 ∈ ℕ)
3027, 28, 29sylancr 698 . . . . . . . . 9 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ)
3130nnnn0d 11514 . . . . . . . 8 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ0)
3226, 31nnexpcld 13195 . . . . . . 7 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℕ)
3332nnred 11198 . . . . . 6 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℝ)
34 2re 11253 . . . . . . 7 2 ∈ ℝ
3534a1i 11 . . . . . 6 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℝ)
3633, 35remulcld 10233 . . . . 5 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) ∈ ℝ)
3731faccld 13236 . . . . . . 7 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℕ)
3837nnred 11198 . . . . . 6 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℝ)
3938, 35remulcld 10233 . . . . 5 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ∈ ℝ)
4030nnred 11198 . . . . . . 7 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℝ)
41 1red 10218 . . . . . . 7 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ∈ ℝ)
4240, 41readdcld 10232 . . . . . 6 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (𝑛 + 1) ∈ ℝ)
4338, 42remulcld 10233 . . . . 5 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · (𝑛 + 1)) ∈ ℝ)
44 2rp 12001 . . . . . . 7 2 ∈ ℝ+
4544a1i 11 . . . . . 6 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℝ+)
46 simpr 479 . . . . . 6 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) < (!‘𝑛))
4733, 38, 45, 46ltmul1dd 12091 . . . . 5 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · 2))
4837nnnn0d 11514 . . . . . . 7 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℕ0)
4948nn0ge0d 11517 . . . . . 6 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 0 ≤ (!‘𝑛))
50 df-2 11242 . . . . . . 7 2 = (1 + 1)
5130nnge1d 11226 . . . . . . . 8 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ≤ 𝑛)
5241, 40, 41, 51leadd1dd 10804 . . . . . . 7 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (1 + 1) ≤ (𝑛 + 1))
5350, 52syl5eqbr 4827 . . . . . 6 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ≤ (𝑛 + 1))
5435, 42, 38, 49, 53lemul2ad 11127 . . . . 5 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ≤ ((!‘𝑛) · (𝑛 + 1)))
5536, 39, 43, 47, 54ltletrd 10360 . . . 4 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · (𝑛 + 1)))
56 2cnd 11256 . . . . 5 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℂ)
5756, 31expp1d 13174 . . . 4 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) = ((2↑𝑛) · 2))
58 facp1 13230 . . . . 5 (𝑛 ∈ ℕ0 → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1)))
5931, 58syl 17 . . . 4 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1)))
6055, 57, 593brtr4d 4824 . . 3 ((𝑛 ∈ (ℤ‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))
6160ex 449 . 2 (𝑛 ∈ (ℤ‘4) → ((2↑𝑛) < (!‘𝑛) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1))))
627, 10, 13, 16, 24, 61uzind4 11910 1 (𝑁 ∈ (ℤ‘4) → (2↑𝑁) < (!‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1620  wcel 2127   class class class wbr 4792  cfv 6037  (class class class)co 6801  cr 10098  1c1 10100   + caddc 10102   · cmul 10104   < clt 10237  cle 10238  cn 11183  2c2 11233  4c4 11235  6c6 11237  0cn0 11455  cz 11540  cdc 11656  cuz 11850  +crp 11996  cexp 13025  !cfa 13225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-cnex 10155  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175  ax-pre-mulgt0 10176
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-om 7219  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-er 7899  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10239  df-mnf 10240  df-xr 10241  df-ltxr 10242  df-le 10243  df-sub 10431  df-neg 10432  df-nn 11184  df-2 11242  df-3 11243  df-4 11244  df-5 11245  df-6 11246  df-7 11247  df-8 11248  df-9 11249  df-n0 11456  df-z 11541  df-dec 11657  df-uz 11851  df-rp 11997  df-seq 12967  df-exp 13026  df-fac 13226
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator