Theorem 3lcm2e6 11681

Description: The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 27-Aug-2020.)

Assertion

Ref	Expression
3lcm2e6	|- ( 3 lcm 2 ) = 6

Proof of Theorem 3lcm2e6

Step	Hyp	Ref	Expression
1		2re 8697	. . . . . 6 |- 2 e. RR
2		2lt3 8791	. . . . . 6 |- 2 < 3
3	1, 2	gtneii 7779	. . . . 5 |- 3 =/= 2
4		3prm 11652	. . . . . 6 |- 3 e. Prime
5		2prm 11651	. . . . . 6 |- 2 e. Prime
6		prmrp 11666	. . . . . 6 |- ( ( 3 e. Prime /\ 2 e. Prime ) -> ( ( 3 gcd 2 ) = 1 <-> 3 =/= 2 ) )
7	4, 5, 6	mp2an 420	. . . . 5 |- ( ( 3 gcd 2 ) = 1 <-> 3 =/= 2 )
8	3, 7	mpbir 145	. . . 4 |- ( 3 gcd 2 ) = 1
9	8	oveq2i 5739	. . 3 |- ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) = ( ( 3 lcm 2 ) x. 1 )
10		3nn 8783	. . . 4 |- 3 e. NN
11		2nn 8782	. . . 4 |- 2 e. NN
12		lcmgcdnn 11606	. . . 4 |- ( ( 3 e. NN /\ 2 e. NN ) -> ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) = ( 3 x. 2 ) )
13	10, 11, 12	mp2an 420	. . 3 |- ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) = ( 3 x. 2 )
14	10	nnzi 8976	. . . . . 6 |- 3 e. ZZ
15	11	nnzi 8976	. . . . . 6 |- 2 e. ZZ
16		lcmcl 11596	. . . . . 6 |- ( ( 3 e. ZZ /\ 2 e. ZZ ) -> ( 3 lcm 2 ) e. NN0 )
17	14, 15, 16	mp2an 420	. . . . 5 |- ( 3 lcm 2 ) e. NN0
18	17	nn0cni 8890	. . . 4 |- ( 3 lcm 2 ) e. CC
19	18	mulid1i 7689	. . 3 |- ( ( 3 lcm 2 ) x. 1 ) = ( 3 lcm 2 )
20	9, 13, 19	3eqtr3ri 2144	. 2 |- ( 3 lcm 2 ) = ( 3 x. 2 )
21		3t2e6 8777	. 2 |- ( 3 x. 2 ) = 6
22	20, 21	eqtri 2135	1 |- ( 3 lcm 2 ) = 6

Syntax hints:   <-> wb 104   = wceq 1314   e. wcel 1463   =/= wne 2282  (class class class)co 5728   1c1 7545   x. cmul 7549   NNcn 8627   2c2 8678   3c3 8679   6c6 8682   NN0cn0 8878   ZZcz 8955   gcd cgcd 11480   lcm clcm 11584   Primecprime 11631

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4003  ax-sep 4006  ax-nul 4014  ax-pow 4058  ax-pr 4091  ax-un 4315  ax-setind 4412  ax-iinf 4462  ax-cnex 7633  ax-resscn 7634  ax-1cn 7635  ax-1re 7636  ax-icn 7637  ax-addcl 7638  ax-addrcl 7639  ax-mulcl 7640  ax-mulrcl 7641  ax-addcom 7642  ax-mulcom 7643  ax-addass 7644  ax-mulass 7645  ax-distr 7646  ax-i2m1 7647  ax-0lt1 7648  ax-1rid 7649  ax-0id 7650  ax-rnegex 7651  ax-precex 7652  ax-cnre 7653  ax-pre-ltirr 7654  ax-pre-ltwlin 7655  ax-pre-lttrn 7656  ax-pre-apti 7657  ax-pre-ltadd 7658  ax-pre-mulgt0 7659  ax-pre-mulext 7660  ax-arch 7661  ax-caucvg 7662

This theorem depends on definitions:  df-bi 116  df-stab 799  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-nel 2378  df-ral 2395  df-rex 2396  df-reu 2397  df-rmo 2398  df-rab 2399  df-v 2659  df-sbc 2879  df-csb 2972  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-nul 3330  df-if 3441  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-int 3738  df-iun 3781  df-br 3896  df-opab 3950  df-mpt 3951  df-tr 3987  df-id 4175  df-po 4178  df-iso 4179  df-iord 4248  df-on 4250  df-ilim 4251  df-suc 4253  df-iom 4465  df-xp 4505  df-rel 4506  df-cnv 4507  df-co 4508  df-dm 4509  df-rn 4510  df-res 4511  df-ima 4512  df-iota 5046  df-fun 5083  df-fn 5084  df-f 5085  df-f1 5086  df-fo 5087  df-f1o 5088  df-fv 5089  df-isom 5090  df-riota 5684  df-ov 5731  df-oprab 5732  df-mpo 5733  df-1st 5992  df-2nd 5993  df-recs 6156  df-frec 6242  df-1o 6267  df-2o 6268  df-er 6383  df-en 6589  df-sup 6823  df-inf 6824  df-pnf 7723  df-mnf 7724  df-xr 7725  df-ltxr 7726  df-le 7727  df-sub 7855  df-neg 7856  df-reap 8252  df-ap 8259  df-div 8343  df-inn 8628  df-2 8686  df-3 8687  df-4 8688  df-5 8689  df-6 8690  df-n0 8879  df-z 8956  df-uz 9226  df-q 9311  df-rp 9341  df-fz 9681  df-fzo 9810  df-fl 9933  df-mod 9986  df-seqfrec 10109  df-exp 10183  df-cj 10504  df-re 10505  df-im 10506  df-rsqrt 10659  df-abs 10660  df-dvds 11339  df-gcd 11481  df-lcm 11585  df-prm 11632

This theorem is referenced by: (None)