Metamath Proof Explorer


Theorem lcmineqlem16

Description: Technical divisibility lemma. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem16.1 φ M
lcmineqlem16.2 φ N
lcmineqlem16.3 φ M N
Assertion lcmineqlem16 φ M ( N M) lcm _ 1 N

Proof

Step Hyp Ref Expression
1 lcmineqlem16.1 φ M
2 lcmineqlem16.2 φ N
3 lcmineqlem16.3 φ M N
4 fz1ssnn 1 N
5 fzfi 1 N Fin
6 lcmfnncl 1 N 1 N Fin lcm _ 1 N
7 4 5 6 mp2an lcm _ 1 N
8 7 a1i φ lcm _ 1 N
9 8 nncnd φ lcm _ 1 N
10 1 nncnd φ M
11 1 nnnn0d φ M 0
12 2 11 3 bccl2d φ ( N M)
13 12 nncnd φ ( N M)
14 10 13 mulcld φ M ( N M)
15 1 nnne0d φ M 0
16 12 nnne0d φ ( N M) 0
17 10 13 15 16 mulne0d φ M ( N M) 0
18 9 14 17 divrecd φ lcm _ 1 N M ( N M) = lcm _ 1 N 1 M ( N M)
19 eqid 0 1 x M 1 1 x N M dx = 0 1 x M 1 1 x N M dx
20 19 1 2 3 lcmineqlem13 φ 0 1 x M 1 1 x N M dx = 1 M ( N M)
21 20 oveq2d φ lcm _ 1 N 0 1 x M 1 1 x N M dx = lcm _ 1 N 1 M ( N M)
22 19 2 1 3 lcmineqlem15 φ lcm _ 1 N 0 1 x M 1 1 x N M dx
23 21 22 eqeltrrd φ lcm _ 1 N 1 M ( N M)
24 18 23 eqeltrd φ lcm _ 1 N M ( N M)
25 1 12 nnmulcld φ M ( N M)
26 25 8 nndivdvdsd φ M ( N M) lcm _ 1 N lcm _ 1 N M ( N M)
27 24 26 mpbird φ M ( N M) lcm _ 1 N