Metamath Proof Explorer

Theorem faclbnd2

Description: A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005)

Ref Expression
Assertion faclbnd2 ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) / 2 ) ≤ ( ! ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 sq2 ⊢ ( 2 ↑ 2 ) = 4
2 2t2e4 ⊢ ( 2 · 2 ) = 4
3 1 2 eqtr4i ⊢ ( 2 ↑ 2 ) = ( 2 · 2 )
4 3 oveq2i ⊢ ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 2 ) ) = ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 · 2 ) )
5 2cn ⊢ 2 ∈ ℂ
6 expp1 ⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
7 5 6 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
8 7 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 · 2 ) ) = ( ( ( 2 ↑ 𝑁 ) · 2 ) / ( 2 · 2 ) ) )
9 4 8 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 2 ) ) = ( ( ( 2 ↑ 𝑁 ) · 2 ) / ( 2 · 2 ) ) )
10 expcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
11 5 10 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℂ )
12 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
13 divmuldiv ⊢ ( ( ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ 2 ∈ ℂ ) ∧ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) ) → ( ( ( 2 ↑ 𝑁 ) / 2 ) · ( 2 / 2 ) ) = ( ( ( 2 ↑ 𝑁 ) · 2 ) / ( 2 · 2 ) ) )
14 12 12 13 mpanr12 ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( ( 2 ↑ 𝑁 ) / 2 ) · ( 2 / 2 ) ) = ( ( ( 2 ↑ 𝑁 ) · 2 ) / ( 2 · 2 ) ) )
15 11 5 14 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 ↑ 𝑁 ) / 2 ) · ( 2 / 2 ) ) = ( ( ( 2 ↑ 𝑁 ) · 2 ) / ( 2 · 2 ) ) )
16 2div2e1 ⊢ ( 2 / 2 ) = 1
17 16 oveq2i ⊢ ( ( ( 2 ↑ 𝑁 ) / 2 ) · ( 2 / 2 ) ) = ( ( ( 2 ↑ 𝑁 ) / 2 ) · 1 )
18 11 halfcld ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) / 2 ) ∈ ℂ )
19 18 mulid1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 ↑ 𝑁 ) / 2 ) · 1 ) = ( ( 2 ↑ 𝑁 ) / 2 ) )
20 17 19 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 ↑ 𝑁 ) / 2 ) · ( 2 / 2 ) ) = ( ( 2 ↑ 𝑁 ) / 2 ) )
21 9 15 20 3eqtr2rd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) / 2 ) = ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 2 ) ) )
22 2nn0 ⊢ 2 ∈ ℕ0
23 faclbnd ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 2 ↑ 2 ) · ( ! ‘ 𝑁 ) ) )
24 22 23 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 2 ↑ 2 ) · ( ! ‘ 𝑁 ) ) )
25 2re ⊢ 2 ∈ ℝ
26 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
27 reexpcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℝ )
28 25 26 27 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℝ )
29 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
30 29 nnred ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℝ )
31 4re ⊢ 4 ∈ ℝ
32 1 31 eqeltri ⊢ ( 2 ↑ 2 ) ∈ ℝ
33 4pos ⊢ 0 < 4
34 33 1 breqtrri ⊢ 0 < ( 2 ↑ 2 )
35 32 34 pm3.2i ⊢ ( ( 2 ↑ 2 ) ∈ ℝ ∧ 0 < ( 2 ↑ 2 ) )
36 ledivmul ⊢ ( ( ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℝ ∧ ( ! ‘ 𝑁 ) ∈ ℝ ∧ ( ( 2 ↑ 2 ) ∈ ℝ ∧ 0 < ( 2 ↑ 2 ) ) ) → ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 2 ) ) ≤ ( ! ‘ 𝑁 ) ↔ ( 2 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 2 ↑ 2 ) · ( ! ‘ 𝑁 ) ) ) )
37 35 36 mp3an3 ⊢ ( ( ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℝ ∧ ( ! ‘ 𝑁 ) ∈ ℝ ) → ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 2 ) ) ≤ ( ! ‘ 𝑁 ) ↔ ( 2 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 2 ↑ 2 ) · ( ! ‘ 𝑁 ) ) ) )
38 28 30 37 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 2 ) ) ≤ ( ! ‘ 𝑁 ) ↔ ( 2 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 2 ↑ 2 ) · ( ! ‘ 𝑁 ) ) ) )
39 24 38 mpbird ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 2 ) ) ≤ ( ! ‘ 𝑁 ) )
40 21 39 eqbrtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) / 2 ) ≤ ( ! ‘ 𝑁 ) )