Metamath Proof Explorer

Theorem 2expltfac

Description: The factorial grows faster than two to the power N . (Contributed by Mario Carneiro, 15-Sep-2016)

Ref Expression
Assertion 2expltfac ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 ↑ 𝑁 ) < ( ! ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 4 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 4 ) )
2 2exp4 ⊢ ( 2 ↑ 4 ) = 1 6
3 1 2 eqtrdi ⊢ ( 𝑥 = 4 → ( 2 ↑ 𝑥 ) = 1 6 )
4 fveq2 ⊢ ( 𝑥 = 4 → ( ! ‘ 𝑥 ) = ( ! ‘ 4 ) )
5 fac4 ⊢ ( ! ‘ 4 ) = 2 4
6 4 5 eqtrdi ⊢ ( 𝑥 = 4 → ( ! ‘ 𝑥 ) = 2 4 )
7 3 6 breq12d ⊢ ( 𝑥 = 4 → ( ( 2 ↑ 𝑥 ) < ( ! ‘ 𝑥 ) ↔ 1 6 < 2 4 ) )
8 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑛 ) )
9 fveq2 ⊢ ( 𝑥 = 𝑛 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑛 ) )
10 8 9 breq12d ⊢ ( 𝑥 = 𝑛 → ( ( 2 ↑ 𝑥 ) < ( ! ‘ 𝑥 ) ↔ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) )
11 oveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 2 ↑ 𝑥 ) = ( 2 ↑ ( 𝑛 + 1 ) ) )
12 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ! ‘ 𝑥 ) = ( ! ‘ ( 𝑛 + 1 ) ) )
13 11 12 breq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 2 ↑ 𝑥 ) < ( ! ‘ 𝑥 ) ↔ ( 2 ↑ ( 𝑛 + 1 ) ) < ( ! ‘ ( 𝑛 + 1 ) ) ) )
14 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑁 ) )
15 fveq2 ⊢ ( 𝑥 = 𝑁 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑁 ) )
16 14 15 breq12d ⊢ ( 𝑥 = 𝑁 → ( ( 2 ↑ 𝑥 ) < ( ! ‘ 𝑥 ) ↔ ( 2 ↑ 𝑁 ) < ( ! ‘ 𝑁 ) ) )
17 1nn0 ⊢ 1 ∈ ℕ0
18 2nn0 ⊢ 2 ∈ ℕ0
19 6nn0 ⊢ 6 ∈ ℕ0
20 4nn0 ⊢ 4 ∈ ℕ0
21 6lt10 ⊢ 6 < 1 0
22 1lt2 ⊢ 1 < 2
23 17 18 19 20 21 22 decltc ⊢ 1 6 < 2 4
24 2nn ⊢ 2 ∈ ℕ
25 24 a1i ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 2 ∈ ℕ )
26 4nn ⊢ 4 ∈ ℕ
27 simpl ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 4 ) )
28 eluznn ⊢ ( ( 4 ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑛 ∈ ℕ )
29 26 27 28 sylancr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 𝑛 ∈ ℕ )
30 29 nnnn0d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 𝑛 ∈ ℕ0 )
31 25 30 nnexpcld ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
32 31 nnred ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
33 2re ⊢ 2 ∈ ℝ
34 33 a1i ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 2 ∈ ℝ )
35 32 34 remulcld ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ( 2 ↑ 𝑛 ) · 2 ) ∈ ℝ )
36 30 faccld ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ! ‘ 𝑛 ) ∈ ℕ )
37 36 nnred ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ! ‘ 𝑛 ) ∈ ℝ )
38 37 34 remulcld ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ( ! ‘ 𝑛 ) · 2 ) ∈ ℝ )
39 29 nnred ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 𝑛 ∈ ℝ )
40 1red ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 1 ∈ ℝ )
41 39 40 readdcld ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( 𝑛 + 1 ) ∈ ℝ )
42 37 41 remulcld ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ( ! ‘ 𝑛 ) · ( 𝑛 + 1 ) ) ∈ ℝ )
43 2rp ⊢ 2 ∈ ℝ+
44 43 a1i ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 2 ∈ ℝ+ )
45 simpr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) )
46 32 37 44 45 ltmul1dd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ( 2 ↑ 𝑛 ) · 2 ) < ( ( ! ‘ 𝑛 ) · 2 ) )
47 36 nnnn0d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ! ‘ 𝑛 ) ∈ ℕ0 )
48 47 nn0ge0d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 0 ≤ ( ! ‘ 𝑛 ) )
49 df-2 ⊢ 2 = ( 1 + 1 )
50 29 nnge1d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 1 ≤ 𝑛 )
51 40 39 40 50 leadd1dd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( 1 + 1 ) ≤ ( 𝑛 + 1 ) )
52 49 51 eqbrtrid ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 2 ≤ ( 𝑛 + 1 ) )
53 34 41 37 48 52 lemul2ad ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ( ! ‘ 𝑛 ) · 2 ) ≤ ( ( ! ‘ 𝑛 ) · ( 𝑛 + 1 ) ) )
54 35 38 42 46 53 ltletrd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ( 2 ↑ 𝑛 ) · 2 ) < ( ( ! ‘ 𝑛 ) · ( 𝑛 + 1 ) ) )
55 2cnd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → 2 ∈ ℂ )
56 55 30 expp1d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( 2 ↑ ( 𝑛 + 1 ) ) = ( ( 2 ↑ 𝑛 ) · 2 ) )
57 facp1 ⊢ ( 𝑛 ∈ ℕ0 → ( ! ‘ ( 𝑛 + 1 ) ) = ( ( ! ‘ 𝑛 ) · ( 𝑛 + 1 ) ) )
58 30 57 syl ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( ! ‘ ( 𝑛 + 1 ) ) = ( ( ! ‘ 𝑛 ) · ( 𝑛 + 1 ) ) )
59 54 56 58 3brtr4d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) ) → ( 2 ↑ ( 𝑛 + 1 ) ) < ( ! ‘ ( 𝑛 + 1 ) ) )
60 59 ex ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) → ( ( 2 ↑ 𝑛 ) < ( ! ‘ 𝑛 ) → ( 2 ↑ ( 𝑛 + 1 ) ) < ( ! ‘ ( 𝑛 + 1 ) ) ) )
61 7 10 13 16 23 60 uzind4i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 ↑ 𝑁 ) < ( ! ‘ 𝑁 ) )