Metamath Proof Explorer

Theorem lcmineqlem21

Description: The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024)

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

Proof

Step Hyp Ref Expression
1 lcmineqlem21.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 lcmineqlem21.2 ⊢ ( 𝜑 → 4 ≤ 𝑁 )
3 2nn0 ⊢ 2 ∈ ℕ0
4 3 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
5 4 nn0red ⊢ ( 𝜑 → 2 ∈ ℝ )
6 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7 4 6 nn0mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
8 7 4 nn0addcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℕ0 )
9 5 8 reexpcld ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ∈ ℝ )
10 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
11 2rp ⊢ 2 ∈ ℝ+
12 11 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
13 2z ⊢ 2 ∈ ℤ
14 13 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
15 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16 14 15 zmulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
17 12 16 rpexpcld ⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ+ )
18 17 rpred ⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
19 10 18 remulcld ⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ∈ ℝ )
20 fz1ssnn ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ
21 fzfi ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin
22 lcmfnncl ⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
23 20 21 22 mp2an ⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ
24 23 a1i ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
25 24 nnred ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
26 4re ⊢ 4 ∈ ℝ
27 26 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
28 27 10 17 lemul1d ⊢ ( 𝜑 → ( 4 ≤ 𝑁 ↔ ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ) )
29 2 28 mpbid ⊢ ( 𝜑 → ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) )
30 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
31 30 4 7 expaddd ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) = ( ( 2 ↑ ( 2 · 𝑁 ) ) · ( 2 ↑ 2 ) ) )
32 sq2 ⊢ ( 2 ↑ 2 ) = 4
33 32 oveq2i ⊢ ( ( 2 ↑ ( 2 · 𝑁 ) ) · ( 2 ↑ 2 ) ) = ( ( 2 ↑ ( 2 · 𝑁 ) ) · 4 )
34 31 33 eqtrdi ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) = ( ( 2 ↑ ( 2 · 𝑁 ) ) · 4 ) )
35 17 rpcnd ⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℂ )
36 27 recnd ⊢ ( 𝜑 → 4 ∈ ℂ )
37 35 36 mulcomd ⊢ ( 𝜑 → ( ( 2 ↑ ( 2 · 𝑁 ) ) · 4 ) = ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) )
38 34 37 eqtrd ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) = ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) )
39 38 breq1d ⊢ ( 𝜑 → ( ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ↔ ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ) )
40 29 39 mpbird ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) )
41 1 lcmineqlem20 ⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
42 9 19 25 40 41 letrd ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )