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	$$⊢\phi \to A\in \mathbb{N}$$
	fltne.b	$$⊢\phi \to B\in \mathbb{N}$$
	fltne.c	$$⊢\phi \to C\in \mathbb{N}$$
	fltne.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 2}$$
	fltne.1	$$⊢\phi \to A^N+B^N=C^N$$
Assertion	fltne	$$⊢\phi \to A\ne B$$

Proof

Step	Hyp	Ref	Expression
1		fltne.a	$$⊢\phi \to A\in \mathbb{N}$$
2		fltne.b	$$⊢\phi \to B\in \mathbb{N}$$
3		fltne.c	$$⊢\phi \to C\in \mathbb{N}$$
4		fltne.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 2}$$
5		fltne.1	$$⊢\phi \to A^N+B^N=C^N$$
6		2prm	$$⊢2\in \mathbb{P}$$
7		rtprmirr	$$⊢\left(2\in \mathbb{P}\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to 2^{\frac{1}{N}}\in \left(ℝ\setminus \mathbb{Q}\right)$$
8	6 4 7	sylancr	$$⊢\phi \to 2^{\frac{1}{N}}\in \left(ℝ\setminus \mathbb{Q}\right)$$
9	8	eldifbd	$$⊢\phi \to \neg 2^{\frac{1}{N}}\in \mathbb{Q}$$
10	3	nnzd	$$⊢\phi \to C\in \mathbb{Z}$$
11		znq	$$⊢\left(C\in \mathbb{Z}\wedge A\in \mathbb{N}\right)\to \frac{C}{A}\in \mathbb{Q}$$
12	10 1 11	syl2anc	$$⊢\phi \to \frac{C}{A}\in \mathbb{Q}$$
13		eleq1a	$$⊢\frac{C}{A}\in \mathbb{Q}\to \left(2^{\frac{1}{N}}=\frac{C}{A}\to 2^{\frac{1}{N}}\in \mathbb{Q}\right)$$
14	12 13	syl	$$⊢\phi \to \left(2^{\frac{1}{N}}=\frac{C}{A}\to 2^{\frac{1}{N}}\in \mathbb{Q}\right)$$
15	14	necon3bd	$$⊢\phi \to \left(\neg 2^{\frac{1}{N}}\in \mathbb{Q}\to 2^{\frac{1}{N}}\ne \frac{C}{A}\right)$$
16	9 15	mpd	$$⊢\phi \to 2^{\frac{1}{N}}\ne \frac{C}{A}$$
17		2rp	$$⊢2\in {ℝ}^{+}$$
18	17	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
19		eluz2nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{N}$$
20	4 19	syl	$$⊢\phi \to N\in \mathbb{N}$$
21	20	nnrecred	$$⊢\phi \to \frac{1}{N}\in ℝ$$
22	18 21	rpcxpcld	$$⊢\phi \to 2^{\frac{1}{N}}\in {ℝ}^{+}$$
23	22	adantr	$$⊢\left(\phi \wedge A=B\right)\to 2^{\frac{1}{N}}\in {ℝ}^{+}$$
24	3	nnrpd	$$⊢\phi \to C\in {ℝ}^{+}$$
25	1	nnrpd	$$⊢\phi \to A\in {ℝ}^{+}$$
26	24 25	rpdivcld	$$⊢\phi \to \frac{C}{A}\in {ℝ}^{+}$$
27	26	adantr	$$⊢\left(\phi \wedge A=B\right)\to \frac{C}{A}\in {ℝ}^{+}$$
28	20	adantr	$$⊢\left(\phi \wedge A=B\right)\to N\in \mathbb{N}$$
29	20	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
30	1 29	nnexpcld	$$⊢\phi \to A^N\in \mathbb{N}$$
31	30	adantr	$$⊢\left(\phi \wedge A=B\right)\to A^N\in \mathbb{N}$$
32	31	nncnd	$$⊢\left(\phi \wedge A=B\right)\to A^N\in ℂ$$
33		2cnd	$$⊢\left(\phi \wedge A=B\right)\to 2\in ℂ$$
34	31	nnne0d	$$⊢\left(\phi \wedge A=B\right)\to A^N\ne 0$$
35	30	nncnd	$$⊢\phi \to A^N\in ℂ$$
36	35	times2d	$$⊢\phi \to A^N\cdot 2=A^N+A^N$$
37	36	adantr	$$⊢\left(\phi \wedge A=B\right)\to A^N\cdot 2=A^N+A^N$$
38		simpr	$$⊢\left(\phi \wedge A=B\right)\to A=B$$
39	38	oveq1d	$$⊢\left(\phi \wedge A=B\right)\to A^N=B^N$$
40	39	oveq2d	$$⊢\left(\phi \wedge A=B\right)\to A^N+A^N=A^N+B^N$$
41	5	adantr	$$⊢\left(\phi \wedge A=B\right)\to A^N+B^N=C^N$$
42	37 40 41	3eqtrd	$$⊢\left(\phi \wedge A=B\right)\to A^N\cdot 2=C^N$$
43	32 33 34 42	mvllmuld	$$⊢\left(\phi \wedge A=B\right)\to 2=\frac{C^N}{A^N}$$
44		2cn	$$⊢2\in ℂ$$
45		cxproot	$$⊢\left(2\in ℂ\wedge N\in \mathbb{N}\right)\to {\left(2^{\frac{1}{N}}\right)}^N=2$$
46	44 20 45	sylancr	$$⊢\phi \to {\left(2^{\frac{1}{N}}\right)}^N=2$$
47	46	adantr	$$⊢\left(\phi \wedge A=B\right)\to {\left(2^{\frac{1}{N}}\right)}^N=2$$
48	3	nncnd	$$⊢\phi \to C\in ℂ$$
49	1	nncnd	$$⊢\phi \to A\in ℂ$$
50	1	nnne0d	$$⊢\phi \to A\ne 0$$
51	48 49 50 29	expdivd	$$⊢\phi \to {\left(\frac{C}{A}\right)}^N=\frac{C^N}{A^N}$$
52	51	adantr	$$⊢\left(\phi \wedge A=B\right)\to {\left(\frac{C}{A}\right)}^N=\frac{C^N}{A^N}$$
53	43 47 52	3eqtr4d	$$⊢\left(\phi \wedge A=B\right)\to {\left(2^{\frac{1}{N}}\right)}^N={\left(\frac{C}{A}\right)}^N$$
54	23 27 28 53	exp11nnd	$$⊢\left(\phi \wedge A=B\right)\to 2^{\frac{1}{N}}=\frac{C}{A}$$
55	16 54	mteqand	$$⊢\phi \to A\ne B$$