Metamath Proof Explorer


Theorem lcmineqlem20

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

Ref Expression
Hypothesis lcmineqlem20.1 φ N
Assertion lcmineqlem20 φ N 2 2 N lcm _ 1 2 N + 1

Proof

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