Greatest common divisor

Symbol: GCD —

\gcd\!\left(a, b\right)

— Greatest common divisor

The greatest common divisor function can be called either with with an arbitrary number of integer arguments or with a single finite set of integers as the argument. The current entries only deal with the case of two arguments.

Domain	Codomain
$a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}$	$\gcd\!\left(a, b\right) \in \mathbb{Z}_{\ge 0}$
$S \in \mathscr{P}\!\left(\mathbb{Z}\right) \,\mathbin{\operatorname{and}}\, \left\|S\right\| \lt \left\|\mathbb{Z}\right\|$	$\gcd\!\left(S\right) \in \mathbb{Z}_{\ge 0}$

Table data:

\left(P, Q\right)

such that

\left(P\right) \implies \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`PowerSet`	$\mathscr{P}\!\left(S\right)$	Power set
`Cardinality`	$\left\|S\right\|$	Set cardinality

Source code for this entry:

Entry(ID("287e28"),
    SymbolDefinition(GCD, GCD(a, b), "Greatest common divisor"),
    Description("The greatest common divisor function can be called either with with an arbitrary number of integer arguments or with a single finite set of integers as the argument. The current entries only deal with the case of two arguments."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(a, ZZ), Element(b, ZZ)), Element(GCD(a, b), ZZGreaterEqual(0))), Tuple(And(Element(S, PowerSet(ZZ)), Less(Cardinality(S), Cardinality(ZZ))), Element(GCD(S), ZZGreaterEqual(0))))))

c03ed9

Symbol: LCM —

\operatorname{lcm}\!\left(a, b\right)

— Least common multiple

The least common multiple function can be called either with with an arbitrary number of integer arguments or with a single finite set of integers as the argument. The current entries only deal with the case of two arguments.

Domain	Codomain
$a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}$	$\operatorname{lcm}\!\left(a, b\right) \in \mathbb{Z}_{\ge 0}$
$S \in \mathscr{P}\!\left(\mathbb{Z}\right) \,\mathbin{\operatorname{and}}\, \left\|S\right\| \lt \left\|\mathbb{Z}\right\|$	$\operatorname{lcm}\!\left(S\right) \in \mathbb{Z}_{\ge 0}$

Table data:

\left(P, Q\right)

such that

\left(P\right) \implies \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`PowerSet`	$\mathscr{P}\!\left(S\right)$	Power set
`Cardinality`	$\left\|S\right\|$	Set cardinality

Source code for this entry:

Entry(ID("c03ed9"),
    SymbolDefinition(LCM, LCM(a, b), "Least common multiple"),
    Description("The least common multiple function can be called either with with an arbitrary number of integer arguments or with a single finite set of integers as the argument. The current entries only deal with the case of two arguments."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(a, ZZ), Element(b, ZZ)), Element(LCM(a, b), ZZGreaterEqual(0))), Tuple(And(Element(S, PowerSet(ZZ)), Less(Cardinality(S), Cardinality(ZZ))), Element(LCM(S), ZZGreaterEqual(0))))))

5daceb

Symbol: XGCD —

\operatorname{xgcd}\!\left(a, b\right)

— Extended greatest common divisor

Domain	Codomain
$a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}$	$d \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, u \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, v \in \mathbb{Z}\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)$

Table data:

\left(P, Q\right)

such that

\left(P\right) \implies \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("5daceb"),
    SymbolDefinition(XGCD, XGCD(a, b), "Extended greatest common divisor"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(a, ZZ), Element(b, ZZ)), Where(And(Element(d, ZZGreaterEqual(0)), Element(u, ZZ), Element(v, ZZ)), Equal(Tuple(d, u, v), XGCD(a, b)))))))

8b2743

Table of

\gcd\!\left(n, k\right)

for

0 \le n \le 15

and

0 \le k \le 15

$n$ \ $k$	0	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15
0	0	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15
1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1
2	2	1	2	1	2	1	2	1	2	1	2	1	2	1	2	1
3	3	1	1	3	1	1	3	1	1	3	1	1	3	1	1	3
4	4	1	2	1	4	1	2	1	4	1	2	1	4	1	2	1
5	5	1	1	1	1	5	1	1	1	1	5	1	1	1	1	5
6	6	1	2	3	2	1	6	1	2	3	2	1	6	1	2	3
7	7	1	1	1	1	1	1	7	1	1	1	1	1	1	7	1
8	8	1	2	1	4	1	2	1	8	1	2	1	4	1	2	1
9	9	1	1	3	1	1	3	1	1	9	1	1	3	1	1	3
10	10	1	2	1	2	5	2	1	2	1	10	1	2	1	2	5
11	11	1	1	1	1	1	1	1	1	1	1	11	1	1	1	1
12	12	1	2	3	4	1	6	1	4	3	2	1	12	1	2	3
13	13	1	1	1	1	1	1	1	1	1	1	1	1	13	1	1
14	14	1	2	1	2	1	2	7	2	1	2	1	2	1	14	1
15	15	1	1	3	1	5	3	1	1	3	5	1	3	1	1	15

Table data:

\left(n, k, y\right)

such that

\gcd\!\left(n, k\right) = y

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor

Source code for this entry:

