Theorem 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 ) ) )