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

Theorem rpmulgcd2 11846
 Description: If is relatively prime to , then the GCD of with is the product of the GCDs with and respectively. (Contributed by Mario Carneiro, 2-Jul-2015.)
Assertion
Ref Expression
rpmulgcd2

Proof of Theorem rpmulgcd2
StepHypRef Expression
1 simpl1 985 . . 3
2 simpl2 986 . . . 4
3 simpl3 987 . . . 4
42, 3zmulcld 9230 . . 3
51, 4gcdcld 11727 . 2
61, 2gcdcld 11727 . . 3
71, 3gcdcld 11727 . . 3
86, 7nn0mulcld 9086 . 2
9 mulgcddvds 11845 . . 3
11 gcddvds 11722 . . . . . 6
121, 2, 11syl2anc 409 . . . . 5
1312simpld 111 . . . 4
14 gcddvds 11722 . . . . . 6
151, 3, 14syl2anc 409 . . . . 5
1615simpld 111 . . . 4
176nn0zd 9222 . . . . 5
187nn0zd 9222 . . . . 5
19 gcddvds 11722 . . . . . . . . . . 11
2017, 18, 19syl2anc 409 . . . . . . . . . 10
2120simpld 111 . . . . . . . . 9
2212simprd 113 . . . . . . . . 9
2317, 18gcdcld 11727 . . . . . . . . . . 11
2423nn0zd 9222 . . . . . . . . . 10
25 dvdstr 11600 . . . . . . . . . 10
2624, 17, 2, 25syl3anc 1217 . . . . . . . . 9
2721, 22, 26mp2and 430 . . . . . . . 8
2820simprd 113 . . . . . . . . 9
2915simprd 113 . . . . . . . . 9
30 dvdstr 11600 . . . . . . . . . 10
3124, 18, 3, 30syl3anc 1217 . . . . . . . . 9
3228, 29, 31mp2and 430 . . . . . . . 8
33 dvdsgcd 11770 . . . . . . . . 9
3424, 2, 3, 33syl3anc 1217 . . . . . . . 8
3527, 32, 34mp2and 430 . . . . . . 7
36 simpr 109 . . . . . . 7
3735, 36breqtrd 3963 . . . . . 6
38 dvds1 11621 . . . . . . 7
3923, 38syl 14 . . . . . 6
4037, 39mpbid 146 . . . . 5
41 coprmdvds2 11844 . . . . 5
4217, 18, 1, 40, 41syl31anc 1220 . . . 4
4313, 16, 42mp2and 430 . . 3
44 dvdscmul 11590 . . . . . 6
4518, 3, 17, 44syl3anc 1217 . . . . 5
46 dvdsmulc 11591 . . . . . 6
4717, 2, 3, 46syl3anc 1217 . . . . 5
4817, 18zmulcld 9230 . . . . . 6
4917, 3zmulcld 9230 . . . . . 6
50 dvdstr 11600 . . . . . 6
5148, 49, 4, 50syl3anc 1217 . . . . 5
5245, 47, 51syl2and 293 . . . 4
5329, 22, 52mp2and 430 . . 3
54 dvdsgcd 11770 . . . 4
5548, 1, 4, 54syl3anc 1217 . . 3
5643, 53, 55mp2and 430 . 2
57 dvdseq 11616 . 2
585, 8, 10, 56, 57syl22anc 1218 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 963   wceq 1332   wcel 1481   class class class wbr 3938  (class class class)co 5785  c1 7672   cmul 7676  cn0 9028  cz 9105   cdvds 11563   cgcd 11705 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-iinf 4512  ax-cnex 7762  ax-resscn 7763  ax-1cn 7764  ax-1re 7765  ax-icn 7766  ax-addcl 7767  ax-addrcl 7768  ax-mulcl 7769  ax-mulrcl 7770  ax-addcom 7771  ax-mulcom 7772  ax-addass 7773  ax-mulass 7774  ax-distr 7775  ax-i2m1 7776  ax-0lt1 7777  ax-1rid 7778  ax-0id 7779  ax-rnegex 7780  ax-precex 7781  ax-cnre 7782  ax-pre-ltirr 7783  ax-pre-ltwlin 7784  ax-pre-lttrn 7785  ax-pre-apti 7786  ax-pre-ltadd 7787  ax-pre-mulgt0 7788  ax-pre-mulext 7789  ax-arch 7790  ax-caucvg 7791 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4225  df-po 4228  df-iso 4229  df-iord 4298  df-on 4300  df-ilim 4301  df-suc 4303  df-iom 4515  df-xp 4556  df-rel 4557  df-cnv 4558  df-co 4559  df-dm 4560  df-rn 4561  df-res 4562  df-ima 4563  df-iota 5099  df-fun 5136  df-fn 5137  df-f 5138  df-f1 5139  df-fo 5140  df-f1o 5141  df-fv 5142  df-riota 5741  df-ov 5788  df-oprab 5789  df-mpo 5790  df-1st 6049  df-2nd 6050  df-recs 6213  df-frec 6299  df-sup 6887  df-pnf 7853  df-mnf 7854  df-xr 7855  df-ltxr 7856  df-le 7857  df-sub 7986  df-neg 7987  df-reap 8388  df-ap 8395  df-div 8484  df-inn 8772  df-2 8830  df-3 8831  df-4 8832  df-n0 9029  df-z 9106  df-uz 9378  df-q 9466  df-rp 9498  df-fz 9849  df-fzo 9978  df-fl 10101  df-mod 10154  df-seqfrec 10277  df-exp 10351  df-cj 10673  df-re 10674  df-im 10675  df-rsqrt 10829  df-abs 10830  df-dvds 11564  df-gcd 11706 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator