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

Metamath Proof Explorer

Theorem fltaccoprm

Description: A counterexample to FLT with A , B coprime also has A , C coprime. (Contributed by SN, 20-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 fltabcoprmex.a 
 |-  ( ph -> A e. NN )
2 fltabcoprmex.b 
 |-  ( ph -> B e. NN )
3 fltabcoprmex.c 
 |-  ( ph -> C e. NN )
4 fltabcoprmex.n 
 |-  ( ph -> N e. NN0 )
5 fltabcoprmex.1 
 |-  ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
6 fltaccoprm.1 
 |-  ( ph -> ( A gcd B ) = 1 )
7 coprmgcdb 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )
8 1 2 7 syl2anc 
 |-  ( ph -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )
9 6 8 mpbird 
 |-  ( ph -> A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) )
10 simprl 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> i || A )
11 simpr 
 |-  ( ( ph /\ i e. NN ) -> i e. NN )
12 11 nnzd 
 |-  ( ( ph /\ i e. NN ) -> i e. ZZ )
13 3 nnzd 
 |-  ( ph -> C e. ZZ )
14 13 adantr 
 |-  ( ( ph /\ i e. NN ) -> C e. ZZ )
15 4 adantr 
 |-  ( ( ph /\ i e. NN ) -> N e. NN0 )
16 dvdsexpim 
 |-  ( ( i e. ZZ /\ C e. ZZ /\ N e. NN0 ) -> ( i || C -> ( i ^ N ) || ( C ^ N ) ) )
17 12 14 15 16 syl3anc 
 |-  ( ( ph /\ i e. NN ) -> ( i || C -> ( i ^ N ) || ( C ^ N ) ) )
18 1 nnzd 
 |-  ( ph -> A e. ZZ )
19 18 adantr 
 |-  ( ( ph /\ i e. NN ) -> A e. ZZ )
20 dvdsexpim 
 |-  ( ( i e. ZZ /\ A e. ZZ /\ N e. NN0 ) -> ( i || A -> ( i ^ N ) || ( A ^ N ) ) )
21 12 19 15 20 syl3anc 
 |-  ( ( ph /\ i e. NN ) -> ( i || A -> ( i ^ N ) || ( A ^ N ) ) )
22 17 21 anim12d 
 |-  ( ( ph /\ i e. NN ) -> ( ( i || C /\ i || A ) -> ( ( i ^ N ) || ( C ^ N ) /\ ( i ^ N ) || ( A ^ N ) ) ) )
23 22 ancomsd 
 |-  ( ( ph /\ i e. NN ) -> ( ( i || A /\ i || C ) -> ( ( i ^ N ) || ( C ^ N ) /\ ( i ^ N ) || ( A ^ N ) ) ) )
24 23 imp 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( ( i ^ N ) || ( C ^ N ) /\ ( i ^ N ) || ( A ^ N ) ) )
25 11 15 nnexpcld 
 |-  ( ( ph /\ i e. NN ) -> ( i ^ N ) e. NN )
26 25 nnzd 
 |-  ( ( ph /\ i e. NN ) -> ( i ^ N ) e. ZZ )
27 26 adantr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( i ^ N ) e. ZZ )
28 3 4 nnexpcld 
 |-  ( ph -> ( C ^ N ) e. NN )
29 28 nnzd 
 |-  ( ph -> ( C ^ N ) e. ZZ )
30 29 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( C ^ N ) e. ZZ )
31 1 4 nnexpcld 
 |-  ( ph -> ( A ^ N ) e. NN )
32 31 nnzd 
 |-  ( ph -> ( A ^ N ) e. ZZ )
33 32 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( A ^ N ) e. ZZ )
34 dvds2sub 
 |-  ( ( ( i ^ N ) e. ZZ /\ ( C ^ N ) e. ZZ /\ ( A ^ N ) e. ZZ ) -> ( ( ( i ^ N ) || ( C ^ N ) /\ ( i ^ N ) || ( A ^ N ) ) -> ( i ^ N ) || ( ( C ^ N ) - ( A ^ N ) ) ) )
35 27 30 33 34 syl3anc 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( ( ( i ^ N ) || ( C ^ N ) /\ ( i ^ N ) || ( A ^ N ) ) -> ( i ^ N ) || ( ( C ^ N ) - ( A ^ N ) ) ) )
36 24 35 mpd 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( i ^ N ) || ( ( C ^ N ) - ( A ^ N ) ) )
37 1 nncnd 
 |-  ( ph -> A e. CC )
38 37 4 expcld 
 |-  ( ph -> ( A ^ N ) e. CC )
39 2 nncnd 
 |-  ( ph -> B e. CC )
40 39 4 expcld 
 |-  ( ph -> ( B ^ N ) e. CC )
41 38 40 5 laddrotrd 
 |-  ( ph -> ( ( C ^ N ) - ( A ^ N ) ) = ( B ^ N ) )
42 41 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( ( C ^ N ) - ( A ^ N ) ) = ( B ^ N ) )
43 36 42 breqtrd 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( i ^ N ) || ( B ^ N ) )
44 simplr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> i e. NN )
45 2 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> B e. NN )
46 3 nncnd 
 |-  ( ph -> C e. CC )
47 37 39 46 4 5 flt0 
 |-  ( ph -> N e. NN )
48 47 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> N e. NN )
49 dvdsexpnn 
 |-  ( ( i e. NN /\ B e. NN /\ N e. NN ) -> ( i || B <-> ( i ^ N ) || ( B ^ N ) ) )
50 44 45 48 49 syl3anc 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( i || B <-> ( i ^ N ) || ( B ^ N ) ) )
51 43 50 mpbird 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> i || B )
52 10 51 jca 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || C ) ) -> ( i || A /\ i || B ) )
53 52 ex 
 |-  ( ( ph /\ i e. NN ) -> ( ( i || A /\ i || C ) -> ( i || A /\ i || B ) ) )
54 53 imim1d 
 |-  ( ( ph /\ i e. NN ) -> ( ( ( i || A /\ i || B ) -> i = 1 ) -> ( ( i || A /\ i || C ) -> i = 1 ) ) )
55 54 ralimdva 
 |-  ( ph -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) -> A. i e. NN ( ( i || A /\ i || C ) -> i = 1 ) ) )
56 9 55 mpd 
 |-  ( ph -> A. i e. NN ( ( i || A /\ i || C ) -> i = 1 ) )
57 coprmgcdb 
 |-  ( ( A e. NN /\ C e. NN ) -> ( A. i e. NN ( ( i || A /\ i || C ) -> i = 1 ) <-> ( A gcd C ) = 1 ) )
58 1 3 57 syl2anc 
 |-  ( ph -> ( A. i e. NN ( ( i || A /\ i || C ) -> i = 1 ) <-> ( A gcd C ) = 1 ) )
59 56 58 mpbid 
 |-  ( ph -> ( A gcd C ) = 1 )