Entry(ID("8b2743"),
    Description("Table of", GCD(n, k), "for", LessEqual(0, n, 15), "and", LessEqual(0, k, 15)),
    Table(TableRelation(Tuple(n, k, y), Equal(GCD(n, k), y)), TableHeadings(Description(n, "\", k), 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), TableColumnHeadings(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), List(Tuple(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), Tuple(1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1), Tuple(2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1), Tuple(3, 1, 1, 3, 1, 1, 3, 1, 1, 3, 1, 1, 3, 1, 1, 3), Tuple(4, 1, 2, 1, 4, 1, 2, 1, 4, 1, 2, 1, 4, 1, 2, 1), Tuple(5, 1, 1, 1, 1, 5, 1, 1, 1, 1, 5, 1, 1, 1, 1, 5), Tuple(6, 1, 2, 3, 2, 1, 6, 1, 2, 3, 2, 1, 6, 1, 2, 3), Tuple(7, 1, 1, 1, 1, 1, 1, 7, 1, 1, 1, 1, 1, 1, 7, 1), Tuple(8, 1, 2, 1, 4, 1, 2, 1, 8, 1, 2, 1, 4, 1, 2, 1), Tuple(9, 1, 1, 3, 1, 1, 3, 1, 1, 9, 1, 1, 3, 1, 1, 3), Tuple(10, 1, 2, 1, 2, 5, 2, 1, 2, 1, 10, 1, 2, 1, 2, 5), Tuple(11, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 11, 1, 1, 1, 1), Tuple(12, 1, 2, 3, 4, 1, 6, 1, 4, 3, 2, 1, 12, 1, 2, 3), Tuple(13, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 13, 1, 1), Tuple(14, 1, 2, 1, 2, 1, 2, 7, 2, 1, 2, 1, 2, 1, 14, 1), Tuple(15, 1, 1, 3, 1, 5, 3, 1, 1, 3, 5, 1, 3, 1, 1, 15))))

a0d13f

Table of

\operatorname{lcm}\!\left(n, k\right)

for

0 \le n \le 15

and

0 \le k \le 15

$n$ \ $k$	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15
0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
1	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15
2	2	2	6	4	10	6	14	8	18	10	22	12	26	14	30
3	3	6	3	12	15	6	21	24	9	30	33	12	39	42	15
4	4	4	12	4	20	12	28	8	36	20	44	12	52	28	60
5	5	10	15	20	5	30	35	40	45	10	55	60	65	70	15
6	6	6	6	12	30	6	42	24	18	30	66	12	78	42	30
7	7	14	21	28	35	42	7	56	63	70	77	84	91	14	105
8	8	8	24	8	40	24	56	8	72	40	88	24	104	56	120
9	9	18	9	36	45	18	63	72	9	90	99	36	117	126	45
10	10	10	30	20	10	30	70	40	90	10	110	60	130	70	30
11	11	22	33	44	55	66	77	88	99	110	11	132	143	154	165
12	12	12	12	12	60	12	84	24	36	60	132	12	156	84	60
13	13	26	39	52	65	78	91	104	117	130	143	156	13	182	195
14	14	14	42	28	70	42	14	56	126	70	154	84	182	14	210
15	15	30	15	60	15	30	105	120	45	30	165	60	195	210	15

Table data:

\left(n, k, y\right)

such that

\operatorname{lcm}\!\left(n, k\right) = y

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple

Source code for this entry:

Entry(ID("a0d13f"),
    Description("Table of", LCM(n, k), "for", LessEqual(0, n, 15), "and", LessEqual(0, k, 15)),
    Table(TableRelation(Tuple(n, k, y), Equal(LCM(n, k), y)), TableHeadings(Description(n, "\", k), 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), TableColumnHeadings(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), List(Tuple(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), Tuple(0, 2, 2, 6, 4, 10, 6, 14, 8, 18, 10, 22, 12, 26, 14, 30), Tuple(0, 3, 6, 3, 12, 15, 6, 21, 24, 9, 30, 33, 12, 39, 42, 15), Tuple(0, 4, 4, 12, 4, 20, 12, 28, 8, 36, 20, 44, 12, 52, 28, 60), Tuple(0, 5, 10, 15, 20, 5, 30, 35, 40, 45, 10, 55, 60, 65, 70, 15), Tuple(0, 6, 6, 6, 12, 30, 6, 42, 24, 18, 30, 66, 12, 78, 42, 30), Tuple(0, 7, 14, 21, 28, 35, 42, 7, 56, 63, 70, 77, 84, 91, 14, 105), Tuple(0, 8, 8, 24, 8, 40, 24, 56, 8, 72, 40, 88, 24, 104, 56, 120), Tuple(0, 9, 18, 9, 36, 45, 18, 63, 72, 9, 90, 99, 36, 117, 126, 45), Tuple(0, 10, 10, 30, 20, 10, 30, 70, 40, 90, 10, 110, 60, 130, 70, 30), Tuple(0, 11, 22, 33, 44, 55, 66, 77, 88, 99, 110, 11, 132, 143, 154, 165), Tuple(0, 12, 12, 12, 12, 60, 12, 84, 24, 36, 60, 132, 12, 156, 84, 60), Tuple(0, 13, 26, 39, 52, 65, 78, 91, 104, 117, 130, 143, 156, 13, 182, 195), Tuple(0, 14, 14, 42, 28, 70, 42, 14, 56, 126, 70, 154, 84, 182, 14, 210), Tuple(0, 15, 30, 15, 60, 15, 30, 105, 120, 45, 30, 165, 60, 195, 210, 15))))

99dc4a

Table of

\operatorname{xgcd}\!\left(n, k\right)

for

0 \le n \le 10

and

0 \le k \le 10

$n$ \ $k$	0	1	2	3	4	5	6	7	8	9	10
0	(0, 0, 0)	(1, 0, 1)	(2, 0, 1)	(3, 0, 1)	(4, 0, 1)	(5, 0, 1)	(6, 0, 1)	(7, 0, 1)	(8, 0, 1)	(9, 0, 1)	(10, 0, 1)
1	(1, 1, 0)	(1, 0, 1)	(1, 1, 0)	(1, 1, 0)	(1, 1, 0)	(1, 1, 0)	(1, 1, 0)	(1, 1, 0)	(1, 1, 0)	(1, 1, 0)	(1, 1, 0)
2	(2, 1, 0)	(1, 0, 1)	(2, 0, 1)	(1, -1, 1)	(2, 1, 0)	(1, -2, 1)	(2, 1, 0)	(1, -3, 1)	(2, 1, 0)	(1, -4, 1)	(2, 1, 0)
3	(3, 1, 0)	(1, 0, 1)	(1, 1, -1)	(3, 0, 1)	(1, -1, 1)	(1, 2, -1)	(3, 1, 0)	(1, -2, 1)	(1, 3, -1)	(3, 1, 0)	(1, -3, 1)
4	(4, 1, 0)	(1, 0, 1)	(2, 0, 1)	(1, 1, -1)	(4, 0, 1)	(1, -1, 1)	(2, -1, 1)	(1, 2, -1)	(4, 1, 0)	(1, -2, 1)	(2, -2, 1)
5	(5, 1, 0)	(1, 0, 1)	(1, 1, -2)	(1, -1, 2)	(1, 1, -1)	(5, 0, 1)	(1, -1, 1)	(1, 3, -2)	(1, -3, 2)	(1, 2, -1)	(5, 1, 0)
6	(6, 1, 0)	(1, 0, 1)	(2, 0, 1)	(3, 0, 1)	(2, 1, -1)	(1, 1, -1)	(6, 0, 1)	(1, -1, 1)	(2, -1, 1)	(3, -1, 1)	(2, 2, -1)
7	(7, 1, 0)	(1, 0, 1)	(1, 1, -3)	(1, 1, -2)	(1, -1, 2)	(1, -2, 3)	(1, 1, -1)	(7, 0, 1)	(1, -1, 1)	(1, 4, -3)	(1, 3, -2)
8	(8, 1, 0)	(1, 0, 1)	(2, 0, 1)	(1, -1, 3)	(4, 0, 1)	(1, 2, -3)	(2, 1, -1)	(1, 1, -1)	(8, 0, 1)	(1, -1, 1)	(2, -1, 1)
9	(9, 1, 0)	(1, 0, 1)	(1, 1, -4)	(3, 0, 1)	(1, 1, -2)	(1, -1, 2)	(3, 1, -1)	(1, -3, 4)	(1, 1, -1)	(9, 0, 1)	(1, -1, 1)
10	(10, 1, 0)	(1, 0, 1)	(2, 0, 1)	(1, 1, -3)	(2, 1, -2)	(5, 0, 1)	(2, -1, 2)	(1, -2, 3)	(2, 1, -1)	(1, 1, -1)	(10, 0, 1)

Table data:

\left(n, k, \left(d, u, v\right)\right)

such that

\operatorname{xgcd}\!\left(n, k\right) = \left(d, u, v\right)

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor

Source code for this entry:

Entry(ID("99dc4a"),
    Description("Table of", XGCD(n, k), "for", LessEqual(0, n, 10), "and", LessEqual(0, k, 10)),
    Table(TableRelation(Tuple(n, k, Tuple(d, u, v)), Equal(XGCD(n, k), Tuple(d, u, v))), TableHeadings(Description(n, "\", k), 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10), TableColumnHeadings(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10), List(Tuple(Tuple(0, 0, 0), Tuple(1, 0, 1), Tuple(2, 0, 1), Tuple(3, 0, 1), Tuple(4, 0, 1), Tuple(5, 0, 1), Tuple(6, 0, 1), Tuple(7, 0, 1), Tuple(8, 0, 1), Tuple(9, 0, 1), Tuple(10, 0, 1)), Tuple(Tuple(1, 1, 0), Tuple(1, 0, 1), Tuple(1, 1, 0), Tuple(1, 1, 0), Tuple(1, 1, 0), Tuple(1, 1, 0), Tuple(1, 1, 0), Tuple(1, 1, 0), Tuple(1, 1, 0), Tuple(1, 1, 0), Tuple(1, 1, 0)), Tuple(Tuple(2, 1, 0), Tuple(1, 0, 1), Tuple(2, 0, 1), Tuple(1, -1, 1), Tuple(2, 1, 0), Tuple(1, -2, 1), Tuple(2, 1, 0), Tuple(1, -3, 1), Tuple(2, 1, 0), Tuple(1, -4, 1), Tuple(2, 1, 0)), Tuple(Tuple(3, 1, 0), Tuple(1, 0, 1), Tuple(1, 1, -1), Tuple(3, 0, 1), Tuple(1, -1, 1), Tuple(1, 2, -1), Tuple(3, 1, 0), Tuple(1, -2, 1), Tuple(1, 3, -1), Tuple(3, 1, 0), Tuple(1, -3, 1)), Tuple(Tuple(4, 1, 0), Tuple(1, 0, 1), Tuple(2, 0, 1), Tuple(1, 1, -1), Tuple(4, 0, 1), Tuple(1, -1, 1), Tuple(2, -1, 1), Tuple(1, 2, -1), Tuple(4, 1, 0), Tuple(1, -2, 1), Tuple(2, -2, 1)), Tuple(Tuple(5, 1, 0), Tuple(1, 0, 1), Tuple(1, 1, -2), Tuple(1, -1, 2), Tuple(1, 1, -1), Tuple(5, 0, 1), Tuple(1, -1, 1), Tuple(1, 3, -2), Tuple(1, -3, 2), Tuple(1, 2, -1), Tuple(5, 1, 0)), Tuple(Tuple(6, 1, 0), Tuple(1, 0, 1), Tuple(2, 0, 1), Tuple(3, 0, 1), Tuple(2, 1, -1), Tuple(1, 1, -1), Tuple(6, 0, 1), Tuple(1, -1, 1), Tuple(2, -1, 1), Tuple(3, -1, 1), Tuple(2, 2, -1)), Tuple(Tuple(7, 1, 0), Tuple(1, 0, 1), Tuple(1, 1, -3), Tuple(1, 1, -2), Tuple(1, -1, 2), Tuple(1, -2, 3), Tuple(1, 1, -1), Tuple(7, 0, 1), Tuple(1, -1, 1), Tuple(1, 4, -3), Tuple(1, 3, -2)), Tuple(Tuple(8, 1, 0), Tuple(1, 0, 1), Tuple(2, 0, 1), Tuple(1, -1, 3), Tuple(4, 0, 1), Tuple(1, 2, -3), Tuple(2, 1, -1), Tuple(1, 1, -1), Tuple(8, 0, 1), Tuple(1, -1, 1), Tuple(2, -1, 1)), Tuple(Tuple(9, 1, 0), Tuple(1, 0, 1), Tuple(1, 1, -4), Tuple(3, 0, 1), Tuple(1, 1, -2), Tuple(1, -1, 2), Tuple(3, 1, -1), Tuple(1, -3, 4), Tuple(1, 1, -1), Tuple(9, 0, 1), Tuple(1, -1, 1)), Tuple(Tuple(10, 1, 0), Tuple(1, 0, 1), Tuple(2, 0, 1), Tuple(1, 1, -3), Tuple(2, 1, -2), Tuple(5, 0, 1), Tuple(2, -1, 2), Tuple(1, -2, 3), Tuple(2, 1, -1), Tuple(1, 1, -1), Tuple(10, 0, 1)))))

6880d0

\gcd\!\left(a, b\right) = \max\left(\left\{ d : d \in \mathbb{Z}_{\ge 1} \,\mathbin{\operatorname{and}}\, d \mid a \,\mathbin{\operatorname{and}}\, d \mid b \right\}\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

\gcd\!\left(a, b\right) = \max\left(\left\{ d : d \in \mathbb{Z}_{\ge 1} \,\mathbin{\operatorname{and}}\, d \mid a \,\mathbin{\operatorname{and}}\, d \mid b \right\}\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Maximum`	$\mathop{\max}\limits_{P\left(x\right)} f\!\left(x\right)$	Maximum value of a set or function
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("6880d0"),
    Formula(Equal(GCD(a, b), Maximum(SetBuilder(d, d, And(Element(d, ZZGreaterEqual(1)), Divides(d, a), Divides(d, b)))))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

805c7a

\operatorname{lcm}\!\left(a, b\right) = \min\left(\left\{ m : m \in \mathbb{Z}_{\ge 1} \,\mathbin{\operatorname{and}}\, a \mid m \,\mathbin{\operatorname{and}}\, b \mid m \right\}\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\operatorname{lcm}\!\left(a, b\right) = \min\left(\left\{ m : m \in \mathbb{Z}_{\ge 1} \,\mathbin{\operatorname{and}}\, a \mid m \,\mathbin{\operatorname{and}}\, b \mid m \right\}\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Minimum`	$\mathop{\min}\limits_{P\left(x\right)} f\!\left(x\right)$	Minimum value of a set or function
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("805c7a"),
    Formula(Equal(LCM(a, b), Minimum(SetBuilder(m, m, And(Element(m, ZZGreaterEqual(1)), Divides(a, m), Divides(b, m)))))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

7638c5

\left(d \mid a \,\mathbin{\operatorname{and}}\, d \mid b\right) \implies \left(d \mid \gcd\!\left(a, b\right)\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z}

TeX:

\left(d \mid a \,\mathbin{\operatorname{and}}\, d \mid b\right) \implies \left(d \mid \gcd\!\left(a, b\right)\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("7638c5"),
    Formula(Implies(And(Divides(d, a), Divides(d, b)), Divides(d, GCD(a, b)))),
    Variables(a, b, d),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(d, ZZ))))

3605cc

\left(a \mid m \,\mathbin{\operatorname{and}}\, b \mid m\right) \implies \left(\operatorname{lcm}\!\left(a, b\right) \mid m\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z}

TeX:

\left(a \mid m \,\mathbin{\operatorname{and}}\, b \mid m\right) \implies \left(\operatorname{lcm}\!\left(a, b\right) \mid m\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("3605cc"),
    Formula(Implies(And(Divides(a, m), Divides(b, m)), Divides(LCM(a, b), m))),
    Variables(a, b, d),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(d, ZZ))))

5d03d2

\left(d \mid a \,\mathbin{\operatorname{or}}\, d \mid b\right) \implies \left(d \mid \operatorname{lcm}\!\left(a, b\right)\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z}

TeX:

\left(d \mid a \,\mathbin{\operatorname{or}}\, d \mid b\right) \implies \left(d \mid \operatorname{lcm}\!\left(a, b\right)\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("5d03d2"),
    Formula(Implies(Or(Divides(d, a), Divides(d, b)), Divides(d, LCM(a, b)))),
    Variables(a, b, d),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(d, ZZ))))

a9c81e

\gcd\!\left(a, b\right) \mid a

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

\gcd\!\left(a, b\right) \mid a

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("a9c81e"),
    Formula(Divides(GCD(a, b), a)),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

272bc8

\gcd\!\left(a, b\right) \mid b

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

\gcd\!\left(a, b\right) \mid b

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("272bc8"),
    Formula(Divides(GCD(a, b), b)),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

67978f

a \mid \operatorname{lcm}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

a \mid \operatorname{lcm}\!\left(a, b\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("67978f"),
    Formula(Divides(a, LCM(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, ZZ))))

4f1441

b \mid \operatorname{lcm}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

b \mid \operatorname{lcm}\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("4f1441"),
    Formula(Divides(b, LCM(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, SetMinus(ZZ, Set(0))))))

65cfe5

\operatorname{lcm}\!\left(a, b\right) \mid a b

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{and}}\, b \ne 0\right)

TeX:

\operatorname{lcm}\!\left(a, b\right) \mid a b

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{and}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("65cfe5"),
    Formula(Divides(LCM(a, b), Mul(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), And(Unequal(a, 0), Unequal(b, 0)))))

b60924

\gcd\!\left(a, b\right) \mid a b

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

\gcd\!\left(a, b\right) \mid a b

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("b60924"),
    Formula(Divides(GCD(a, b), Mul(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

1277f6

\gcd\!\left(a, b\right) \mid \operatorname{lcm}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{and}}\, b \ne 0\right)

TeX:

\gcd\!\left(a, b\right) \mid \operatorname{lcm}\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{and}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("1277f6"),
    Formula(Divides(GCD(a, b), LCM(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), And(Unequal(a, 0), Unequal(b, 0)))))

e3392b

\gcd\!\left(a, b\right) \mid a + b

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

\gcd\!\left(a, b\right) \mid a + b

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("e3392b"),
    Formula(Divides(GCD(a, b), Add(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

663d9c

\gcd\!\left(a, b\right) \mid a x + b y

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, x \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, y \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

\gcd\!\left(a, b\right) \mid a x + b y

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, x \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, y \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("663d9c"),
    Formula(Divides(GCD(a, b), Add(Mul(a, x), Mul(b, y)))),
    Variables(a, b, x, y),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(x, ZZ), Element(y, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

be5fcd

\gcd\!\left(a, b\right) = d = a u + b v\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a, b\right) = d = a u + b v\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("be5fcd"),
    Formula(Where(Equal(GCD(a, b), d, Add(Mul(a, u), Mul(b, v))), Equal(Tuple(d, u, v), XGCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

965ac0

\left\{ a x + b y : x \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, y \in \mathbb{Z} \right\} = \left\{ n d : n \in \mathbb{Z} \right\}\; \text{ where } d = \gcd\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\left\{ a x + b y : x \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, y \in \mathbb{Z} \right\} = \left\{ n d : n \in \mathbb{Z} \right\}\; \text{ where } d = \gcd\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`ZZ`	$\mathbb{Z}$	Integers
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor

Source code for this entry:

Entry(ID("965ac0"),
    Formula(Where(Equal(SetBuilder(Add(Mul(a, x), Mul(b, y)), Tuple(x, y), And(Element(x, ZZ), Element(y, ZZ))), SetBuilder(Mul(n, d), n, Element(n, ZZ))), Equal(d, GCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

e922c4

\gcd\!\left(a, b\right) = \min\left(\left\{ a x + b y : x \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, y \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, a x + b y \ge 1 \right\}\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

\gcd\!\left(a, b\right) = \min\left(\left\{ a x + b y : x \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, y \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, a x + b y \ge 1 \right\}\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Minimum`	$\mathop{\min}\limits_{P\left(x\right)} f\!\left(x\right)$	Minimum value of a set or function
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("e922c4"),
    Formula(Equal(GCD(a, b), Minimum(SetBuilder(Add(Mul(a, x), Mul(b, y)), Tuple(x, y), And(Element(x, ZZ), Element(y, ZZ), GreaterEqual(Add(Mul(a, x), Mul(b, y)), 1)))))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

f20503

d = a x + b y\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right),\,\left(x, y\right) = \left(u + \frac{k b}{d}, v - \frac{k a}{d}\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, k \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

d = a x + b y\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right),\,\left(x, y\right) = \left(u + \frac{k b}{d}, v - \frac{k a}{d}\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, k \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("f20503"),
    Formula(Where(Equal(d, Add(Mul(a, x), Mul(b, y))), Equal(Tuple(d, u, v), XGCD(a, b)), Equal(Tuple(x, y), Tuple(Add(u, Div(Mul(k, b), d)), Sub(v, Div(Mul(k, a), d)))))),
    Variables(a, b, k),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(k, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

4d3127

\gcd\!\left(a, b\right) \operatorname{lcm}\!\left(a, b\right) = \left|a b\right|

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a, b\right) \operatorname{lcm}\!\left(a, b\right) = \left|a b\right|

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("4d3127"),
    Formula(Equal(Mul(GCD(a, b), LCM(a, b)), Abs(Mul(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

6572c5

\gcd\!\left(a, b\right) = \frac{\left|a b\right|}{\operatorname{lcm}\!\left(a, b\right)}

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, a \ne 0 \,\mathbin{\operatorname{and}}\, b \ne 0

TeX:

\gcd\!\left(a, b\right) = \frac{\left|a b\right|}{\operatorname{lcm}\!\left(a, b\right)}

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, a \ne 0 \,\mathbin{\operatorname{and}}\, b \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("6572c5"),
    Formula(Equal(GCD(a, b), Div(Abs(Mul(a, b)), LCM(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Unequal(a, 0), Unequal(b, 0))))

927e6e

\operatorname{lcm}\!\left(a, b\right) = \frac{\left|a b\right|}{\gcd\!\left(a, b\right)}

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

TeX:

\operatorname{lcm}\!\left(a, b\right) = \frac{\left|a b\right|}{\gcd\!\left(a, b\right)}

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \left(a \ne 0 \,\mathbin{\operatorname{or}}\, b \ne 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("927e6e"),
    Formula(Equal(LCM(a, b), Div(Abs(Mul(a, b)), GCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Or(Unequal(a, 0), Unequal(b, 0)))))

126f3e

\gcd\!\left(a, b\right) = d\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a, b\right) = d\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("126f3e"),
    Formula(Equal(GCD(a, b), Where(d, Equal(Tuple(d, u, v), XGCD(a, b))))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

19ceaa

\gcd\!\left(0, 0\right) = 0

TeX:

\gcd\!\left(0, 0\right) = 0

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor

Source code for this entry:

Entry(ID("19ceaa"),
    Formula(Equal(GCD(0, 0), 0)))

af512f

\operatorname{lcm}\!\left(0, 0\right) = 0

TeX:

\operatorname{lcm}\!\left(0, 0\right) = 0

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple

Source code for this entry:

Entry(ID("af512f"),
    Formula(Equal(LCM(0, 0), 0)))

554b2e

\gcd\!\left(1, 1\right) = 1

TeX:

\gcd\!\left(1, 1\right) = 1

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor

Source code for this entry:

Entry(ID("554b2e"),
    Formula(Equal(GCD(1, 1), 1)))

34378a

\operatorname{lcm}\!\left(1, 1\right) = 1

TeX:

\operatorname{lcm}\!\left(1, 1\right) = 1

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple

Source code for this entry:

Entry(ID("34378a"),
    Formula(Equal(LCM(1, 1), 1)))

c40be0

\gcd\!\left(a, 0\right) = \left|a\right|

Assumptions:

a \in \mathbb{Z}

TeX:

\gcd\!\left(a, 0\right) = \left|a\right|

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("c40be0"),
    Formula(Equal(GCD(a, 0), Abs(a))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

0a7aff

\operatorname{lcm}\!\left(a, 0\right) = 0

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, 0\right) = 0

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("0a7aff"),
    Formula(Equal(LCM(a, 0), 0)),
    Variables(a),
    Assumptions(Element(a, ZZ)))

720766

\gcd\!\left(a, 1\right) = 1

Assumptions:

a \in \mathbb{Z}

TeX:

\gcd\!\left(a, 1\right) = 1

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("720766"),
    Formula(Equal(GCD(a, 1), 1)),
    Variables(a),
    Assumptions(Element(a, ZZ)))

8d90e9

\operatorname{lcm}\!\left(a, 1\right) = \left|a\right|

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, 1\right) = \left|a\right|

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("8d90e9"),
    Formula(Equal(LCM(a, 1), Abs(a))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

0f26cc

\gcd\!\left(a, a\right) = \left|a\right|

Assumptions:

a \in \mathbb{Z}

TeX:

\gcd\!\left(a, a\right) = \left|a\right|

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("0f26cc"),
    Formula(Equal(GCD(a, a), Abs(a))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

c6631e

\operatorname{lcm}\!\left(a, a\right) = \left|a\right|

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, a\right) = \left|a\right|

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("c6631e"),
    Formula(Equal(LCM(a, a), Abs(a))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

5fb5e2

\gcd\!\left(a, 2\right) = 1 + \frac{1 + {\left(-1\right)}^{a}}{2}

Assumptions:

a \in \mathbb{Z}

TeX:

\gcd\!\left(a, 2\right) = 1 + \frac{1 + {\left(-1\right)}^{a}}{2}

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Pow`	${a}^{b}$	Power
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("5fb5e2"),
    Formula(Equal(GCD(a, 2), Add(1, Div(Add(1, Pow(-1, a)), 2)))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

157c33

\operatorname{lcm}\!\left(a, 2\right) = \left|a\right| \left(1 + \frac{1 - {\left(-1\right)}^{a}}{2}\right)

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, 2\right) = \left|a\right| \left(1 + \frac{1 - {\left(-1\right)}^{a}}{2}\right)

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`Pow`	${a}^{b}$	Power
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("157c33"),
    Formula(Equal(LCM(a, 2), Mul(Abs(a), Add(1, Div(Sub(1, Pow(-1, a)), 2))))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

c70178

\gcd\!\left(a, a - 1\right) = 1

Assumptions:

a \in \mathbb{Z}

TeX:

\gcd\!\left(a, a - 1\right) = 1

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("c70178"),
    Formula(Equal(GCD(a, Sub(a, 1)), 1)),
    Variables(a),
    Assumptions(Element(a, ZZ)))

e19e40

\operatorname{lcm}\!\left(a, a - 1\right) = a \left(a - 1\right)

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, a - 1\right) = a \left(a - 1\right)

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("e19e40"),
    Formula(Equal(LCM(a, Sub(a, 1)), Mul(a, Sub(a, 1)))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

80f20f

\gcd\!\left(a, a - 2\right) = 1 + \frac{1 + {\left(-1\right)}^{a}}{2}

Assumptions:

a \in \mathbb{Z}

TeX:

\gcd\!\left(a, a - 2\right) = 1 + \frac{1 + {\left(-1\right)}^{a}}{2}

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Pow`	${a}^{b}$	Power
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("80f20f"),
    Formula(Equal(GCD(a, Sub(a, 2)), Add(1, Div(Add(1, Pow(-1, a)), 2)))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

7a1799

\operatorname{lcm}\!\left(a, a - 2\right) = \frac{\left|a \left(a - 2\right)\right|}{2} \left(1 + \frac{1 - {\left(-1\right)}^{a}}{2}\right)

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, a - 2\right) = \frac{\left|a \left(a - 2\right)\right|}{2} \left(1 + \frac{1 - {\left(-1\right)}^{a}}{2}\right)

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`Pow`	${a}^{b}$	Power
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("7a1799"),
    Formula(Equal(LCM(a, Sub(a, 2)), Mul(Div(Abs(Mul(a, Sub(a, 2))), 2), Add(1, Div(Sub(1, Pow(-1, a)), 2))))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

e352ca

\operatorname{xgcd}\!\left(a, 0\right) = \left(\left|a\right|, \operatorname{sgn}\!\left(a\right), 0\right)

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{xgcd}\!\left(a, 0\right) = \left(\left|a\right|, \operatorname{sgn}\!\left(a\right), 0\right)

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("e352ca"),
    Formula(Equal(XGCD(a, 0), Tuple(Abs(a), Sign(a), 0))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

6fd925

\operatorname{xgcd}\!\left(0, b\right) = \left(\left|b\right|, 0, \operatorname{sgn}\!\left(b\right)\right)

Assumptions:

b \in \mathbb{Z}

TeX:

\operatorname{xgcd}\!\left(0, b\right) = \left(\left|b\right|, 0, \operatorname{sgn}\!\left(b\right)\right)

b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("6fd925"),
    Formula(Equal(XGCD(0, b), Tuple(Abs(b), 0, Sign(b)))),
    Variables(b),
    Assumptions(Element(b, ZZ)))

13ed5e

\operatorname{xgcd}\!\left(a, 1\right) = \left(1, 0, 1\right)

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{xgcd}\!\left(a, 1\right) = \left(1, 0, 1\right)

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("13ed5e"),
    Formula(Equal(XGCD(a, 1), Tuple(1, 0, 1))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

bf877e

\operatorname{xgcd}\!\left(1, b\right) = \left(1, \left|\operatorname{sgn}\!\left(\left(b - 1\right) \left(b + 1\right)\right)\right|, \operatorname{sgn}\!\left(b\right) \left(\operatorname{sgn}\!\left(b + 1\right) - \operatorname{sgn}\!\left(b - 1\right)\right)\right)

Assumptions:

b \in \mathbb{Z}

TeX:

\operatorname{xgcd}\!\left(1, b\right) = \left(1, \left|\operatorname{sgn}\!\left(\left(b - 1\right) \left(b + 1\right)\right)\right|, \operatorname{sgn}\!\left(b\right) \left(\operatorname{sgn}\!\left(b + 1\right) - \operatorname{sgn}\!\left(b - 1\right)\right)\right)

b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("bf877e"),
    Formula(Equal(XGCD(1, b), Tuple(1, Abs(Sign(Mul(Sub(b, 1), Add(b, 1)))), Mul(Sign(b), Sub(Sign(Add(b, 1)), Sign(Sub(b, 1))))))),
    Variables(b),
    Assumptions(Element(b, ZZ)))

945be9

\operatorname{xgcd}\!\left(a, a\right) = \left(\left|a\right|, 0, \operatorname{sgn}\!\left(a\right)\right)

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{xgcd}\!\left(a, a\right) = \left(\left|a\right|, 0, \operatorname{sgn}\!\left(a\right)\right)

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("945be9"),
    Formula(Equal(XGCD(a, a), Tuple(Abs(a), 0, Sign(a)))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

0bb73e

\operatorname{xgcd}\!\left(a, -a\right) = \left(\left|a\right|, 0, -\operatorname{sgn}\!\left(a\right)\right)

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{xgcd}\!\left(a, -a\right) = \left(\left|a\right|, 0, -\operatorname{sgn}\!\left(a\right)\right)

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("0bb73e"),
    Formula(Equal(XGCD(a, Neg(a)), Tuple(Abs(a), 0, Neg(Sign(a))))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

b66d1e

\operatorname{xgcd}\!\left(a, -1\right) = \left(1, 0, -1\right)

Assumptions:

a \in \mathbb{Z}

TeX:

\operatorname{xgcd}\!\left(a, -1\right) = \left(1, 0, -1\right)

a \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("b66d1e"),
    Formula(Equal(XGCD(a, -1), Tuple(1, 0, -1))),
    Variables(a),
    Assumptions(Element(a, ZZ)))

1b47db

\operatorname{xgcd}\!\left(-1, b\right) = \left(1, -\left|\operatorname{sgn}\!\left(\left(b - 1\right) \left(b + 1\right)\right)\right|, \operatorname{sgn}\!\left(b\right) \left(\operatorname{sgn}\!\left(b + 1\right) - \operatorname{sgn}\!\left(b - 1\right)\right)\right)

Assumptions:

b \in \mathbb{Z}

TeX:

\operatorname{xgcd}\!\left(-1, b\right) = \left(1, -\left|\operatorname{sgn}\!\left(\left(b - 1\right) \left(b + 1\right)\right)\right|, \operatorname{sgn}\!\left(b\right) \left(\operatorname{sgn}\!\left(b + 1\right) - \operatorname{sgn}\!\left(b - 1\right)\right)\right)

b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("1b47db"),
    Formula(Equal(XGCD(-1, b), Tuple(1, Neg(Abs(Sign(Mul(Sub(b, 1), Add(b, 1))))), Mul(Sign(b), Sub(Sign(Add(b, 1)), Sign(Sub(b, 1))))))),
    Variables(b),
    Assumptions(Element(b, ZZ)))

a5ef5f

\left(\left|a\right| = \left|b\right|\right) \implies \left(\left(u, v\right) = \left(0, \operatorname{sgn}\!\left(b\right)\right)\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\left(\left|a\right| = \left|b\right|\right) \implies \left(\left(u, v\right) = \left(0, \operatorname{sgn}\!\left(b\right)\right)\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("a5ef5f"),
    Formula(Where(Implies(Equal(Abs(a), Abs(b)), Equal(Tuple(u, v), Tuple(0, Sign(b)))), Equal(Tuple(d, u, v), XGCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

633265

\left(\left|a\right| \ne \left|b\right| \,\mathbin{\operatorname{and}}\, \left|a\right| \ne \left|2 d\right|\right) \implies \left(2 d \left|v\right| \lt \left|a\right|\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\left(\left|a\right| \ne \left|b\right| \,\mathbin{\operatorname{and}}\, \left|a\right| \ne \left|2 d\right|\right) \implies \left(2 d \left|v\right| \lt \left|a\right|\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("633265"),
    Formula(Where(Implies(And(Unequal(Abs(a), Abs(b)), Unequal(Abs(a), Abs(Mul(2, d)))), Less(Mul(Mul(2, d), Abs(v)), Abs(a))), Equal(Tuple(d, u, v), XGCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

4e5aad

\left(\left|a\right| \ne \left|b\right| \,\mathbin{\operatorname{and}}\, \left|a\right| = \left|2 d\right|\right) \implies \left(v = \operatorname{sgn}\!\left(b\right)\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\left(\left|a\right| \ne \left|b\right| \,\mathbin{\operatorname{and}}\, \left|a\right| = \left|2 d\right|\right) \implies \left(v = \operatorname{sgn}\!\left(b\right)\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("4e5aad"),
    Formula(Where(Implies(And(Unequal(Abs(a), Abs(b)), Equal(Abs(a), Abs(Mul(2, d)))), Equal(v, Sign(b))), Equal(Tuple(d, u, v), XGCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

da7d00

\left(\left|a\right| \ne \left|b\right| \,\mathbin{\operatorname{and}}\, \left|b\right| \ne \left|2 d\right|\right) \implies \left(2 d \left|u\right| \lt \left|b\right|\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\left(\left|a\right| \ne \left|b\right| \,\mathbin{\operatorname{and}}\, \left|b\right| \ne \left|2 d\right|\right) \implies \left(2 d \left|u\right| \lt \left|b\right|\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("da7d00"),
    Formula(Where(Implies(And(Unequal(Abs(a), Abs(b)), Unequal(Abs(b), Abs(Mul(2, d)))), Less(Mul(Mul(2, d), Abs(u)), Abs(b))), Equal(Tuple(d, u, v), XGCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

569278

\left(\left|a\right| \ne \left|b\right| \,\mathbin{\operatorname{and}}\, \left|b\right| = \left|2 d\right|\right) \implies \left(u = \operatorname{sgn}\!\left(a\right)\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\left(\left|a\right| \ne \left|b\right| \,\mathbin{\operatorname{and}}\, \left|b\right| = \left|2 d\right|\right) \implies \left(u = \operatorname{sgn}\!\left(a\right)\right)\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Sign`	$\operatorname{sgn}\!\left(z\right)$	Sign function
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("569278"),
    Formula(Where(Implies(And(Unequal(Abs(a), Abs(b)), Equal(Abs(b), Abs(Mul(2, d)))), Equal(u, Sign(a))), Equal(Tuple(d, u, v), XGCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

258fc7

\gcd\!\left(a, b\right) = \gcd\!\left(b, a\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a, b\right) = \gcd\!\left(b, a\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("258fc7"),
    Formula(Equal(GCD(a, b), GCD(b, a))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

14b96c

\operatorname{lcm}\!\left(a, b\right) = \operatorname{lcm}\!\left(b, a\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, b\right) = \operatorname{lcm}\!\left(b, a\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("14b96c"),
    Formula(Equal(LCM(a, b), LCM(b, a))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

f1817f

\gcd\!\left(a, b\right) = \gcd\!\left(-a, b\right) = \gcd\!\left(a, -b\right) = \gcd\!\left(-a, -b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a, b\right) = \gcd\!\left(-a, b\right) = \gcd\!\left(a, -b\right) = \gcd\!\left(-a, -b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("f1817f"),
    Formula(Equal(GCD(a, b), GCD(Neg(a), b), GCD(a, Neg(b)), GCD(Neg(a), Neg(b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

dc0823

\operatorname{lcm}\!\left(a, b\right) = \operatorname{lcm}\!\left(-a, b\right) = \operatorname{lcm}\!\left(a, -b\right) = \operatorname{lcm}\!\left(-a, -b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, b\right) = \operatorname{lcm}\!\left(-a, b\right) = \operatorname{lcm}\!\left(a, -b\right) = \operatorname{lcm}\!\left(-a, -b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("dc0823"),
    Formula(Equal(LCM(a, b), LCM(Neg(a), b), LCM(a, Neg(b)), LCM(Neg(a), Neg(b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

e65763

\gcd\!\left(a + b, b\right) = \gcd\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a + b, b\right) = \gcd\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("e65763"),
    Formula(Equal(GCD(Add(a, b), b), GCD(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

b36dba

\gcd\!\left(a - b, b\right) = \gcd\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a - b, b\right) = \gcd\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("b36dba"),
    Formula(Equal(GCD(Sub(a, b), b), GCD(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

07ac4a

\gcd\!\left(a + n b, b\right) = \gcd\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

TeX:

\gcd\!\left(a + n b, b\right) = \gcd\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("07ac4a"),
    Formula(Equal(GCD(Add(a, Mul(n, b)), b), GCD(a, b))),
    Variables(a, b, n),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(n, ZZ))))

959a25

\gcd\!\left(a \bmod b, b\right) = \gcd\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \ne 0

TeX:

\gcd\!\left(a \bmod b, b\right) = \gcd\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("959a25"),
    Formula(Equal(GCD(Mod(a, b), b), GCD(a, b))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Unequal(b, 0))))

d4852c

\gcd\!\left(n a, n b\right) = \left|n\right| \gcd\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

TeX:

\gcd\!\left(n a, n b\right) = \left|n\right| \gcd\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("d4852c"),
    Formula(Equal(GCD(Mul(n, a), Mul(n, b)), Mul(Abs(n), GCD(a, b)))),
    Variables(a, b, n),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(n, ZZ))))

9500d3

\operatorname{lcm}\!\left(n a, n b\right) = \left|n\right| \operatorname{lcm}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(n a, n b\right) = \left|n\right| \operatorname{lcm}\!\left(a, b\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("9500d3"),
    Formula(Equal(LCM(Mul(n, a), Mul(n, b)), Mul(Abs(n), LCM(a, b)))),
    Variables(a, b, n),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(n, ZZ))))

5781de

\operatorname{lcm}\!\left(a + b, b\right) = \frac{\left|a + b\right| \operatorname{lcm}\!\left(a, b\right)}{\left|a\right|}

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a + b, b\right) = \frac{\left|a + b\right| \operatorname{lcm}\!\left(a, b\right)}{\left|a\right|}

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("5781de"),
    Formula(Equal(LCM(Add(a, b), b), Div(Mul(Abs(Add(a, b)), LCM(a, b)), Abs(a)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, ZZ), Element(n, ZZ))))

e74d86

\operatorname{lcm}\!\left(a - b, b\right) = \frac{\left|a - b\right| \operatorname{lcm}\!\left(a, b\right)}{\left|a\right|}

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a - b, b\right) = \frac{\left|a - b\right| \operatorname{lcm}\!\left(a, b\right)}{\left|a\right|}

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("e74d86"),
    Formula(Equal(LCM(Sub(a, b), b), Div(Mul(Abs(Sub(a, b)), LCM(a, b)), Abs(a)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, ZZ), Element(n, ZZ))))

1bbdaf

\operatorname{lcm}\!\left(a + n b, b\right) = \frac{\left|a + n b\right| \operatorname{lcm}\!\left(a, b\right)}{\left|a\right|}

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a + n b, b\right) = \frac{\left|a + n b\right| \operatorname{lcm}\!\left(a, b\right)}{\left|a\right|}

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("1bbdaf"),
    Formula(Equal(LCM(Add(a, Mul(n, b)), b), Div(Mul(Abs(Add(a, Mul(n, b))), LCM(a, b)), Abs(a)))),
    Variables(a, b, n),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, ZZ), Element(n, ZZ))))

646745

\gcd\!\left(\frac{a}{d}, \frac{b}{d}\right) = \frac{\gcd\!\left(a, b\right)}{\left|d\right|}

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \mid a \,\mathbin{\operatorname{and}}\, d \mid b

TeX:

\gcd\!\left(\frac{a}{d}, \frac{b}{d}\right) = \frac{\gcd\!\left(a, b\right)}{\left|d\right|}

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \mid a \,\mathbin{\operatorname{and}}\, d \mid b

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("646745"),
    Formula(Equal(GCD(Div(a, d), Div(b, d)), Div(GCD(a, b), Abs(d)))),
    Variables(a, b, d),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(d, ZZ), Divides(d, a), Divides(d, b))))

cb9f61

\operatorname{lcm}\!\left(\frac{a}{d}, \frac{b}{d}\right) = \frac{\operatorname{lcm}\!\left(a, b\right)}{\left|d\right|}

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \mid a \,\mathbin{\operatorname{and}}\, d \mid b

TeX:

\operatorname{lcm}\!\left(\frac{a}{d}, \frac{b}{d}\right) = \frac{\operatorname{lcm}\!\left(a, b\right)}{\left|d\right|}

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, d \mid a \,\mathbin{\operatorname{and}}\, d \mid b

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("cb9f61"),
    Formula(Equal(LCM(Div(a, d), Div(b, d)), Div(LCM(a, b), Abs(d)))),
    Variables(a, b, d),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(d, ZZ), Divides(d, a), Divides(d, b))))

4366b2

\gcd\!\left(a, \gcd\!\left(b, c\right)\right) = \gcd\!\left(\gcd\!\left(a, b\right), c\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z}

TeX:

\gcd\!\left(a, \gcd\!\left(b, c\right)\right) = \gcd\!\left(\gcd\!\left(a, b\right), c\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("4366b2"),
    Formula(Equal(GCD(a, GCD(b, c)), GCD(GCD(a, b), c))),
    Variables(a, b, c),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(c, ZZ))))

1cde02

\operatorname{lcm}\!\left(a, \operatorname{lcm}\!\left(b, c\right)\right) = \operatorname{lcm}\!\left(\operatorname{lcm}\!\left(a, b\right), c\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, \operatorname{lcm}\!\left(b, c\right)\right) = \operatorname{lcm}\!\left(\operatorname{lcm}\!\left(a, b\right), c\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("1cde02"),
    Formula(Equal(LCM(a, LCM(b, c)), LCM(LCM(a, b), c))),
    Variables(a, b, c),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(c, ZZ))))

8dc1c9

\gcd\!\left(a, \operatorname{lcm}\!\left(b, c\right)\right) = \operatorname{lcm}\!\left(\gcd\!\left(a, b\right), \gcd\!\left(a, c\right)\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z}

TeX:

\gcd\!\left(a, \operatorname{lcm}\!\left(b, c\right)\right) = \operatorname{lcm}\!\left(\gcd\!\left(a, b\right), \gcd\!\left(a, c\right)\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("8dc1c9"),
    Formula(Equal(GCD(a, LCM(b, c)), LCM(GCD(a, b), GCD(a, c)))),
    Variables(a, b, c),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(c, ZZ))))

c4a892

\operatorname{lcm}\!\left(a, \gcd\!\left(b, c\right)\right) = \gcd\!\left(\operatorname{lcm}\!\left(a, b\right), \operatorname{lcm}\!\left(a, c\right)\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, \gcd\!\left(b, c\right)\right) = \gcd\!\left(\operatorname{lcm}\!\left(a, b\right), \operatorname{lcm}\!\left(a, c\right)\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("c4a892"),
    Formula(Equal(LCM(a, GCD(b, c)), GCD(LCM(a, b), LCM(a, c)))),
    Variables(a, b, c),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ), Element(c, ZZ))))

1d1653

\gcd\!\left(a, \operatorname{lcm}\!\left(a, b\right)\right) = \left|a\right|

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a, \operatorname{lcm}\!\left(a, b\right)\right) = \left|a\right|

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("1d1653"),
    Formula(Equal(GCD(a, LCM(a, b)), Abs(a))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

7009cc

\operatorname{lcm}\!\left(a, \gcd\!\left(a, b\right)\right) = \left|a\right|

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, \gcd\!\left(a, b\right)\right) = \left|a\right|

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("7009cc"),
    Formula(Equal(LCM(a, GCD(a, b)), Abs(a))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

8621f6

\gcd\!\left(r s, c\right) = \gcd\!\left(r, c\right) \gcd\!\left(s, c\right)

Assumptions:

r \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, s \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \gcd\!\left(r, s\right) = 1

TeX:

\gcd\!\left(r s, c\right) = \gcd\!\left(r, c\right) \gcd\!\left(s, c\right)

r \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, s \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \gcd\!\left(r, s\right) = 1

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("8621f6"),
    Formula(Equal(GCD(Mul(r, s), c), Mul(GCD(r, c), GCD(s, c)))),
    Variables(r, s, c),
    Assumptions(And(Element(r, ZZ), Element(s, ZZ), Element(c, ZZ), Equal(GCD(r, s), 1))))

fbe121

\operatorname{lcm}\!\left(r s, c\right) = \frac{\operatorname{lcm}\!\left(r, c\right) \operatorname{lcm}\!\left(s, c\right)}{\left|c\right|}

Assumptions:

r \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, s \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \gcd\!\left(r, s\right) = 1 \,\mathbin{\operatorname{and}}\, c \ne 0

TeX:

\operatorname{lcm}\!\left(r s, c\right) = \frac{\operatorname{lcm}\!\left(r, c\right) \operatorname{lcm}\!\left(s, c\right)}{\left|c\right|}

r \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, s \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, c \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \gcd\!\left(r, s\right) = 1 \,\mathbin{\operatorname{and}}\, c \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor

Source code for this entry:

Entry(ID("fbe121"),
    Formula(Equal(LCM(Mul(r, s), c), Div(Mul(LCM(r, c), LCM(s, c)), Abs(c)))),
    Variables(r, s, c),
    Assumptions(And(Element(r, ZZ), Element(s, ZZ), Element(c, ZZ), Equal(GCD(r, s), 1), Unequal(c, 0))))

5aad5c

\gcd\!\left({r}^{m}, {s}^{n}\right) = 1

Assumptions:

r \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, s \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \gcd\!\left(r, s\right) = 1 \,\mathbin{\operatorname{and}}\, m \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 0}

TeX:

\gcd\!\left({r}^{m}, {s}^{n}\right) = 1

r \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, s \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \gcd\!\left(r, s\right) = 1 \,\mathbin{\operatorname{and}}\, m \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Pow`	${a}^{b}$	Power
`ZZ`	$\mathbb{Z}$	Integers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("5aad5c"),
    Formula(Equal(GCD(Pow(r, m), Pow(s, n)), 1)),
    Variables(r, s, m, n),
    Assumptions(And(Element(r, ZZ), Element(s, ZZ), Equal(GCD(r, s), 1), Element(m, ZZGreaterEqual(0)), Element(n, ZZGreaterEqual(0)))))

250a45

\operatorname{lcm}\!\left(r, s\right) = \left|r s\right|

Assumptions:

r \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, s \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \gcd\!\left(r, s\right) = 1

TeX:

\operatorname{lcm}\!\left(r, s\right) = \left|r s\right|

r \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, s \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, \gcd\!\left(r, s\right) = 1

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor

Source code for this entry:

Entry(ID("250a45"),
    Formula(Equal(LCM(r, s), Abs(Mul(r, s)))),
    Variables(r, s),
    Assumptions(And(Element(r, ZZ), Element(s, ZZ), Equal(GCD(r, s), 1))))

062423

\gcd\!\left(p, q\right) = 1

Assumptions:

p \in \mathbb{P} \,\mathbin{\operatorname{and}}\, q \in \mathbb{P} \,\mathbin{\operatorname{and}}\, p \ne q

TeX:

\gcd\!\left(p, q\right) = 1

p \in \mathbb{P} \,\mathbin{\operatorname{and}}\, q \in \mathbb{P} \,\mathbin{\operatorname{and}}\, p \ne q

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`PP`	$\mathbb{P}$	Prime numbers

Source code for this entry:

Entry(ID("062423"),
    Formula(Equal(GCD(p, q), 1)),
    Variables(p, q),
    Assumptions(And(Element(p, PP), Element(q, PP), Unequal(p, q))))

499cfc

\gcd\!\left({p}^{m}, {q}^{n}\right) = 1

Assumptions:

p \in \mathbb{P} \,\mathbin{\operatorname{and}}\, q \in \mathbb{P} \,\mathbin{\operatorname{and}}\, p \ne q \,\mathbin{\operatorname{and}}\, m \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 0}

TeX:

\gcd\!\left({p}^{m}, {q}^{n}\right) = 1

p \in \mathbb{P} \,\mathbin{\operatorname{and}}\, q \in \mathbb{P} \,\mathbin{\operatorname{and}}\, p \ne q \,\mathbin{\operatorname{and}}\, m \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Pow`	${a}^{b}$	Power
`PP`	$\mathbb{P}$	Prime numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("499cfc"),
    Formula(Equal(GCD(Pow(p, m), Pow(q, n)), 1)),
    Variables(p, q, m, n),
    Assumptions(And(Element(p, PP), Element(q, PP), Unequal(p, q), Element(m, ZZGreaterEqual(0)), Element(n, ZZGreaterEqual(0)))))

25986e

\gcd\!\left(\prod_{k=1}^{m} {p_{k}}^{{e}_{k}}, \prod_{k=1}^{m} {p_{k}}^{{f}_{k}}\right) = \prod_{k=1}^{m} {p_{k}}^{\min\left({e}_{k}, {f}_{k}\right)}

Assumptions:

{e}_{k} \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, {f}_{k} \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, m \in \mathbb{Z}_{\ge 0}

TeX:

\gcd\!\left(\prod_{k=1}^{m} {p_{k}}^{{e}_{k}}, \prod_{k=1}^{m} {p_{k}}^{{f}_{k}}\right) = \prod_{k=1}^{m} {p_{k}}^{\min\left({e}_{k}, {f}_{k}\right)}

{e}_{k} \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, {f}_{k} \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, m \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Pow`	${a}^{b}$	Power
`PrimeNumber`	$p_{n}$	nth prime number
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("25986e"),
    Formula(Equal(GCD(Product(Pow(PrimeNumber(k), Subscript(e, k)), Tuple(k, 1, m)), Product(Pow(PrimeNumber(k), Subscript(f, k)), Tuple(k, 1, m))), Product(Pow(PrimeNumber(k), Min(Subscript(e, k), Subscript(f, k))), Tuple(k, 1, m)))),
    Variables(e, f, m),
    Assumptions(And(Element(Subscript(e, k), ZZGreaterEqual(0)), Element(Subscript(f, k), ZZGreaterEqual(0)), Element(m, ZZGreaterEqual(0)))))

6cefd7

\operatorname{lcm}\!\left(\prod_{k=1}^{m} {p_{k}}^{{e}_{k}}, \prod_{k=1}^{m} {p_{k}}^{{f}_{k}}\right) = \prod_{k=1}^{m} {p_{k}}^{\max\left({e}_{k}, {f}_{k}\right)}

Assumptions:

{e}_{k} \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, {f}_{k} \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, m \in \mathbb{Z}_{\ge 0}

TeX:

\operatorname{lcm}\!\left(\prod_{k=1}^{m} {p_{k}}^{{e}_{k}}, \prod_{k=1}^{m} {p_{k}}^{{f}_{k}}\right) = \prod_{k=1}^{m} {p_{k}}^{\max\left({e}_{k}, {f}_{k}\right)}

{e}_{k} \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, {f}_{k} \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, m \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Pow`	${a}^{b}$	Power
`PrimeNumber`	$p_{n}$	nth prime number
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("6cefd7"),
    Formula(Equal(LCM(Product(Pow(PrimeNumber(k), Subscript(e, k)), Tuple(k, 1, m)), Product(Pow(PrimeNumber(k), Subscript(f, k)), Tuple(k, 1, m))), Product(Pow(PrimeNumber(k), Max(Subscript(e, k), Subscript(f, k))), Tuple(k, 1, m)))),
    Variables(e, f, m),
    Assumptions(And(Element(Subscript(e, k), ZZGreaterEqual(0)), Element(Subscript(f, k), ZZGreaterEqual(0)), Element(m, ZZGreaterEqual(0)))))

