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 φ A
fltne.b φ B
fltne.c φ C
fltne.n φ N 2
fltne.1 φ A N + B N = C N
Assertion fltne φ A B

Proof

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