Metamath Proof Explorer

Theorem flt4lem6

Description: Remove shared factors in a solution to A ^ 4 + B ^ 4 = C ^ 2 . (Contributed by SN, 24-Jul-2024)

Ref Expression
Hypotheses flt4lem6.a 
|- ( ph -> A e. NN )
flt4lem6.b 
|- ( ph -> B e. NN )
flt4lem6.c 
|- ( ph -> C e. NN )
flt4lem6.1 
|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
Assertion flt4lem6 
|- ( ph -> ( ( ( A / ( A gcd B ) ) e. NN /\ ( B / ( A gcd B ) ) e. NN /\ ( C / ( ( A gcd B ) ^ 2 ) ) e. NN ) /\ ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( ( C / ( ( A gcd B ) ^ 2 ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 flt4lem6.a 
 |-  ( ph -> A e. NN )
2 flt4lem6.b 
 |-  ( ph -> B e. NN )
3 flt4lem6.c 
 |-  ( ph -> C e. NN )
4 flt4lem6.1 
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
5 2 nnzd 
 |-  ( ph -> B e. ZZ )
6 divgcdnn 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A / ( A gcd B ) ) e. NN )
7 1 5 6 syl2anc 
 |-  ( ph -> ( A / ( A gcd B ) ) e. NN )
8 1 nnzd 
 |-  ( ph -> A e. ZZ )
9 divgcdnnr 
 |-  ( ( B e. NN /\ A e. ZZ ) -> ( B / ( A gcd B ) ) e. NN )
10 2 8 9 syl2anc 
 |-  ( ph -> ( B / ( A gcd B ) ) e. NN )
11 gcdnncl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
12 1 2 11 syl2anc 
 |-  ( ph -> ( A gcd B ) e. NN )
13 12 nncnd 
 |-  ( ph -> ( A gcd B ) e. CC )
14 13 flt4lem 
 |-  ( ph -> ( ( A gcd B ) ^ 4 ) = ( ( ( A gcd B ) ^ 2 ) ^ 2 ) )
15 4 14 oveq12d 
 |-  ( ph -> ( ( ( A ^ 4 ) + ( B ^ 4 ) ) / ( ( A gcd B ) ^ 4 ) ) = ( ( C ^ 2 ) / ( ( ( A gcd B ) ^ 2 ) ^ 2 ) ) )
16 1 nncnd 
 |-  ( ph -> A e. CC )
17 12 nnne0d 
 |-  ( ph -> ( A gcd B ) =/= 0 )
18 4nn0 
 |-  4 e. NN0
19 18 a1i 
 |-  ( ph -> 4 e. NN0 )
20 16 13 17 19 expdivd 
 |-  ( ph -> ( ( A / ( A gcd B ) ) ^ 4 ) = ( ( A ^ 4 ) / ( ( A gcd B ) ^ 4 ) ) )
21 2 nncnd 
 |-  ( ph -> B e. CC )
22 21 13 17 19 expdivd 
 |-  ( ph -> ( ( B / ( A gcd B ) ) ^ 4 ) = ( ( B ^ 4 ) / ( ( A gcd B ) ^ 4 ) ) )
23 20 22 oveq12d 
 |-  ( ph -> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( ( ( A ^ 4 ) / ( ( A gcd B ) ^ 4 ) ) + ( ( B ^ 4 ) / ( ( A gcd B ) ^ 4 ) ) ) )
24 16 19 expcld 
 |-  ( ph -> ( A ^ 4 ) e. CC )
25 21 19 expcld 
 |-  ( ph -> ( B ^ 4 ) e. CC )
26 13 19 expcld 
 |-  ( ph -> ( ( A gcd B ) ^ 4 ) e. CC )
27 12 19 nnexpcld 
 |-  ( ph -> ( ( A gcd B ) ^ 4 ) e. NN )
28 27 nnne0d 
 |-  ( ph -> ( ( A gcd B ) ^ 4 ) =/= 0 )
29 24 25 26 28 divdird 
 |-  ( ph -> ( ( ( A ^ 4 ) + ( B ^ 4 ) ) / ( ( A gcd B ) ^ 4 ) ) = ( ( ( A ^ 4 ) / ( ( A gcd B ) ^ 4 ) ) + ( ( B ^ 4 ) / ( ( A gcd B ) ^ 4 ) ) ) )
30 23 29 eqtr4d 
 |-  ( ph -> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( ( ( A ^ 4 ) + ( B ^ 4 ) ) / ( ( A gcd B ) ^ 4 ) ) )
31 3 nncnd 
 |-  ( ph -> C e. CC )
32 12 nnsqcld 
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) e. NN )
33 32 nncnd 
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) e. CC )
34 32 nnne0d 
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) =/= 0 )
35 31 33 34 sqdivd 
 |-  ( ph -> ( ( C / ( ( A gcd B ) ^ 2 ) ) ^ 2 ) = ( ( C ^ 2 ) / ( ( ( A gcd B ) ^ 2 ) ^ 2 ) ) )
36 15 30 35 3eqtr4d 
 |-  ( ph -> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( ( C / ( ( A gcd B ) ^ 2 ) ) ^ 2 ) )
37 7 19 nnexpcld 
 |-  ( ph -> ( ( A / ( A gcd B ) ) ^ 4 ) e. NN )
38 10 19 nnexpcld 
 |-  ( ph -> ( ( B / ( A gcd B ) ) ^ 4 ) e. NN )
39 37 38 nnaddcld 
 |-  ( ph -> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) e. NN )
40 39 nnzd 
 |-  ( ph -> ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) e. ZZ )
41 36 40 eqeltrrd 
 |-  ( ph -> ( ( C / ( ( A gcd B ) ^ 2 ) ) ^ 2 ) e. ZZ )
42 3 nnzd 
 |-  ( ph -> C e. ZZ )
43 znq 
 |-  ( ( C e. ZZ /\ ( ( A gcd B ) ^ 2 ) e. NN ) -> ( C / ( ( A gcd B ) ^ 2 ) ) e. QQ )
44 42 32 43 syl2anc 
 |-  ( ph -> ( C / ( ( A gcd B ) ^ 2 ) ) e. QQ )
45 3 nnred 
 |-  ( ph -> C e. RR )
46 32 nnred 
 |-  ( ph -> ( ( A gcd B ) ^ 2 ) e. RR )
47 3 nngt0d 
 |-  ( ph -> 0 < C )
48 32 nngt0d 
 |-  ( ph -> 0 < ( ( A gcd B ) ^ 2 ) )
49 45 46 47 48 divgt0d 
 |-  ( ph -> 0 < ( C / ( ( A gcd B ) ^ 2 ) ) )
50 41 44 49 posqsqznn 
 |-  ( ph -> ( C / ( ( A gcd B ) ^ 2 ) ) e. NN )
51 7 10 50 3jca 
 |-  ( ph -> ( ( A / ( A gcd B ) ) e. NN /\ ( B / ( A gcd B ) ) e. NN /\ ( C / ( ( A gcd B ) ^ 2 ) ) e. NN ) )
52 51 36 jca 
 |-  ( ph -> ( ( ( A / ( A gcd B ) ) e. NN /\ ( B / ( A gcd B ) ) e. NN /\ ( C / ( ( A gcd B ) ^ 2 ) ) e. NN ) /\ ( ( ( A / ( A gcd B ) ) ^ 4 ) + ( ( B / ( A gcd B ) ) ^ 4 ) ) = ( ( C / ( ( A gcd B ) ^ 2 ) ) ^ 2 ) ) )