Name Conclusion Link
natural-divides_1 !a. divides a 0 link to proof
natural-divides_2 !a. divides a a link to proof
natural-divides_3 !a. divides 1 a link to proof
natural-divides_4 !a. gcd 0 a = a link to proof
natural-divides_5 !a. gcd a 0 = a link to proof
natural-divides_6 !a. gcd a a = a link to proof
natural-divides_7 !a. lcm 0 a = 0 link to proof
natural-divides_8 !a. lcm a 0 = 0 link to proof
natural-divides_9 !a. lcm a a = a link to proof
natural-divides_10 !b. FST (egcd 0 b) = b link to proof
natural-divides_11 !a. lcm a 1 = a link to proof
natural-divides_12 !a. lcm 1 a = a link to proof
natural-divides_13 !a b. divides a (lcm a b) link to proof
natural-divides_14 !a b. divides b (lcm a b) link to proof
natural-divides_15 !a b. divides (gcd a b) a link to proof
natural-divides_16 !a b. divides (gcd a b) b link to proof
natural-divides_17 !a. divides 0 a <=> a = 0 link to proof
natural-divides_18 !a. gcd a 1 = 1 link to proof
natural-divides_19 !a. gcd 1 a = 1 link to proof
natural-divides_20 !a b. divides (FST (egcd a b)) a link to proof
natural-divides_21 !a b. divides (FST (egcd a b)) b link to proof
natural-divides_22 !a. divides 2 a <=> EVEN a link to proof
natural-divides_23 !a b. gcd a b = gcd b a link to proof
natural-divides_24 !a b. lcm a b = lcm b a link to proof
natural-divides_25 !a b. a = b ==> divides a b link to proof
natural-divides_26 !a. divides a 1 <=> a = 1 link to proof
natural-divides_27 !a b. FST (egcd a b) = gcd a b link to proof
natural-divides_28 !a. egcd a 0 = a,1,0 link to proof
natural-divides_29 !a b. gcd a b = a <=> divides a b link to proof
natural-divides_30 !a b. gcd b a = a <=> divides a b link to proof
natural-divides_31 !a b. lcm a b = a <=> divides b a link to proof
natural-divides_32 !a b. lcm b a = a <=> divides b a link to proof
natural-divides_33 !a b. gcd a (a + b) = gcd a b link to proof
natural-divides_34 !a b. gcd a (b + a) = gcd a b link to proof
natural-divides_35 !a b. gcd (a + b) b = gcd a b link to proof
natural-divides_36 !a b. gcd (b + a) b = gcd a b link to proof
natural-divides_37 !a b c. divides a b ==> divides a (b * c) link to proof
natural-divides_38 !a b c. divides a b ==> divides a (lcm b c) link to proof
natural-divides_39 !a b c. divides a b ==> divides a (lcm c b) link to proof
natural-divides_40 !a b c. divides a c ==> divides a (b * c) link to proof
natural-divides_41 !a b c. divides b a ==> divides (gcd b c) a link to proof
natural-divides_42 !a b c. divides b a ==> divides (gcd c b) a link to proof
natural-divides_43 !a b c. divides (a * b) c ==> divides a c link to proof
natural-divides_44 !a b c. divides (a * b) c ==> divides b c link to proof
natural-divides_45 !a b. divides a b <=> (?c. c * a = b) link to proof
natural-divides_46 !b. egcd 1 b = 1,1,0 link to proof
natural-divides_47 !a b. lcm a b * gcd a b = a * b link to proof
natural-divides_48 !a b. divides a b /\ divides b a ==> a = b link to proof
natural-divides_49 !a b. ~(b = 0) /\ divides a b ==> a <= b link to proof
natural-divides_50 !a b c. gcd (gcd a b) c = gcd a (gcd b c) link to proof
natural-divides_51 !a b c. lcm (lcm a b) c = lcm a (lcm b c) link to proof
natural-divides_52 !a b c. divides a b /\ divides b c ==> divides a c link to proof
natural-divides_53 !a b. (!c. divides b c ==> divides a c) <=> divides a b link to proof
natural-divides_54 !a b. (!c. divides c a ==> divides c b) <=> divides a b link to proof
natural-divides_55 !a b. (!c. divides b c ==> divides a c) ==> divides a b link to proof
natural-divides_56 !a b. (!c. divides c a ==> divides c b) ==> divides a b link to proof
natural-divides_57 !a b. a <= b ==> gcd a (b - a) = gcd a b link to proof
natural-divides_58 !a b. b <= a ==> gcd (a - b) b = gcd a b link to proof
natural-divides_59 !a b. gcd a b = 0 <=> a = 0 /\ b = 0 link to proof
natural-divides_60 !a b. lcm a b = 0 <=> a = 0 \/ b = 0 link to proof
natural-divides_61 !a b. ~(b = 0) /\ b <= a ==> divides b (FACT a) link to proof
natural-divides_62 !a b s t. divides (gcd a b) (dist (s * a) (t * b)) link to proof
natural-divides_63 !a b. ?s t. dist (s * a) (t * b) = gcd a b link to proof
natural-divides_64 !a b. ~(a = 0) ==> (divides a b <=> b MOD a = 0) link to proof
natural-divides_65 !a b. ~(a = 0) ==> gcd a (b MOD a) = gcd a b link to proof
natural-divides_66 !a b c. divides c (gcd a b) <=> divides c a /\ divides c b link to proof
natural-divides_67 !a b c. divides (lcm a b) c <=> divides a c /\ divides b c link to proof
natural-divides_68 !a b c. gcd a (lcm b c) = lcm (gcd a b) (gcd a c) link to proof
natural-divides_69 !a b c. lcm a (gcd b c) = gcd (lcm a b) (lcm a c) link to proof
natural-divides_70 !a b c. gcd (lcm b c) a = lcm (gcd b a) (gcd c a) link to proof
natural-divides_71 !a b c. lcm (gcd b c) a = gcd (lcm b a) (lcm c a) link to proof
natural-divides_72 !a b c. divides (gcd a (b * c)) (gcd a b * gcd a c) link to proof
natural-divides_73 !a b c. gcd (a * b) (a * c) = a * gcd b c link to proof
natural-divides_74 !a b c. gcd (b * a) (c * a) = gcd b c * a link to proof
natural-divides_75 !a b c. lcm (a * b) (a * c) = a * lcm b c link to proof
natural-divides_76 !a b c. lcm (b * a) (c * a) = lcm b c * a link to proof
natural-divides_77 !a b c. divides a b /\ divides a c ==> divides a (b + c) link to proof
natural-divides_78 !a b c. divides a c /\ divides b c ==> divides (lcm a b) c link to proof
natural-divides_79 !a b c. divides c a /\ divides c b ==> divides c (dist a b) link to proof
natural-divides_80 !a b c. divides c a /\ divides c b ==> divides c (gcd a b) link to proof
natural-divides_81 !a. divides a 2 <=> a = 1 \/ a = 2 link to proof
natural-divides_82 !a. divides a 3 <=> a = 1 \/ a = 3 link to proof
natural-divides_83 !a b. gcd a b = 1 ==> gcd (a * a) b = 1 link to proof
natural-divides_84 !a b. gcd b a = 1 ==> gcd b (a * a) = 1 link to proof
natural-divides_85 !a b. gcd b (a * a) = 1 <=> gcd b a = 1 link to proof
natural-divides_86 !a b. gcd (a * a) b = 1 <=> gcd a b = 1 link to proof
natural-divides_87 !a b. divides a b <=> (if a = 0 then b = 0 else b MOD a = 0) link to proof
natural-divides_88 !a b. ~(a = 0) ==> (divides a b <=> b DIV a * a = b) link to proof
natural-divides_89 !a b. lcm a b = 1 <=> a = 1 /\ b = 1 link to proof
natural-divides_90 !a b c. divides (a * b) (a * c) <=> a = 0 \/ divides b c link to proof
natural-divides_91 !a b c. divides (b * a) (c * a) <=> a = 0 \/ divides b c link to proof
natural-divides_92 !a b c. gcd b (a * c) = 1 ==> gcd b c = 1 link to proof
natural-divides_93 !a b c. gcd b (c * a) = 1 ==> gcd b c = 1 link to proof
natural-divides_94 !a b c. gcd (a * b) c = 1 ==> gcd b c = 1 link to proof
natural-divides_95 !a b c. gcd (b * a) c = 1 ==> gcd b c = 1 link to proof
natural-divides_96 !a b c. gcd a b = 1 ==> gcd a (b * c) = gcd a c link to proof
natural-divides_97 !a b c. gcd a b = 1 ==> gcd a (c * b) = gcd a c link to proof
natural-divides_98 !a b c. gcd b a = 1 ==> gcd (b * c) a = gcd c a link to proof
natural-divides_99 !a b c. gcd b a = 1 ==> gcd (c * b) a = gcd c a link to proof
natural-divides_100 !a b c d. divides a c /\ divides b d ==> divides (a * b) (c * d) link to proof
natural-divides_101 !a b c. c <= b /\ divides a b /\ divides a c ==> divides a (b - c) link to proof
natural-divides_102 !a. ~(a = 0) ==> egcd a 1 = 1,1,a - 1 link to proof
natural-divides_103 !a b. ~(a = 0) ==> (?s t. t * b + gcd a b = s * a) link to proof
natural-divides_104 !a b. ~(a = 0) ==> (?s t. t * b + gcd b a = s * a) link to proof
natural-divides_105 !a b x y. x < a /\ y < b ==> chinese a b x y < a * b link to proof
natural-divides_106 !a b s t. dist (s * a) (t * b) = 1 ==> gcd a b = 1 link to proof
natural-divides_107 !a b. (!c. divides c a /\ divides c b ==> c = 1) ==> gcd a b = 1 link to proof
natural-divides_108 !a b. gcd a b = (if a = 0 then b else if a <= b then gcd a (b - a) else gcd b a) link to proof
natural-divides_109 !a b c. gcd b c = 1 /\ divides b a /\ divides c a ==> divides (b * c) a link to proof
natural-divides_110 !a b. 1 < b /\ gcd a b = 1 ==> (?s. (s * a) MOD b = 1) link to proof
natural-divides_111 !a b. ?g. divides g a /\ divides g b /\ (!c. divides c a /\ divides c b ==> divides c g) link to proof
natural-divides_112 !a b c. gcd a (b * c) = 1 <=> gcd a b = 1 /\ gcd a c = 1 link to proof
natural-divides_113 !a b c. gcd (b * c) a = 1 <=> gcd b a = 1 /\ gcd c a = 1 link to proof
natural-divides_114 !a b c. gcd a b = 1 /\ gcd a c = 1 ==> gcd a (b * c) = 1 link to proof
natural-divides_115 !a b c. gcd b a = 1 /\ gcd c a = 1 ==> gcd (b * c) a = 1 link to proof
natural-divides_116 !ap b. let a = ap + 1 in let g,s,t = egcd a b in t < a link to proof
natural-divides_117 !a b s t g. s * a + g = t * b /\ divides g a /\ divides g b ==> gcd a b = g link to proof
natural-divides_118 !a b s t g. t * b + g = s * a /\ divides g a /\ divides g b ==> gcd a b = g link to proof
natural-divides_119 !a b s t g. dist (s * a) (t * b) = g /\ divides g a /\ divides g b ==> gcd a b = g link to proof
natural-divides_120 !ap b. let a = ap + 1 in let g,s,t = egcd a b in s < MAX b 2 link to proof
natural-divides_121 !a b l. divides a l /\ divides b l /\ (!c. divides a c /\ divides b c ==> divides l c) ==> lcm a b = l link to proof
natural-divides_122 !a b g. divides g a /\ divides g b /\ (!c. divides c a /\ divides c b ==> divides c g) ==> gcd a b = g link to proof
natural-divides_123 !a b g s t. ~(a = 0) /\ egcd a b = g,s,t ==> t * b + g = s * a link to proof
natural-divides_124 !ap b. let a = ap + 1 in let g,s,t = egcd a b in t * b + g = s * a link to proof
natural-divides_125 !a b g s t. ~(a = 0) /\ egcd a b = g,s,t ==> s < MAX b 2 /\ t < a link to proof
natural-divides_126 !a b. ~(a = 0) ==> (?s t. egcd a b = gcd a b,s,t /\ t * b + gcd a b = s * a) link to proof
natural-divides_127 !p. (!n. p 0 n) /\ (!m n. n < m /\ p n m ==> p m n) /\ (!m n. p m n ==> p m (n + m)) ==> (!m n. p m n) link to proof
natural-divides_128 !a b x y n. gcd a b = 1 /\ x < a /\ y < b /\ chinese a b x y = n ==> n MOD a = x /\ n MOD b = y link to proof
natural-divides_129 !ap bp xp yp. let aq = ap + 1 in let bq = bp + 1 in let g = FST (egcd aq bq) in let a = aq DIV g in let b = bq DIV g in let x = xp MOD a in let y = yp MOD b in chinese a b x y < a * b link to proof
natural-divides_130 !ap bp xp yp. let aq = ap + 1 in let bq = bp + 1 in let g = FST (egcd aq bq) in let a = aq DIV g in let b = bq DIV g in let x = xp MOD a in let y = yp MOD b in chinese a b x y MOD a = x link to proof
natural-divides_131 !ap bp xp yp. let aq = ap + 1 in let bq = bp + 1 in let g = FST (egcd aq bq) in let a = aq DIV g in let b = bq DIV g in let x = xp MOD a in let y = yp MOD b in chinese a b x y MOD b = y link to proof
natural-divides_132 !a b x y. chinese a b x y = (let g,s,t = egcd a b in (x * (a - t) * b + y * s * a) MOD (a * b)) link to proof
natural-divides_133 !a b. chinese a b = (let g,s,t = egcd a b in let ab = a * b in let sa = s * a in let tb = (a - t) * b in \x y. (x * tb + y * sa) MOD ab) link to proof
natural-divides_134 !p. p 0 0 /\ (!a b. gcd a b = 1 ==> p a b) /\ (!c a b. ~(c = 0) /\ p a b ==> p (c * a) (c * b)) ==> (!a b. p a b) link to proof
natural-divides_135 !p. (!a. p a 0) /\ (!a b. ~(b = 0) /\ divides b a ==> p a b) /\ (!a b c. ~(b = 0) /\ c = a MOD b /\ ~(c = 0) /\ p c (b MOD c) ==> p a b) ==> (!a b. p a b) link to proof
natural-divides_136 !a b. egcd a b = (if b = 0 then a,1,0 else let c = a MOD b in if c = 0 then b,1,a DIV b - 1 else let g,s,t = egcd c (b MOD c) in let u = s + b DIV c * t in g,u,t + a DIV b * u) link to proof
Back to ProofCloud main page