let n, m, n1, m1 be Nat; :: thesis: ( n1 in NatDivisors n & m1 in NatDivisors m & n,m are_coprime implies n1,m1 are_coprime )
A1: n1 gcd m1 divides m1 by INT_2:def 2;
assume n1 in NatDivisors n ; :: thesis: ( not m1 in NatDivisors m or not n,m are_coprime or n1,m1 are_coprime )
then A2: n1 divides n by MOEBIUS1:39;
n1 gcd m1 divides n1 by INT_2:def 2;
then A3: n1 gcd m1 divides n by A2, INT_2:9;
assume A4: m1 in NatDivisors m ; :: thesis: ( not n,m are_coprime or n1,m1 are_coprime )
then m1 divides m by MOEBIUS1:39;
then A5: n1 gcd m1 divides m by A1, INT_2:9;
0 < m1 by A4, MOEBIUS1:39;
then n1 gcd m1 <> 0 by INT_2:5;
then (n1 gcd m1) + 1 > 0 + 1 by XREAL_1:8;
then A6: n1 gcd m1 >= 1 by NAT_1:13;
assume A7: n,m are_coprime ; :: thesis: n1,m1 are_coprime
assume not n1,m1 are_coprime ; :: thesis: contradiction
then A8: n1 gcd m1 <> 1 by INT_2:def 3;
n gcd m > 0 by A7, INT_2:def 3;
then n1 gcd m1 <= n gcd m by A3, A5, INT_2:22, INT_2:27;
then n gcd m <> 1 by A8, A6, XXREAL_0:1;
hence contradiction by A7, INT_2:def 3; :: thesis: verum