fdae67

\gcd\!\left({n}^{a} - 1, {n}^{b} - 1\right) = {n}^{\gcd\left(a, b\right)} - 1

Assumptions:

a \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 1}

TeX:

\gcd\!\left({n}^{a} - 1, {n}^{b} - 1\right) = {n}^{\gcd\left(a, b\right)} - 1

a \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 1}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("fdae67"),
    Formula(Equal(GCD(Sub(Pow(n, a), 1), Sub(Pow(n, b), 1)), Sub(Pow(n, GCD(a, b)), 1))),
    Variables(a, b, n),
    Assumptions(And(Element(a, ZZGreaterEqual(0)), Element(b, ZZGreaterEqual(0)), Element(n, ZZGreaterEqual(1)))))

da45c0

\gcd\!\left(F_{m}, F_{n}\right) = F_{\gcd\left(m, n\right)}

Assumptions:

m \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

TeX:

\gcd\!\left(F_{m}, F_{n}\right) = F_{\gcd\left(m, n\right)}

m \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("da45c0"),
    Formula(Equal(GCD(Fibonacci(m), Fibonacci(n)), Fibonacci(GCD(m, n)))),
    Variables(m, n),
    Assumptions(And(Element(m, ZZ), Element(n, ZZ))))

7b27cd

