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

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