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

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 )