\left|\left\{ k : k \in \{1, 2, \ldots n\} \,\mathbin{\operatorname{and}}\, \gcd\!\left(n, k\right) = 1 \right\}\right| = \varphi\!\left(n\right)

Assumptions:

n \in \mathbb{Z}_{\ge 1}

TeX:

\left|\left\{ k : k \in \{1, 2, \ldots n\} \,\mathbin{\operatorname{and}}\, \gcd\!\left(n, k\right) = 1 \right\}\right| = \varphi\!\left(n\right)

n \in \mathbb{Z}_{\ge 1}

Definitions:

Fungrim symbol	Notation	Short description
`Cardinality`	$\left\|S\right\|$	Set cardinality
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`ZZBetween`	$\{a, a + 1, \ldots b\}$	Integers between a and b inclusive
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("7b27cd"),
    Formula(Equal(Cardinality(SetBuilder(k, k, And(Element(k, ZZBetween(1, n)), Equal(GCD(n, k), 1)))), Totient(n))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(1))))

4099d2

\lim_{N \to \infty} \frac{1}{{N}^{n}} \left|\left\{ T : T \in {\left(\{1, 2, \ldots N\}\right)}^{n} \,\mathbin{\operatorname{and}}\, \gcd\!\left(T\right) = 1 \right\}\right| = \frac{1}{\zeta\!\left(n\right)}

