Metamath Proof Explorer

Theorem lcmineqlem20

Description: Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypothesis lcmineqlem20.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion lcmineqlem20 ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem20.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
3 2nn0 ⊢ 2 ∈ ℕ0
4 3 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
5 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 4 5 nn0mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
7 2re ⊢ 2 ∈ ℝ
8 reexpcl ⊢ ( ( 2 ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℕ0 ) → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
9 7 8 mpan ⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
10 6 9 syl ⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
11 2 10 remulcld ⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ∈ ℝ )
12 7 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
13 12 2 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
14 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
15 13 14 readdcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
16 2nn ⊢ 2 ∈ ℕ
17 16 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
18 17 1 nnmulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
19 5 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
20 17 nnge1d ⊢ ( 𝜑 → 1 ≤ 2 )
21 2 12 19 20 lemulge12d ⊢ ( 𝜑 → 𝑁 ≤ ( 2 · 𝑁 ) )
22 18 5 21 bccl2d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
23 22 nnred ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ )
24 15 23 remulcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℝ )
25 2 24 remulcld ⊢ ( 𝜑 → ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℝ )
26 fz1ssnn ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ
27 fzfi ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin
28 lcmfnncl ⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
29 26 27 28 mp2an ⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ
30 29 a1i ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
31 30 nnred ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
32 5 lcmineqlem17 ⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )
33 1 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
34 10 24 33 lemul2d ⊢ ( 𝜑 → ( ( 2 ↑ ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ↔ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) )
35 32 34 mpbid ⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
36 2 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
37 15 recnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
38 23 recnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℂ )
39 36 37 38 mulassd ⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
40 1 lcmineqlem19 ⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
41 18 peano2nnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
42 1 41 nnmulcld ⊢ ( 𝜑 → ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
43 42 22 nnmulcld ⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ )
44 43 nnzd ⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℤ )
45 dvdsle ⊢ ( ( ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℤ ∧ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ ) → ( ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
46 44 30 45 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
47 40 46 mpd ⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
48 39 47 eqbrtrrd ⊢ ( 𝜑 → ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
49 11 25 31 35 48 letrd ⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )