lcmgcdlem

Description: Lemma for lcmgcd and lcmdvds . Prove them for positive M , N , and K . (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

		Ref	Expression
	Assertion	lcmgcdlem	\|- ( ( M e. NN /\ N e. NN ) -> ( ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) /\ ( ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) -> ( M lcm N ) \|\| K ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnmulcl	\|- ( ( M e. NN /\ N e. NN ) -> ( M x. N ) e. NN )
2	1	nnred	\|- ( ( M e. NN /\ N e. NN ) -> ( M x. N ) e. RR )
3		nnz	\|- ( M e. NN -> M e. ZZ )
4	3	adantr	\|- ( ( M e. NN /\ N e. NN ) -> M e. ZZ )
5	4	zred	\|- ( ( M e. NN /\ N e. NN ) -> M e. RR )
6		nnz	\|- ( N e. NN -> N e. ZZ )
7	6	adantl	\|- ( ( M e. NN /\ N e. NN ) -> N e. ZZ )
8	7	zred	\|- ( ( M e. NN /\ N e. NN ) -> N e. RR )
9		0red	\|- ( M e. NN -> 0 e. RR )
10		nnre	\|- ( M e. NN -> M e. RR )
11		nngt0	\|- ( M e. NN -> 0 < M )
12	9 10 11	ltled	\|- ( M e. NN -> 0 <_ M )
13	12	adantr	\|- ( ( M e. NN /\ N e. NN ) -> 0 <_ M )
14		0red	\|- ( N e. NN -> 0 e. RR )
15		nnre	\|- ( N e. NN -> N e. RR )
16		nngt0	\|- ( N e. NN -> 0 < N )
17	14 15 16	ltled	\|- ( N e. NN -> 0 <_ N )
18	17	adantl	\|- ( ( M e. NN /\ N e. NN ) -> 0 <_ N )
19	5 8 13 18	mulge0d	\|- ( ( M e. NN /\ N e. NN ) -> 0 <_ ( M x. N ) )
20	2 19	absidd	\|- ( ( M e. NN /\ N e. NN ) -> ( abs ` ( M x. N ) ) = ( M x. N ) )
21	3 6	anim12i	\|- ( ( M e. NN /\ N e. NN ) -> ( M e. ZZ /\ N e. ZZ ) )
22		nnne0	\|- ( M e. NN -> M =/= 0 )
23	22	neneqd	\|- ( M e. NN -> -. M = 0 )
24		nnne0	\|- ( N e. NN -> N =/= 0 )
25	24	neneqd	\|- ( N e. NN -> -. N = 0 )
26	23 25	anim12i	\|- ( ( M e. NN /\ N e. NN ) -> ( -. M = 0 /\ -. N = 0 ) )
27		ioran	\|- ( -. ( M = 0 \/ N = 0 ) <-> ( -. M = 0 /\ -. N = 0 ) )
28	26 27	sylibr	\|- ( ( M e. NN /\ N e. NN ) -> -. ( M = 0 \/ N = 0 ) )
29		lcmn0val	\|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = inf ( { x e. NN \| ( M \|\| x /\ N \|\| x ) } , RR , < ) )
30	21 28 29	syl2anc	\|- ( ( M e. NN /\ N e. NN ) -> ( M lcm N ) = inf ( { x e. NN \| ( M \|\| x /\ N \|\| x ) } , RR , < ) )
31		ltso	\|- < Or RR
32	31	a1i	\|- ( ( M e. NN /\ N e. NN ) -> < Or RR )
33		gcddvds	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) \|\| M /\ ( M gcd N ) \|\| N ) )
34	33	simpld	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) \|\| M )
35		gcdcl	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
36	35	nn0zd	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. ZZ )
37		dvdsmultr1	\|- ( ( ( M gcd N ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) \|\| M -> ( M gcd N ) \|\| ( M x. N ) ) )
38	37	3expb	\|- ( ( ( M gcd N ) e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( M gcd N ) \|\| M -> ( M gcd N ) \|\| ( M x. N ) ) )
39	36 38	mpancom	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) \|\| M -> ( M gcd N ) \|\| ( M x. N ) ) )
40	34 39	mpd	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) \|\| ( M x. N ) )
41	21 40	syl	\|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) \|\| ( M x. N ) )
42		gcdnncl	\|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. NN )
43		nndivdvds	\|- ( ( ( M x. N ) e. NN /\ ( M gcd N ) e. NN ) -> ( ( M gcd N ) \|\| ( M x. N ) <-> ( ( M x. N ) / ( M gcd N ) ) e. NN ) )
44	1 42 43	syl2anc	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M gcd N ) \|\| ( M x. N ) <-> ( ( M x. N ) / ( M gcd N ) ) e. NN ) )
45	41 44	mpbid	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) e. NN )
46	45	nnred	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) e. RR )
47		breq2	\|- ( x = ( ( M x. N ) / ( M gcd N ) ) -> ( M \|\| x <-> M \|\| ( ( M x. N ) / ( M gcd N ) ) ) )
48		breq2	\|- ( x = ( ( M x. N ) / ( M gcd N ) ) -> ( N \|\| x <-> N \|\| ( ( M x. N ) / ( M gcd N ) ) ) )
49	47 48	anbi12d	\|- ( x = ( ( M x. N ) / ( M gcd N ) ) -> ( ( M \|\| x /\ N \|\| x ) <-> ( M \|\| ( ( M x. N ) / ( M gcd N ) ) /\ N \|\| ( ( M x. N ) / ( M gcd N ) ) ) ) )
50	33	simprd	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) \|\| N )
51	21 50	syl	\|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) \|\| N )
52	21 36	syl	\|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. ZZ )
53	42	nnne0d	\|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) =/= 0 )
54		dvdsval2	\|- ( ( ( M gcd N ) e. ZZ /\ ( M gcd N ) =/= 0 /\ N e. ZZ ) -> ( ( M gcd N ) \|\| N <-> ( N / ( M gcd N ) ) e. ZZ ) )
55	52 53 7 54	syl3anc	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M gcd N ) \|\| N <-> ( N / ( M gcd N ) ) e. ZZ ) )
56	51 55	mpbid	\|- ( ( M e. NN /\ N e. NN ) -> ( N / ( M gcd N ) ) e. ZZ )
57		dvdsmul1	\|- ( ( M e. ZZ /\ ( N / ( M gcd N ) ) e. ZZ ) -> M \|\| ( M x. ( N / ( M gcd N ) ) ) )
58	4 56 57	syl2anc	\|- ( ( M e. NN /\ N e. NN ) -> M \|\| ( M x. ( N / ( M gcd N ) ) ) )
59		nncn	\|- ( M e. NN -> M e. CC )
60	59	adantr	\|- ( ( M e. NN /\ N e. NN ) -> M e. CC )
61		nncn	\|- ( N e. NN -> N e. CC )
62	61	adantl	\|- ( ( M e. NN /\ N e. NN ) -> N e. CC )
63	42	nncnd	\|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. CC )
64	60 62 63 53	divassd	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) = ( M x. ( N / ( M gcd N ) ) ) )
65	58 64	breqtrrd	\|- ( ( M e. NN /\ N e. NN ) -> M \|\| ( ( M x. N ) / ( M gcd N ) ) )
66	21 34	syl	\|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) \|\| M )
67		dvdsval2	\|- ( ( ( M gcd N ) e. ZZ /\ ( M gcd N ) =/= 0 /\ M e. ZZ ) -> ( ( M gcd N ) \|\| M <-> ( M / ( M gcd N ) ) e. ZZ ) )
68	52 53 4 67	syl3anc	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M gcd N ) \|\| M <-> ( M / ( M gcd N ) ) e. ZZ ) )
69	66 68	mpbid	\|- ( ( M e. NN /\ N e. NN ) -> ( M / ( M gcd N ) ) e. ZZ )
70		dvdsmul1	\|- ( ( N e. ZZ /\ ( M / ( M gcd N ) ) e. ZZ ) -> N \|\| ( N x. ( M / ( M gcd N ) ) ) )
71	7 69 70	syl2anc	\|- ( ( M e. NN /\ N e. NN ) -> N \|\| ( N x. ( M / ( M gcd N ) ) ) )
72	60 62	mulcomd	\|- ( ( M e. NN /\ N e. NN ) -> ( M x. N ) = ( N x. M ) )
73	72	oveq1d	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) = ( ( N x. M ) / ( M gcd N ) ) )
74	62 60 63 53	divassd	\|- ( ( M e. NN /\ N e. NN ) -> ( ( N x. M ) / ( M gcd N ) ) = ( N x. ( M / ( M gcd N ) ) ) )
75	73 74	eqtrd	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) = ( N x. ( M / ( M gcd N ) ) ) )
76	71 75	breqtrrd	\|- ( ( M e. NN /\ N e. NN ) -> N \|\| ( ( M x. N ) / ( M gcd N ) ) )
77	65 76	jca	\|- ( ( M e. NN /\ N e. NN ) -> ( M \|\| ( ( M x. N ) / ( M gcd N ) ) /\ N \|\| ( ( M x. N ) / ( M gcd N ) ) ) )
78	49 45 77	elrabd	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) e. { x e. NN \| ( M \|\| x /\ N \|\| x ) } )
79	46	adantr	\|- ( ( ( M e. NN /\ N e. NN ) /\ n e. { x e. NN \| ( M \|\| x /\ N \|\| x ) } ) -> ( ( M x. N ) / ( M gcd N ) ) e. RR )
80		elrabi	\|- ( n e. { x e. NN \| ( M \|\| x /\ N \|\| x ) } -> n e. NN )
81	80	nnred	\|- ( n e. { x e. NN \| ( M \|\| x /\ N \|\| x ) } -> n e. RR )
82	81	adantl	\|- ( ( ( M e. NN /\ N e. NN ) /\ n e. { x e. NN \| ( M \|\| x /\ N \|\| x ) } ) -> n e. RR )
83		breq2	\|- ( x = n -> ( M \|\| x <-> M \|\| n ) )
84		breq2	\|- ( x = n -> ( N \|\| x <-> N \|\| n ) )
85	83 84	anbi12d	\|- ( x = n -> ( ( M \|\| x /\ N \|\| x ) <-> ( M \|\| n /\ N \|\| n ) ) )
86	85	elrab	\|- ( n e. { x e. NN \| ( M \|\| x /\ N \|\| x ) } <-> ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) )
87		bezout	\|- ( ( M e. ZZ /\ N e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) )
88	21 87	syl	\|- ( ( M e. NN /\ N e. NN ) -> E. x e. ZZ E. y e. ZZ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) )
89	88	adantr	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> E. x e. ZZ E. y e. ZZ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) )
90		nncn	\|- ( n e. NN -> n e. CC )
91	90	ad2antlr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> n e. CC )
92	1	nncnd	\|- ( ( M e. NN /\ N e. NN ) -> ( M x. N ) e. CC )
93	92	ad2antrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M x. N ) e. CC )
94	63	ad2antrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M gcd N ) e. CC )
95	60	ad2antrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> M e. CC )
96	61	ad3antlr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> N e. CC )
97	22	ad3antrrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> M =/= 0 )
98	24	ad3antlr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> N =/= 0 )
99	95 96 97 98	mulne0d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M x. N ) =/= 0 )
100	53	ad2antrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M gcd N ) =/= 0 )
101	91 93 94 99 100	divdiv2d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n / ( ( M x. N ) / ( M gcd N ) ) ) = ( ( n x. ( M gcd N ) ) / ( M x. N ) ) )
102	101	adantr	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( n / ( ( M x. N ) / ( M gcd N ) ) ) = ( ( n x. ( M gcd N ) ) / ( M x. N ) ) )
103		oveq2	\|- ( ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> ( n x. ( M gcd N ) ) = ( n x. ( ( M x. x ) + ( N x. y ) ) ) )
104	103	oveq1d	\|- ( ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> ( ( n x. ( M gcd N ) ) / ( M x. N ) ) = ( ( n x. ( ( M x. x ) + ( N x. y ) ) ) / ( M x. N ) ) )
105		zcn	\|- ( x e. ZZ -> x e. CC )
106	105	ad2antrl	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. CC )
107	95 106	mulcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M x. x ) e. CC )
108		zcn	\|- ( y e. ZZ -> y e. CC )
109	108	ad2antll	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. CC )
110	96 109	mulcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( N x. y ) e. CC )
111	91 107 110	adddid	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. ( ( M x. x ) + ( N x. y ) ) ) = ( ( n x. ( M x. x ) ) + ( n x. ( N x. y ) ) ) )
112	111	oveq1d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( n x. ( ( M x. x ) + ( N x. y ) ) ) / ( M x. N ) ) = ( ( ( n x. ( M x. x ) ) + ( n x. ( N x. y ) ) ) / ( M x. N ) ) )
113	91 107	mulcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. ( M x. x ) ) e. CC )
114	91 110	mulcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. ( N x. y ) ) e. CC )
115	113 114 93 99	divdird	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( n x. ( M x. x ) ) + ( n x. ( N x. y ) ) ) / ( M x. N ) ) = ( ( ( n x. ( M x. x ) ) / ( M x. N ) ) + ( ( n x. ( N x. y ) ) / ( M x. N ) ) ) )
116	112 115	eqtrd	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( n x. ( ( M x. x ) + ( N x. y ) ) ) / ( M x. N ) ) = ( ( ( n x. ( M x. x ) ) / ( M x. N ) ) + ( ( n x. ( N x. y ) ) / ( M x. N ) ) ) )
117	104 116	sylan9eqr	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( ( n x. ( M gcd N ) ) / ( M x. N ) ) = ( ( ( n x. ( M x. x ) ) / ( M x. N ) ) + ( ( n x. ( N x. y ) ) / ( M x. N ) ) ) )
118	91 95 106	mul12d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. ( M x. x ) ) = ( M x. ( n x. x ) ) )
119	118	oveq1d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( n x. ( M x. x ) ) / ( M x. N ) ) = ( ( M x. ( n x. x ) ) / ( M x. N ) ) )
120	91 106	mulcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. x ) e. CC )
121	120 96 95 98 97	divcan5d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M x. ( n x. x ) ) / ( M x. N ) ) = ( ( n x. x ) / N ) )
122	119 121	eqtrd	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( n x. ( M x. x ) ) / ( M x. N ) ) = ( ( n x. x ) / N ) )
123	91 96 109	mul12d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. ( N x. y ) ) = ( N x. ( n x. y ) ) )
124	123	oveq1d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( n x. ( N x. y ) ) / ( M x. N ) ) = ( ( N x. ( n x. y ) ) / ( M x. N ) ) )
125	72	ad2antrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M x. N ) = ( N x. M ) )
126	125	oveq2d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( N x. ( n x. y ) ) / ( M x. N ) ) = ( ( N x. ( n x. y ) ) / ( N x. M ) ) )
127	91 109	mulcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. y ) e. CC )
128	127 95 96 97 98	divcan5d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( N x. ( n x. y ) ) / ( N x. M ) ) = ( ( n x. y ) / M ) )
129	124 126 128	3eqtrd	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( n x. ( N x. y ) ) / ( M x. N ) ) = ( ( n x. y ) / M ) )
130	122 129	oveq12d	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( n x. ( M x. x ) ) / ( M x. N ) ) + ( ( n x. ( N x. y ) ) / ( M x. N ) ) ) = ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) )
131	130	adantr	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( ( ( n x. ( M x. x ) ) / ( M x. N ) ) + ( ( n x. ( N x. y ) ) / ( M x. N ) ) ) = ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) )
132	102 117 131	3eqtrd	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( n / ( ( M x. N ) / ( M gcd N ) ) ) = ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) )
133	132	ex	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> ( n / ( ( M x. N ) / ( M gcd N ) ) ) = ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) ) )
134	133	adantlrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> ( n / ( ( M x. N ) / ( M gcd N ) ) ) = ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) ) )
135	134	imp	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( n / ( ( M x. N ) / ( M gcd N ) ) ) = ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) )
136	6	ad3antlr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> N e. ZZ )
137		nnz	\|- ( n e. NN -> n e. ZZ )
138	137	ad2antlr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> n e. ZZ )
139		simprl	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. ZZ )
140		dvdsmultr1	\|- ( ( N e. ZZ /\ n e. ZZ /\ x e. ZZ ) -> ( N \|\| n -> N \|\| ( n x. x ) ) )
141	136 138 139 140	syl3anc	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( N \|\| n -> N \|\| ( n x. x ) ) )
142	138 139	zmulcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. x ) e. ZZ )
143		dvdsval2	\|- ( ( N e. ZZ /\ N =/= 0 /\ ( n x. x ) e. ZZ ) -> ( N \|\| ( n x. x ) <-> ( ( n x. x ) / N ) e. ZZ ) )
144	136 98 142 143	syl3anc	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( N \|\| ( n x. x ) <-> ( ( n x. x ) / N ) e. ZZ ) )
145	141 144	sylibd	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( N \|\| n -> ( ( n x. x ) / N ) e. ZZ ) )
146	145	adantld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M \|\| n /\ N \|\| n ) -> ( ( n x. x ) / N ) e. ZZ ) )
147	146	3impia	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) /\ ( M \|\| n /\ N \|\| n ) ) -> ( ( n x. x ) / N ) e. ZZ )
148	3	ad3antrrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> M e. ZZ )
149		simprr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. ZZ )
150		dvdsmultr1	\|- ( ( M e. ZZ /\ n e. ZZ /\ y e. ZZ ) -> ( M \|\| n -> M \|\| ( n x. y ) ) )
151	148 138 149 150	syl3anc	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M \|\| n -> M \|\| ( n x. y ) ) )
152	138 149	zmulcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( n x. y ) e. ZZ )
153		dvdsval2	\|- ( ( M e. ZZ /\ M =/= 0 /\ ( n x. y ) e. ZZ ) -> ( M \|\| ( n x. y ) <-> ( ( n x. y ) / M ) e. ZZ ) )
154	148 97 152 153	syl3anc	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M \|\| ( n x. y ) <-> ( ( n x. y ) / M ) e. ZZ ) )
155	151 154	sylibd	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( M \|\| n -> ( ( n x. y ) / M ) e. ZZ ) )
156	155	adantrd	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M \|\| n /\ N \|\| n ) -> ( ( n x. y ) / M ) e. ZZ ) )
157	156	3impia	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) /\ ( M \|\| n /\ N \|\| n ) ) -> ( ( n x. y ) / M ) e. ZZ )
158	147 157	zaddcld	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) /\ ( M \|\| n /\ N \|\| n ) ) -> ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) e. ZZ )
159	158	3expia	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M \|\| n /\ N \|\| n ) -> ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) e. ZZ ) )
160	159	an32s	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ n e. NN ) -> ( ( M \|\| n /\ N \|\| n ) -> ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) e. ZZ ) )
161	160	impr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) e. ZZ )
162	161	an32s	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) e. ZZ )
163	162	adantr	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( ( ( n x. x ) / N ) + ( ( n x. y ) / M ) ) e. ZZ )
164	135 163	eqeltrd	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( n / ( ( M x. N ) / ( M gcd N ) ) ) e. ZZ )
165	45	nnzd	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) e. ZZ )
166	165	ad2antrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M x. N ) / ( M gcd N ) ) e. ZZ )
167	1	nnne0d	\|- ( ( M e. NN /\ N e. NN ) -> ( M x. N ) =/= 0 )
168	92 63 167 53	divne0d	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) =/= 0 )
169	168	ad2antrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M x. N ) / ( M gcd N ) ) =/= 0 )
170	138	adantlrr	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> n e. ZZ )
171		dvdsval2	\|- ( ( ( ( M x. N ) / ( M gcd N ) ) e. ZZ /\ ( ( M x. N ) / ( M gcd N ) ) =/= 0 /\ n e. ZZ ) -> ( ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> ( n / ( ( M x. N ) / ( M gcd N ) ) ) e. ZZ ) )
172	166 169 170 171	syl3anc	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> ( n / ( ( M x. N ) / ( M gcd N ) ) ) e. ZZ ) )
173	172	adantr	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> ( n / ( ( M x. N ) / ( M gcd N ) ) ) e. ZZ ) )
174	164 173	mpbird	\|- ( ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) ) -> ( ( M x. N ) / ( M gcd N ) ) \|\| n )
175	174	ex	\|- ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> ( ( M x. N ) / ( M gcd N ) ) \|\| n ) )
176	175	reximdvva	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( E. x e. ZZ E. y e. ZZ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> E. x e. ZZ E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n ) )
177	89 176	mpd	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> E. x e. ZZ E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n )
178		1z	\|- 1 e. ZZ
179		ne0i	\|- ( 1 e. ZZ -> ZZ =/= (/) )
180		r19.9rzv	\|- ( ZZ =/= (/) -> ( ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n ) )
181	178 179 180	mp2b	\|- ( ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n )
182		r19.9rzv	\|- ( ZZ =/= (/) -> ( E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> E. x e. ZZ E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n ) )
183	178 179 182	mp2b	\|- ( E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> E. x e. ZZ E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n )
184	181 183	bitri	\|- ( ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> E. x e. ZZ E. y e. ZZ ( ( M x. N ) / ( M gcd N ) ) \|\| n )
185	177 184	sylibr	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( ( M x. N ) / ( M gcd N ) ) \|\| n )
186	165	adantr	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( ( M x. N ) / ( M gcd N ) ) e. ZZ )
187		simprl	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> n e. NN )
188		dvdsle	\|- ( ( ( ( M x. N ) / ( M gcd N ) ) e. ZZ /\ n e. NN ) -> ( ( ( M x. N ) / ( M gcd N ) ) \|\| n -> ( ( M x. N ) / ( M gcd N ) ) <_ n ) )
189	186 187 188	syl2anc	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( ( ( M x. N ) / ( M gcd N ) ) \|\| n -> ( ( M x. N ) / ( M gcd N ) ) <_ n ) )
190	185 189	mpd	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( ( M x. N ) / ( M gcd N ) ) <_ n )
191	86 190	sylan2b	\|- ( ( ( M e. NN /\ N e. NN ) /\ n e. { x e. NN \| ( M \|\| x /\ N \|\| x ) } ) -> ( ( M x. N ) / ( M gcd N ) ) <_ n )
192	79 82 191	lensymd	\|- ( ( ( M e. NN /\ N e. NN ) /\ n e. { x e. NN \| ( M \|\| x /\ N \|\| x ) } ) -> -. n < ( ( M x. N ) / ( M gcd N ) ) )
193	32 46 78 192	infmin	\|- ( ( M e. NN /\ N e. NN ) -> inf ( { x e. NN \| ( M \|\| x /\ N \|\| x ) } , RR , < ) = ( ( M x. N ) / ( M gcd N ) ) )
194	30 193	eqtr2d	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M x. N ) / ( M gcd N ) ) = ( M lcm N ) )
195	194 45	eqeltrrd	\|- ( ( M e. NN /\ N e. NN ) -> ( M lcm N ) e. NN )
196	195	nncnd	\|- ( ( M e. NN /\ N e. NN ) -> ( M lcm N ) e. CC )
197	92 196 63 53	divmul3d	\|- ( ( M e. NN /\ N e. NN ) -> ( ( ( M x. N ) / ( M gcd N ) ) = ( M lcm N ) <-> ( M x. N ) = ( ( M lcm N ) x. ( M gcd N ) ) ) )
198	194 197	mpbid	\|- ( ( M e. NN /\ N e. NN ) -> ( M x. N ) = ( ( M lcm N ) x. ( M gcd N ) ) )
199	20 198	eqtr2d	\|- ( ( M e. NN /\ N e. NN ) -> ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) )
200		simprl	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) ) -> K e. NN )
201		eleq1	\|- ( n = K -> ( n e. NN <-> K e. NN ) )
202		breq2	\|- ( n = K -> ( M \|\| n <-> M \|\| K ) )
203		breq2	\|- ( n = K -> ( N \|\| n <-> N \|\| K ) )
204	202 203	anbi12d	\|- ( n = K -> ( ( M \|\| n /\ N \|\| n ) <-> ( M \|\| K /\ N \|\| K ) ) )
205	201 204	anbi12d	\|- ( n = K -> ( ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) <-> ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) ) )
206	205	anbi2d	\|- ( n = K -> ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) <-> ( ( M e. NN /\ N e. NN ) /\ ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) ) ) )
207		breq2	\|- ( n = K -> ( ( M lcm N ) \|\| n <-> ( M lcm N ) \|\| K ) )
208	206 207	imbi12d	\|- ( n = K -> ( ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( M lcm N ) \|\| n ) <-> ( ( ( M e. NN /\ N e. NN ) /\ ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) ) -> ( M lcm N ) \|\| K ) ) )
209	194	breq1d	\|- ( ( M e. NN /\ N e. NN ) -> ( ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> ( M lcm N ) \|\| n ) )
210	209	adantr	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( ( ( M x. N ) / ( M gcd N ) ) \|\| n <-> ( M lcm N ) \|\| n ) )
211	185 210	mpbid	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( n e. NN /\ ( M \|\| n /\ N \|\| n ) ) ) -> ( M lcm N ) \|\| n )
212	208 211	vtoclg	\|- ( K e. NN -> ( ( ( M e. NN /\ N e. NN ) /\ ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) ) -> ( M lcm N ) \|\| K ) )
213	200 212	mpcom	\|- ( ( ( M e. NN /\ N e. NN ) /\ ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) ) -> ( M lcm N ) \|\| K )
214	213	ex	\|- ( ( M e. NN /\ N e. NN ) -> ( ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) -> ( M lcm N ) \|\| K ) )
215	199 214	jca	\|- ( ( M e. NN /\ N e. NN ) -> ( ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) /\ ( ( K e. NN /\ ( M \|\| K /\ N \|\| K ) ) -> ( M lcm N ) \|\| K ) ) )

Metamath Proof Explorer

Theorem lcmgcdlem

Proof