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 φ N
lcmineqlem22.2 φ 4 N
Assertion lcmineqlem22 φ 2 2 N + 1 lcm _ 1 2 N + 1 2 2 N + 2 lcm _ 1 2 N + 2

Proof

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