Metamath Proof Explorer

Theorem lcmineqlem19

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

Ref Expression
Hypothesis lcmineqlem19.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion lcmineqlem19 ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem19.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 2nn ⊢ 2 ∈ ℕ
3 2 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
4 3 1 nnmulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
5 4 peano2nnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
6 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
8 2re ⊢ 2 ∈ ℝ
9 8 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
10 6 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
11 3 nnge1d ⊢ ( 𝜑 → 1 ≤ 2 )
12 7 9 10 11 lemulge12d ⊢ ( 𝜑 → 𝑁 ≤ ( 2 · 𝑁 ) )
13 4 6 12 bccl2d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
14 fz1ssnn ⊢ ( 1 ... ( 2 · 𝑁 ) ) ⊆ ℕ
15 fzfi ⊢ ( 1 ... ( 2 · 𝑁 ) ) ∈ Fin
16 lcmfnncl ⊢ ( ( ( 1 ... ( 2 · 𝑁 ) ) ⊆ ℕ ∧ ( 1 ... ( 2 · 𝑁 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∈ ℕ )
17 14 15 16 mp2an ⊢ ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∈ ℕ
18 17 a1i ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∈ ℕ )
19 fz1ssnn ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ
20 fzfi ⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin
21 lcmfnncl ⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
22 19 20 21 mp2an ⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ
23 22 a1i ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
24 1 4 12 lcmineqlem16 ⊢ ( 𝜑 → ( 𝑁 · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) )
25 1 lcmineqlem18 ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )
26 1 peano2nnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
27 9 7 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
28 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
29 7 27 28 12 leadd1dd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( ( 2 · 𝑁 ) + 1 ) )
30 26 5 29 lcmineqlem16 ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) C ( 𝑁 + 1 ) ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
31 25 30 eqbrtrrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
32 18 nnzd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∈ ℤ )
33 5 nnzd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ )
34 32 33 jca ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∈ ℤ ∧ ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ ) )
35 dvdslcm ⊢ ( ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∈ ℤ ∧ ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ ) → ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) ∧ ( ( 2 · 𝑁 ) + 1 ) ∥ ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) ) )
36 34 35 syl ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) ∧ ( ( 2 · 𝑁 ) + 1 ) ∥ ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) ) )
37 36 simpld ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∥ ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) )
38 5 lcmfunnnd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) = ( ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 1 ) − 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) )
39 27 recnd ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
40 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
41 39 40 pncand ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) − 1 ) = ( 2 · 𝑁 ) )
42 41 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( ( 2 · 𝑁 ) + 1 ) − 1 ) ) = ( 1 ... ( 2 · 𝑁 ) ) )
43 42 fveq2d ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 1 ) − 1 ) ) ) = ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) )
44 43 oveq1d ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... ( ( ( 2 · 𝑁 ) + 1 ) − 1 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) = ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) )
45 38 44 eqtrd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) = ( ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) lcm ( ( 2 · 𝑁 ) + 1 ) ) )
46 37 45 breqtrrd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( 2 · 𝑁 ) ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
47 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
48 2z ⊢ 2 ∈ ℤ
49 1z ⊢ 1 ∈ ℤ
50 gcdaddm ⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑁 gcd 1 ) = ( 𝑁 gcd ( 1 + ( 2 · 𝑁 ) ) ) )
51 48 49 50 mp3an13 ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 1 ) = ( 𝑁 gcd ( 1 + ( 2 · 𝑁 ) ) ) )
52 47 51 syl ⊢ ( 𝜑 → ( 𝑁 gcd 1 ) = ( 𝑁 gcd ( 1 + ( 2 · 𝑁 ) ) ) )
53 40 39 addcomd ⊢ ( 𝜑 → ( 1 + ( 2 · 𝑁 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
54 53 oveq2d ⊢ ( 𝜑 → ( 𝑁 gcd ( 1 + ( 2 · 𝑁 ) ) ) = ( 𝑁 gcd ( ( 2 · 𝑁 ) + 1 ) ) )
55 52 54 eqtrd ⊢ ( 𝜑 → ( 𝑁 gcd 1 ) = ( 𝑁 gcd ( ( 2 · 𝑁 ) + 1 ) ) )
56 gcd1 ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 1 ) = 1 )
57 47 56 syl ⊢ ( 𝜑 → ( 𝑁 gcd 1 ) = 1 )
58 55 57 eqtr3d ⊢ ( 𝜑 → ( 𝑁 gcd ( ( 2 · 𝑁 ) + 1 ) ) = 1 )
59 1 5 13 18 23 24 31 46 58 lcmineqlem14 ⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )