Metamath Proof Explorer


Theorem lcmineqlem21

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

Ref Expression
Hypotheses lcmineqlem21.1 φ N
lcmineqlem21.2 φ 4 N
Assertion lcmineqlem21 φ 2 2 N + 2 lcm _ 1 2 N + 1

Proof

Step Hyp Ref Expression
1 lcmineqlem21.1 φ N
2 lcmineqlem21.2 φ 4 N
3 2nn0 2 0
4 3 a1i φ 2 0
5 4 nn0red φ 2
6 1 nnnn0d φ N 0
7 4 6 nn0mulcld φ 2 N 0
8 7 4 nn0addcld φ 2 N + 2 0
9 5 8 reexpcld φ 2 2 N + 2
10 1 nnred φ N
11 2rp 2 +
12 11 a1i φ 2 +
13 2z 2
14 13 a1i φ 2
15 1 nnzd φ N
16 14 15 zmulcld φ 2 N
17 12 16 rpexpcld φ 2 2 N +
18 17 rpred φ 2 2 N
19 10 18 remulcld φ N 2 2 N
20 fz1ssnn 1 2 N + 1
21 fzfi 1 2 N + 1 Fin
22 lcmfnncl 1 2 N + 1 1 2 N + 1 Fin lcm _ 1 2 N + 1
23 20 21 22 mp2an lcm _ 1 2 N + 1
24 23 a1i φ lcm _ 1 2 N + 1
25 24 nnred φ lcm _ 1 2 N + 1
26 4re 4
27 26 a1i φ 4
28 27 10 17 lemul1d φ 4 N 4 2 2 N N 2 2 N
29 2 28 mpbid φ 4 2 2 N N 2 2 N
30 2cnd φ 2
31 30 4 7 expaddd φ 2 2 N + 2 = 2 2 N 2 2
32 sq2 2 2 = 4
33 32 oveq2i 2 2 N 2 2 = 2 2 N 4
34 31 33 eqtrdi φ 2 2 N + 2 = 2 2 N 4
35 17 rpcnd φ 2 2 N
36 27 recnd φ 4
37 35 36 mulcomd φ 2 2 N 4 = 4 2 2 N
38 34 37 eqtrd φ 2 2 N + 2 = 4 2 2 N
39 38 breq1d φ 2 2 N + 2 N 2 2 N 4 2 2 N N 2 2 N
40 29 39 mpbird φ 2 2 N + 2 N 2 2 N
41 1 lcmineqlem20 φ N 2 2 N lcm _ 1 2 N + 1
42 9 19 25 40 41 letrd φ 2 2 N + 2 lcm _ 1 2 N + 1