This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fltdvdsabdvdsc

Description: Any factor of both A and B also divides C . This establishes the validity of fltabcoprmex . (Contributed by SN, 21-Aug-2024)

Ref Expression
Hypotheses fltdvdsabdvdsc.a 
|- ( ph -> A e. NN )
fltdvdsabdvdsc.b 
|- ( ph -> B e. NN )
fltdvdsabdvdsc.c 
|- ( ph -> C e. NN )
fltdvdsabdvdsc.n 
|- ( ph -> N e. NN )
fltdvdsabdvdsc.1 
|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
Assertion fltdvdsabdvdsc 
|- ( ph -> ( A gcd B ) || C )

Proof

Step Hyp Ref Expression
1 fltdvdsabdvdsc.a 
 |-  ( ph -> A e. NN )
2 fltdvdsabdvdsc.b 
 |-  ( ph -> B e. NN )
3 fltdvdsabdvdsc.c 
 |-  ( ph -> C e. NN )
4 fltdvdsabdvdsc.n 
 |-  ( ph -> N e. NN )
5 fltdvdsabdvdsc.1 
 |-  ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
6 gcdnncl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
7 1 2 6 syl2anc 
 |-  ( ph -> ( A gcd B ) e. NN )
8 4 nnnn0d 
 |-  ( ph -> N e. NN0 )
9 7 8 nnexpcld 
 |-  ( ph -> ( ( A gcd B ) ^ N ) e. NN )
10 9 nnzd 
 |-  ( ph -> ( ( A gcd B ) ^ N ) e. ZZ )
11 1 8 nnexpcld 
 |-  ( ph -> ( A ^ N ) e. NN )
12 11 nnzd 
 |-  ( ph -> ( A ^ N ) e. ZZ )
13 2 8 nnexpcld 
 |-  ( ph -> ( B ^ N ) e. NN )
14 13 nnzd 
 |-  ( ph -> ( B ^ N ) e. ZZ )
15 7 nnzd 
 |-  ( ph -> ( A gcd B ) e. ZZ )
16 1 nnzd 
 |-  ( ph -> A e. ZZ )
17 2 nnzd 
 |-  ( ph -> B e. ZZ )
18 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
19 16 17 18 syl2anc 
 |-  ( ph -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
20 19 simpld 
 |-  ( ph -> ( A gcd B ) || A )
21 15 16 8 20 dvdsexpad 
 |-  ( ph -> ( ( A gcd B ) ^ N ) || ( A ^ N ) )
22 19 simprd 
 |-  ( ph -> ( A gcd B ) || B )
23 15 17 8 22 dvdsexpad 
 |-  ( ph -> ( ( A gcd B ) ^ N ) || ( B ^ N ) )
24 10 12 14 21 23 dvds2addd 
 |-  ( ph -> ( ( A gcd B ) ^ N ) || ( ( A ^ N ) + ( B ^ N ) ) )
25 24 5 breqtrd 
 |-  ( ph -> ( ( A gcd B ) ^ N ) || ( C ^ N ) )
26 dvdsexpnn 
 |-  ( ( ( A gcd B ) e. NN /\ C e. NN /\ N e. NN ) -> ( ( A gcd B ) || C <-> ( ( A gcd B ) ^ N ) || ( C ^ N ) ) )
27 7 3 4 26 syl3anc 
 |-  ( ph -> ( ( A gcd B ) || C <-> ( ( A gcd B ) ^ N ) || ( C ^ N ) ) )
28 25 27 mpbird 
 |-  ( ph -> ( A gcd B ) || C )