Metamath Proof Explorer


Theorem lcmineqlem15

Description: F times the least common multiple of 1 to n is a natural number. (Contributed by metakunt, 10-May-2024)

Ref Expression
Hypotheses lcmineqlem15.1 F=01xM11xNMdx
lcmineqlem15.2 φN
lcmineqlem15.3 φM
lcmineqlem15.4 φMN
Assertion lcmineqlem15 φlcm_1NF

Proof

Step Hyp Ref Expression
1 lcmineqlem15.1 F=01xM11xNMdx
2 lcmineqlem15.2 φN
3 lcmineqlem15.3 φM
4 lcmineqlem15.4 φMN
5 1 2 3 4 lcmineqlem6 φlcm_1NF
6 fz1ssnn 1N
7 fzfi 1NFin
8 lcmfnncl 1N1NFinlcm_1N
9 6 7 8 mp2an lcm_1N
10 9 a1i φlcm_1N
11 10 nnred φlcm_1N
12 1 3 2 4 lcmineqlem13 φF=1M(NM)
13 1red φ1
14 3 nnnn0d φM0
15 2 14 4 bccl2d φ(NM)
16 3 15 nnmulcld φM(NM)
17 16 nnred φM(NM)
18 16 nnne0d φM(NM)0
19 13 17 18 redivcld φ1M(NM)
20 12 19 eqeltrd φF
21 10 nngt0d φ0<lcm_1N
22 nnrecgt0 M(NM)0<1M(NM)
23 16 22 syl φ0<1M(NM)
24 23 12 breqtrrd φ0<F
25 11 20 21 24 mulgt0d φ0<lcm_1NF
26 elnnz lcm_1NFlcm_1NF0<lcm_1NF
27 5 25 26 sylanbrc φlcm_1NF