Metamath Proof Explorer

Theorem lcmineqlem22

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

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

Proof

Step Hyp Ref Expression
1 lcmineqlem22.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 lcmineqlem22.2 ⊢ ( 𝜑 → 4 ≤ 𝑁 )
3 2re ⊢ 2 ∈ ℝ
4 3 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
5 2nn0 ⊢ 2 ∈ ℕ0
6 5 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
7 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
8 6 7 nn0mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
9 1nn0 ⊢ 1 ∈ ℕ0
10 9 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
11 8 10 nn0addcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ0 )
12 4 11 reexpcld ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
13 8 6 nn0addcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℕ0 )
14 4 13 reexpcld ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ∈ ℝ )
15 fz1ssnn ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ
16 fzfi ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin
17 lcmfnncl ⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
18 15 16 17 mp2an ⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ
19 18 a1i ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
20 19 nnred ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
21 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
22 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
23 4 22 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
24 1lt2 ⊢ 1 < 2
25 24 a1i ⊢ ( 𝜑 → 1 < 2 )
26 21 4 25 ltled ⊢ ( 𝜑 → 1 ≤ 2 )
27 21 4 23 26 leadd2dd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑁 ) + 2 ) )
28 2z ⊢ 2 ∈ ℤ
29 28 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
30 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
31 29 30 zmulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
32 31 peano2zd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ )
33 31 29 zaddcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℤ )
34 4 32 33 25 leexp2d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑁 ) + 2 ) ↔ ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ) )
35 27 34 mpbid ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) )
36 1 2 lcmineqlem21 ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
37 12 14 20 35 36 letrd ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
38 fz1ssnn ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ⊆ ℕ
39 fzfi ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ∈ Fin
40 lcmfnncl ⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ )
41 38 39 40 mp2an ⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ
42 41 a1i ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ )
43 42 nnred ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℝ )
44 19 nnzd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ )
45 44 33 jca ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ ∧ ( ( 2 · 𝑁 ) + 2 ) ∈ ℤ ) )
46 dvdslcm ⊢ ( ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ ∧ ( ( 2 · 𝑁 ) + 2 ) ∈ ℤ ) → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) ∧ ( ( 2 · 𝑁 ) + 2 ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) ) )
47 45 46 syl ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) ∧ ( ( 2 · 𝑁 ) + 2 ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) ) )
48 47 simpld ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) )
49 2nn ⊢ 2 ∈ ℕ
50 49 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
51 50 1 nnmulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
52 51 50 nnaddcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℕ )
53 52 lcmfunnnd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) = ( ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) )
54 23 recnd ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
55 4 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
56 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
57 54 55 56 addsubassd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) = ( ( 2 · 𝑁 ) + ( 2 − 1 ) ) )
58 2m1e1 ⊢ ( 2 − 1 ) = 1
59 58 oveq2i ⊢ ( ( 2 · 𝑁 ) + ( 2 − 1 ) ) = ( ( 2 · 𝑁 ) + 1 )
60 57 59 eqtrdi ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) = ( ( 2 · 𝑁 ) + 1 ) )
61 60 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) ) = ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) )
62 61 fveq2d ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) ) ) = ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
63 62 oveq1d ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 2 ) − 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) = ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) )
64 53 63 eqtrd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) = ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 2 ) ) )
65 48 64 breqtrrd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) )
66 44 42 jca ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ ∧ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ ) )
67 dvdsle ⊢ ( ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℤ ∧ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ∈ ℕ ) → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ) )
68 66 67 syl ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ) )
69 65 68 mpd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) )
70 14 20 43 36 69 letrd ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) )
71 37 70 jca ⊢ ( 𝜑 → ( ( 2 ↑ ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∧ ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 2 ) ) ) ) )