Conclusion
-1.
(i!1
/=
0)
OR
(j!1
/=
0)
-2.
divides(kk!1,
i!1)
-3.
divides(kk!1,
j!1)
1.
kk!1
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
Tactic
TYPEPRED
"max({k:
posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})"
Premise 1. (has proof of 3 steps)
-1.
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
>
0
-2.
divides(max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}),
i!1)
-3.
divides(max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}),
j!1)
-4.
FORALL
x
:
(divides(x,
i!1)
AND
divides(x,
j!1))
IMPLIES
(x
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}))
-5.
(i!1
/=
0)
OR
(j!1
/=
0)
-6.
divides(kk!1,
i!1)
-7.
divides(kk!1,
j!1)
1.
kk!1
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
Premise 2. (has proof of 5 steps)
-1.
(i!1
/=
0)
OR
(j!1
/=
0)
-2.
divides(kk!1,
i!1)
-3.
divides(kk!1,
j!1)
1.
nonempty?[posnat]({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
AND
(EXISTS
UB
:
FORALL
y:({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
:
y
<
=
UB)
2.
kk!1
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
