Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  lcmgcd Unicode version

Theorem lcmgcd 11831
 Description: The product of two numbers' least common multiple and greatest common divisor is the absolute value of the product of the two numbers. In particular, that absolute value is the least common multiple of two coprime numbers, for which . Multiple methods exist for proving this, and it is often proven either as a consequence of the fundamental theorem of arithmetic or of Bézout's identity bezout 11771; see e.g. https://proofwiki.org/wiki/Product_of_GCD_and_LCM 11771 and https://math.stackexchange.com/a/470827 11771. This proof uses the latter to first confirm it for positive integers and (the "Second Proof" in the above Stack Exchange page), then shows that implies it for all nonzero integer inputs, then finally uses lcm0val 11818 to show it applies when either or both inputs are zero. (Contributed by Steve Rodriguez, 20-Jan-2020.)
Assertion
Ref Expression
lcmgcd lcm

Proof of Theorem lcmgcd
StepHypRef Expression
1 gcdcl 11727 . . . . . . . 8
21nn0cnd 9085 . . . . . . 7
32mul02d 8207 . . . . . 6
4 0z 9118 . . . . . . . . . 10
5 lcmcom 11817 . . . . . . . . . 10 lcm lcm
64, 5mpan2 422 . . . . . . . . 9 lcm lcm
7 lcm0val 11818 . . . . . . . . 9 lcm
86, 7eqtr3d 2176 . . . . . . . 8 lcm
98adantl 275 . . . . . . 7 lcm
109oveq1d 5801 . . . . . 6 lcm
11 zcn 9112 . . . . . . . . 9
1211adantl 275 . . . . . . . 8
1312mul02d 8207 . . . . . . 7
1413abs00bd 10899 . . . . . 6
153, 10, 143eqtr4d 2184 . . . . 5 lcm
1615adantr 274 . . . 4 lcm
17 simpr 109 . . . . . 6
1817oveq1d 5801 . . . . 5 lcm lcm
1918oveq1d 5801 . . . 4 lcm lcm
2017oveq1d 5801 . . . . 5
2120fveq2d 5437 . . . 4
2216, 19, 213eqtr4d 2184 . . 3 lcm
23 lcm0val 11818 . . . . . . . 8 lcm
2423adantr 274 . . . . . . 7 lcm
2524oveq1d 5801 . . . . . 6 lcm
26 zcn 9112 . . . . . . . . 9
2726adantr 274 . . . . . . . 8
2827mul01d 8208 . . . . . . 7
2928abs00bd 10899 . . . . . 6
303, 25, 293eqtr4d 2184 . . . . 5 lcm
3130adantr 274 . . . 4 lcm
32 simpr 109 . . . . . 6
3332oveq2d 5802 . . . . 5 lcm lcm
3433oveq1d 5801 . . . 4 lcm lcm
3532oveq2d 5802 . . . . 5
3635fveq2d 5437 . . . 4
3731, 34, 363eqtr4d 2184 . . 3 lcm
3822, 37jaodan 787 . 2 lcm
39 neanior 2397 . . . . 5
40 nnabscl 10933 . . . . . . 7
41 nnabscl 10933 . . . . . . 7
4240, 41anim12i 336 . . . . . 6
4342an4s 578 . . . . 5
4439, 43sylan2br 286 . . . 4
45 lcmgcdlem 11830 . . . . 5 lcm lcm
4645simpld 111 . . . 4 lcm
4744, 46syl 14 . . 3 lcm
48 lcmabs 11829 . . . . 5 lcm lcm
49 gcdabs 11748 . . . . 5
5048, 49oveq12d 5804 . . . 4 lcm lcm
5150adantr 274 . . 3 lcm lcm
52 absidm 10931 . . . . . . 7
53 absidm 10931 . . . . . . 7
5452, 53oveqan12d 5805 . . . . . 6
5526, 11, 54syl2an 287 . . . . 5
56 nn0abscl 10918 . . . . . . . 8
5756nn0cnd 9085 . . . . . . 7
5857adantr 274 . . . . . 6
59 nn0abscl 10918 . . . . . . . 8
6059nn0cnd 9085 . . . . . . 7
6160adantl 275 . . . . . 6
6258, 61absmuld 11027 . . . . 5
6327, 12absmuld 11027 . . . . 5
6455, 62, 633eqtr4d 2184 . . . 4