Metamath Proof Explorer

Theorem lcmineqlem19

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

Ref Expression
Hypothesis lcmineqlem19.1 
|- ( ph -> N e. NN )
Assertion lcmineqlem19 
|- ( ph -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem19.1 
 |-  ( ph -> N e. NN )
2 2nn 
 |-  2 e. NN
3 2 a1i 
 |-  ( ph -> 2 e. NN )
4 3 1 nnmulcld 
 |-  ( ph -> ( 2 x. N ) e. NN )
5 4 peano2nnd 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. NN )
6 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
7 1 nnred 
 |-  ( ph -> N e. RR )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( ph -> 2 e. RR )
10 6 nn0ge0d 
 |-  ( ph -> 0 <_ N )
11 3 nnge1d 
 |-  ( ph -> 1 <_ 2 )
12 7 9 10 11 lemulge12d 
 |-  ( ph -> N <_ ( 2 x. N ) )
13 4 6 12 bccl2d 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. NN )
14 fz1ssnn 
 |-  ( 1 ... ( 2 x. N ) ) C_ NN
15 fzfi 
 |-  ( 1 ... ( 2 x. N ) ) e. Fin
16 lcmfnncl 
 |-  ( ( ( 1 ... ( 2 x. N ) ) C_ NN /\ ( 1 ... ( 2 x. N ) ) e. Fin ) -> ( _lcm ` ( 1 ... ( 2 x. N ) ) ) e. NN )
17 14 15 16 mp2an 
 |-  ( _lcm ` ( 1 ... ( 2 x. N ) ) ) e. NN
18 17 a1i 
 |-  ( ph -> ( _lcm ` ( 1 ... ( 2 x. N ) ) ) e. NN )
19 fz1ssnn 
 |-  ( 1 ... ( ( 2 x. N ) + 1 ) ) C_ NN
20 fzfi 
 |-  ( 1 ... ( ( 2 x. N ) + 1 ) ) e. Fin
21 lcmfnncl 
 |-  ( ( ( 1 ... ( ( 2 x. N ) + 1 ) ) C_ NN /\ ( 1 ... ( ( 2 x. N ) + 1 ) ) e. Fin ) -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN )
22 19 20 21 mp2an 
 |-  ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN
23 22 a1i 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN )
24 1 4 12 lcmineqlem16 
 |-  ( ph -> ( N x. ( ( 2 x. N ) _C N ) ) || ( _lcm ` ( 1 ... ( 2 x. N ) ) ) )
25 1 lcmineqlem18 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )
26 1 peano2nnd 
 |-  ( ph -> ( N + 1 ) e. NN )
27 9 7 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
28 1red 
 |-  ( ph -> 1 e. RR )
29 7 27 28 12 leadd1dd 
 |-  ( ph -> ( N + 1 ) <_ ( ( 2 x. N ) + 1 ) )
30 26 5 29 lcmineqlem16 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
31 25 30 eqbrtrrd 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
32 18 nnzd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( 2 x. N ) ) ) e. ZZ )
33 5 nnzd 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. ZZ )
34 32 33 jca 
 |-  ( ph -> ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) e. ZZ /\ ( ( 2 x. N ) + 1 ) e. ZZ ) )
35 dvdslcm 
 |-  ( ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) e. ZZ /\ ( ( 2 x. N ) + 1 ) e. ZZ ) -> ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) || ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) lcm ( ( 2 x. N ) + 1 ) ) /\ ( ( 2 x. N ) + 1 ) || ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) lcm ( ( 2 x. N ) + 1 ) ) ) )
36 34 35 syl 
 |-  ( ph -> ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) || ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) lcm ( ( 2 x. N ) + 1 ) ) /\ ( ( 2 x. N ) + 1 ) || ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) lcm ( ( 2 x. N ) + 1 ) ) ) )
37 36 simpld 
 |-  ( ph -> ( _lcm ` ( 1 ... ( 2 x. N ) ) ) || ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) lcm ( ( 2 x. N ) + 1 ) ) )
38 5 lcmfunnnd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) = ( ( _lcm ` ( 1 ... ( ( ( 2 x. N ) + 1 ) - 1 ) ) ) lcm ( ( 2 x. N ) + 1 ) ) )
39 27 recnd 
 |-  ( ph -> ( 2 x. N ) e. CC )
40 1cnd 
 |-  ( ph -> 1 e. CC )
41 39 40 pncand 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) - 1 ) = ( 2 x. N ) )
42 41 oveq2d 
 |-  ( ph -> ( 1 ... ( ( ( 2 x. N ) + 1 ) - 1 ) ) = ( 1 ... ( 2 x. N ) ) )
43 42 fveq2d 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( ( 2 x. N ) + 1 ) - 1 ) ) ) = ( _lcm ` ( 1 ... ( 2 x. N ) ) ) )
44 43 oveq1d 
 |-  ( ph -> ( ( _lcm ` ( 1 ... ( ( ( 2 x. N ) + 1 ) - 1 ) ) ) lcm ( ( 2 x. N ) + 1 ) ) = ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) lcm ( ( 2 x. N ) + 1 ) ) )
45 38 44 eqtrd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) = ( ( _lcm ` ( 1 ... ( 2 x. N ) ) ) lcm ( ( 2 x. N ) + 1 ) ) )
46 37 45 breqtrrd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( 2 x. N ) ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
47 1 nnzd 
 |-  ( ph -> N e. ZZ )
48 2z 
 |-  2 e. ZZ
49 1z 
 |-  1 e. ZZ
50 gcdaddm 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 1 e. ZZ ) -> ( N gcd 1 ) = ( N gcd ( 1 + ( 2 x. N ) ) ) )
51 48 49 50 mp3an13 
 |-  ( N e. ZZ -> ( N gcd 1 ) = ( N gcd ( 1 + ( 2 x. N ) ) ) )
52 47 51 syl 
 |-  ( ph -> ( N gcd 1 ) = ( N gcd ( 1 + ( 2 x. N ) ) ) )
53 40 39 addcomd 
 |-  ( ph -> ( 1 + ( 2 x. N ) ) = ( ( 2 x. N ) + 1 ) )
54 53 oveq2d 
 |-  ( ph -> ( N gcd ( 1 + ( 2 x. N ) ) ) = ( N gcd ( ( 2 x. N ) + 1 ) ) )
55 52 54 eqtrd 
 |-  ( ph -> ( N gcd 1 ) = ( N gcd ( ( 2 x. N ) + 1 ) ) )
56 gcd1 
 |-  ( N e. ZZ -> ( N gcd 1 ) = 1 )
57 47 56 syl 
 |-  ( ph -> ( N gcd 1 ) = 1 )
58 55 57 eqtr3d 
 |-  ( ph -> ( N gcd ( ( 2 x. N ) + 1 ) ) = 1 )
59 1 5 13 18 23 24 31 46 58 lcmineqlem14 
 |-  ( ph -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )