Theorem gcdn0cl 11921

Description: Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)

Assertion

Ref	Expression
gcdn0cl	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )

Proof of Theorem gcdn0cl

Dummy variable n is distinct from all other variables.

Step	Hyp	Ref	Expression
1		gcdn0val 11920	. 2 |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )
2		gcdsupcl 11917	. 2 |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) e. NN )
3	1, 2	eqeltrd 2248	1 |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   = wceq 1349   e. wcel 2142   {crab 2453   class class class wbr 3990  (class class class)co 5857   supcsup 6963   RRcr 7777   0cc0 7778   < clt 7958   NNcn 8882   ZZcz 9216   || cdvds 11753   gcd cgcd 11901

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 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-coll 4105  ax-sep 4108  ax-nul 4116  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-setind 4522  ax-iinf 4573  ax-cnex 7869  ax-resscn 7870  ax-1cn 7871  ax-1re 7872  ax-icn 7873  ax-addcl 7874  ax-addrcl 7875  ax-mulcl 7876  ax-mulrcl 7877  ax-addcom 7878  ax-mulcom 7879  ax-addass 7880  ax-mulass 7881  ax-distr 7882  ax-i2m1 7883  ax-0lt1 7884  ax-1rid 7885  ax-0id 7886  ax-rnegex 7887  ax-precex 7888  ax-cnre 7889  ax-pre-ltirr 7890  ax-pre-ltwlin 7891  ax-pre-lttrn 7892  ax-pre-apti 7893  ax-pre-ltadd 7894  ax-pre-mulgt0 7895  ax-pre-mulext 7896  ax-arch 7897  ax-caucvg 7898

This theorem depends on definitions:  df-bi 116  df-dc 831  df-3or 975  df-3an 976  df-tru 1352  df-fal 1355  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-nel 2437  df-ral 2454  df-rex 2455  df-reu 2456  df-rmo 2457  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-nul 3416  df-if 3528  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-tr 4089  df-id 4279  df-po 4282  df-iso 4283  df-iord 4352  df-on 4354  df-ilim 4355  df-suc 4357  df-iom 4576  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-f1 5205  df-fo 5206  df-f1o 5207  df-fv 5208  df-riota 5813  df-ov 5860  df-oprab 5861  df-mpo 5862  df-1st 6123  df-2nd 6124  df-recs 6288  df-frec 6374  df-sup 6965  df-pnf 7960  df-mnf 7961  df-xr 7962  df-ltxr 7963  df-le 7964  df-sub 8096  df-neg 8097  df-reap 8498  df-ap 8505  df-div 8594  df-inn 8883  df-2 8941  df-3 8942  df-4 8943  df-n0 9140  df-z 9217  df-uz 9492  df-q 9583  df-rp 9615  df-fz 9970  df-fzo 10103  df-fl 10230  df-mod 10283  df-seqfrec 10406  df-exp 10480  df-cj 10810  df-re 10811  df-im 10812  df-rsqrt 10966  df-abs 10967  df-dvds 11754  df-gcd 11902

This theorem is referenced by:  gcddvds  11922  gcdcl  11925  gcdnncl  11926  gcd2n0cl  11928  divgcdnn  11934  gcdeq0  11936  gcd1  11946  sqgcd  11988  bezoutr1  11992  3lcm2e6woprm  12044  6lcm4e12  12045  qredeu  12055  rpdvds  12057  coprm  12102  rpexp  12111  divnumden  12154  divdenle  12155  phimullem  12183  phisum  12198  pythagtriplem4  12226  pythagtriplem8  12230  pythagtriplem9  12231  pcgcd1  12285  pc2dvds  12287  pockthlem  12312  2sqlem8a  13837  2sqlem8  13838