Assumptions:

n \in \mathbb{Z}_{\ge 2}

TeX:

\lim_{N \to \infty} \frac{1}{{N}^{n}} \left|\left\{ T : T \in {\left(\{1, 2, \ldots N\}\right)}^{n} \,\mathbin{\operatorname{and}}\, \gcd\!\left(T\right) = 1 \right\}\right| = \frac{1}{\zeta\!\left(n\right)}

n \in \mathbb{Z}_{\ge 2}

Definitions:

Fungrim symbol	Notation	Short description
`SequenceLimit`	$\lim_{n \to a} f\!\left(n\right)$	Limiting value of sequence
`Pow`	${a}^{b}$	Power
`Cardinality`	$\left\|S\right\|$	Set cardinality
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`ZZBetween`	$\{a, a + 1, \ldots b\}$	Integers between a and b inclusive
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Infinity`	$\infty$	Positive infinity
`RiemannZeta`	$\zeta\!\left(s\right)$	Riemann zeta function
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("4099d2"),
    Formula(Equal(SequenceLimit(Mul(Div(1, Pow(N, n)), Cardinality(SetBuilder(T, T, And(Element(T, Pow(ZZBetween(1, N), n)), Equal(GCD(T), 1))))), N, Infinity), Div(1, RiemannZeta(n)))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(2))))

aaef97

\sum_{k=1}^{n} \gcd\!\left(n, k\right) = \sum_{d \in \{1, 2, \ldots n\},\,d \mid n} d \varphi\!\left(\frac{n}{d}\right)

Assumptions:

n \in \mathbb{Z}_{\ge 0}

TeX:

\sum_{k=1}^{n} \gcd\!\left(n, k\right) = \sum_{d \in \{1, 2, \ldots n\},\,d \mid n} d \varphi\!\left(\frac{n}{d}\right)

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`ZZBetween`	$\{a, a + 1, \ldots b\}$	Integers between a and b inclusive
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("aaef97"),
    Formula(Equal(Sum(GCD(n, k), Tuple(k, 1, n)), SumCondition(Mul(d, Totient(Div(n, d))), d, And(Element(d, ZZBetween(1, n)), Divides(d, n))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))))

c24323

\sum_{k=1}^{n} \operatorname{lcm}\!\left(n, k\right) = \frac{n}{2} \left(1 + \sum_{d \in \{1, 2, \ldots n\},\,d \mid n} d \varphi\!\left(d\right)\right)

Assumptions:

n \in \mathbb{Z}_{\ge 0}

TeX:

\sum_{k=1}^{n} \operatorname{lcm}\!\left(n, k\right) = \frac{n}{2} \left(1 + \sum_{d \in \{1, 2, \ldots n\},\,d \mid n} d \varphi\!\left(d\right)\right)

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`ZZBetween`	$\{a, a + 1, \ldots b\}$	Integers between a and b inclusive
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("c24323"),
    Formula(Equal(Sum(LCM(n, k), Tuple(k, 1, n)), Mul(Div(n, 2), Add(1, SumCondition(Mul(d, Totient(d)), d, And(Element(d, ZZBetween(1, n)), Divides(d, n))))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))))

125606

\operatorname{lcm}\!\left(a, b\right) \le \left|a b\right|

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\operatorname{lcm}\!\left(a, b\right) \le \left|a b\right|

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`LCM`	$\operatorname{lcm}\!\left(a, b\right)$	Least common multiple
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("125606"),
    Formula(LessEqual(LCM(a, b), Abs(Mul(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

56acd6

\gcd\!\left(a, b\right) \le \max\!\left(\left|a\right|, \left|b\right|\right)

Assumptions:

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

TeX:

\gcd\!\left(a, b\right) \le \max\!\left(\left|a\right|, \left|b\right|\right)

a \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("56acd6"),
    Formula(LessEqual(GCD(a, b), Max(Abs(a), Abs(b)))),
    Variables(a, b),
    Assumptions(And(Element(a, ZZ), Element(b, ZZ))))

f91d1c

\gcd\!\left(a, b\right) \le \min\!\left(\left|a\right|, \left|b\right|\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\gcd\!\left(a, b\right) \le \min\!\left(\left|a\right|, \left|b\right|\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`GCD`	$\gcd\!\left(n, k\right)$	Greatest common divisor
`Abs`	$\left\|z\right\|$	Absolute value
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("f91d1c"),
    Formula(LessEqual(GCD(a, b), Min(Abs(a), Abs(b)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

b43dac

\left|u\right| \le \frac{\left|b\right|}{d}\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\left|u\right| \le \frac{\left|b\right|}{d}\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("b43dac"),
    Formula(Where(LessEqual(Abs(u), Div(Abs(b), d)), Equal(Tuple(d, u, v), XGCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

10ed14

\left|v\right| \le \frac{\left|a\right|}{d}\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

Assumptions:

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

TeX:

\left|v\right| \le \frac{\left|a\right|}{d}\; \text{ where } \left(d, u, v\right) = \operatorname{xgcd}\!\left(a, b\right)

a \in \mathbb{Z} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`XGCD`	$\operatorname{xgcd}\!\left(a, b\right)$	Extended greatest common divisor
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("10ed14"),
    Formula(Where(LessEqual(Abs(v), Div(Abs(a), d)), Equal(Tuple(d, u, v), XGCD(a, b)))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(ZZ, Set(0))), Element(b, SetMinus(ZZ, Set(0))))))

Definitions

Tables

Divisibility

Bézout identity

Connection formulas

Specific values

Canonical Bézout coefficients

Functional equations

Symmetry

Addition and multiplication formulas

Distributivity

Factorization

Coprime factors

Coprime arguments

Prime factorization

Special sequences

Summation and counting

Bounds and inequalities