Theorem lcmineqlem14

Description: Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem14.1	|- ( ph -> A e. NN )
	lcmineqlem14.2	|- ( ph -> B e. NN )
	lcmineqlem14.3	|- ( ph -> C e. NN )
	lcmineqlem14.4	|- ( ph -> D e. NN )
	lcmineqlem14.5	|- ( ph -> E e. NN )
	lcmineqlem14.6	|- ( ph -> ( A x. C ) || D )
	lcmineqlem14.7	|- ( ph -> ( B x. C ) || E )
	lcmineqlem14.8	|- ( ph -> D || E )
	lcmineqlem14.9	|- ( ph -> ( A gcd B ) = 1 )
Assertion	lcmineqlem14	|- ( ph -> ( ( A x. B ) x. C ) || E )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem14.1	|- ( ph -> A e. NN )
2		lcmineqlem14.2	|- ( ph -> B e. NN )
3		lcmineqlem14.3	|- ( ph -> C e. NN )
4		lcmineqlem14.4	|- ( ph -> D e. NN )
5		lcmineqlem14.5	|- ( ph -> E e. NN )
6		lcmineqlem14.6	|- ( ph -> ( A x. C ) || D )
7		lcmineqlem14.7	|- ( ph -> ( B x. C ) || E )
8		lcmineqlem14.8	|- ( ph -> D || E )
9		lcmineqlem14.9	|- ( ph -> ( A gcd B ) = 1 )
10	1	nnzd	|- ( ph -> A e. ZZ )
11	2	nnzd	|- ( ph -> B e. ZZ )
12	2 3 5	nnproddivdvdsd	|- ( ph -> ( ( B x. C ) || E <-> B || ( E / C ) ) )
13	7 12	mpbid	|- ( ph -> B || ( E / C ) )
14		dvdszrcl	|- ( B || ( E / C ) -> ( B e. ZZ /\ ( E / C ) e. ZZ ) )
15	13 14	syl	|- ( ph -> ( B e. ZZ /\ ( E / C ) e. ZZ ) )
16	15	simprd	|- ( ph -> ( E / C ) e. ZZ )
17	3	nnzd	|- ( ph -> C e. ZZ )
18	10 17	zmulcld	|- ( ph -> ( A x. C ) e. ZZ )
19	4	nnzd	|- ( ph -> D e. ZZ )
20	5	nnzd	|- ( ph -> E e. ZZ )
21	18 19 20 6 8	dvdstrd	|- ( ph -> ( A x. C ) || E )
22	1 3 5	nnproddivdvdsd	|- ( ph -> ( ( A x. C ) || E <-> A || ( E / C ) ) )
23	21 22	mpbid	|- ( ph -> A || ( E / C ) )
24	10 11 16 9 23 13	coprmdvds2d	|- ( ph -> ( A x. B ) || ( E / C ) )
25	1 2	nnmulcld	|- ( ph -> ( A x. B ) e. NN )
26	25 3 5	nnproddivdvdsd	|- ( ph -> ( ( ( A x. B ) x. C ) || E <-> ( A x. B ) || ( E / C ) ) )
27	24 26	mpbird	|- ( ph -> ( ( A x. B ) x. C ) || E )