Metamath Proof Explorer


Theorem fltne

Description: If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023)

Ref Expression
Hypotheses fltne.a
|- ( ph -> A e. NN )
fltne.b
|- ( ph -> B e. NN )
fltne.c
|- ( ph -> C e. NN )
fltne.n
|- ( ph -> N e. ( ZZ>= ` 2 ) )
fltne.1
|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
Assertion fltne
|- ( ph -> A =/= B )

Proof

Step Hyp Ref Expression
1 fltne.a
 |-  ( ph -> A e. NN )
2 fltne.b
 |-  ( ph -> B e. NN )
3 fltne.c
 |-  ( ph -> C e. NN )
4 fltne.n
 |-  ( ph -> N e. ( ZZ>= ` 2 ) )
5 fltne.1
 |-  ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
6 2prm
 |-  2 e. Prime
7 rtprmirr
 |-  ( ( 2 e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^c ( 1 / N ) ) e. ( RR \ QQ ) )
8 6 4 7 sylancr
 |-  ( ph -> ( 2 ^c ( 1 / N ) ) e. ( RR \ QQ ) )
9 8 eldifbd
 |-  ( ph -> -. ( 2 ^c ( 1 / N ) ) e. QQ )
10 3 nnzd
 |-  ( ph -> C e. ZZ )
11 znq
 |-  ( ( C e. ZZ /\ A e. NN ) -> ( C / A ) e. QQ )
12 10 1 11 syl2anc
 |-  ( ph -> ( C / A ) e. QQ )
13 eleq1a
 |-  ( ( C / A ) e. QQ -> ( ( 2 ^c ( 1 / N ) ) = ( C / A ) -> ( 2 ^c ( 1 / N ) ) e. QQ ) )
14 12 13 syl
 |-  ( ph -> ( ( 2 ^c ( 1 / N ) ) = ( C / A ) -> ( 2 ^c ( 1 / N ) ) e. QQ ) )
15 14 necon3bd
 |-  ( ph -> ( -. ( 2 ^c ( 1 / N ) ) e. QQ -> ( 2 ^c ( 1 / N ) ) =/= ( C / A ) ) )
16 9 15 mpd
 |-  ( ph -> ( 2 ^c ( 1 / N ) ) =/= ( C / A ) )
17 2rp
 |-  2 e. RR+
18 17 a1i
 |-  ( ph -> 2 e. RR+ )
19 eluz2nn
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
20 4 19 syl
 |-  ( ph -> N e. NN )
21 20 nnrecred
 |-  ( ph -> ( 1 / N ) e. RR )
22 18 21 rpcxpcld
 |-  ( ph -> ( 2 ^c ( 1 / N ) ) e. RR+ )
23 22 adantr
 |-  ( ( ph /\ A = B ) -> ( 2 ^c ( 1 / N ) ) e. RR+ )
24 3 nnrpd
 |-  ( ph -> C e. RR+ )
25 1 nnrpd
 |-  ( ph -> A e. RR+ )
26 24 25 rpdivcld
 |-  ( ph -> ( C / A ) e. RR+ )
27 26 adantr
 |-  ( ( ph /\ A = B ) -> ( C / A ) e. RR+ )
28 20 adantr
 |-  ( ( ph /\ A = B ) -> N e. NN )
29 20 nnnn0d
 |-  ( ph -> N e. NN0 )
30 1 29 nnexpcld
 |-  ( ph -> ( A ^ N ) e. NN )
31 30 adantr
 |-  ( ( ph /\ A = B ) -> ( A ^ N ) e. NN )
32 31 nncnd
 |-  ( ( ph /\ A = B ) -> ( A ^ N ) e. CC )
33 2cnd
 |-  ( ( ph /\ A = B ) -> 2 e. CC )
34 31 nnne0d
 |-  ( ( ph /\ A = B ) -> ( A ^ N ) =/= 0 )
35 30 nncnd
 |-  ( ph -> ( A ^ N ) e. CC )
36 35 times2d
 |-  ( ph -> ( ( A ^ N ) x. 2 ) = ( ( A ^ N ) + ( A ^ N ) ) )
37 36 adantr
 |-  ( ( ph /\ A = B ) -> ( ( A ^ N ) x. 2 ) = ( ( A ^ N ) + ( A ^ N ) ) )
38 simpr
 |-  ( ( ph /\ A = B ) -> A = B )
39 38 oveq1d
 |-  ( ( ph /\ A = B ) -> ( A ^ N ) = ( B ^ N ) )
40 39 oveq2d
 |-  ( ( ph /\ A = B ) -> ( ( A ^ N ) + ( A ^ N ) ) = ( ( A ^ N ) + ( B ^ N ) ) )
41 5 adantr
 |-  ( ( ph /\ A = B ) -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
42 37 40 41 3eqtrd
 |-  ( ( ph /\ A = B ) -> ( ( A ^ N ) x. 2 ) = ( C ^ N ) )
43 32 33 34 42 mvllmuld
 |-  ( ( ph /\ A = B ) -> 2 = ( ( C ^ N ) / ( A ^ N ) ) )
44 2cn
 |-  2 e. CC
45 cxproot
 |-  ( ( 2 e. CC /\ N e. NN ) -> ( ( 2 ^c ( 1 / N ) ) ^ N ) = 2 )
46 44 20 45 sylancr
 |-  ( ph -> ( ( 2 ^c ( 1 / N ) ) ^ N ) = 2 )
47 46 adantr
 |-  ( ( ph /\ A = B ) -> ( ( 2 ^c ( 1 / N ) ) ^ N ) = 2 )
48 3 nncnd
 |-  ( ph -> C e. CC )
49 1 nncnd
 |-  ( ph -> A e. CC )
50 1 nnne0d
 |-  ( ph -> A =/= 0 )
51 48 49 50 29 expdivd
 |-  ( ph -> ( ( C / A ) ^ N ) = ( ( C ^ N ) / ( A ^ N ) ) )
52 51 adantr
 |-  ( ( ph /\ A = B ) -> ( ( C / A ) ^ N ) = ( ( C ^ N ) / ( A ^ N ) ) )
53 43 47 52 3eqtr4d
 |-  ( ( ph /\ A = B ) -> ( ( 2 ^c ( 1 / N ) ) ^ N ) = ( ( C / A ) ^ N ) )
54 23 27 28 53 exp11nnd
 |-  ( ( ph /\ A = B ) -> ( 2 ^c ( 1 / N ) ) = ( C / A ) )
55 16 54 mteqand
 |-  ( ph -> A =/= B )