Theorem fltne

Description: If a counterexample to FLT exists, its addends are not equal. (Contributed by Steven Nguyen, 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 3}$$
	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 3}$$
5		fltne.1	$$⊢\phi \to A^N+B^N=C^N$$
6		2prm	$$⊢2\in \mathbb{P}$$
7	6	a1i	$$⊢\phi \to 2\in \mathbb{P}$$
8		uzuzle23	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in {\mathbb{Z}}_{\ge 2}$$
9	4 8	syl	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 2}$$
10		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)$$
11	7 9 10	syl2anc	$$⊢\phi \to 2^{\frac{1}{N}}\in \left(ℝ\setminus \mathbb{Q}\right)$$
12	11	eldifbd	$$⊢\phi \to \neg 2^{\frac{1}{N}}\in \mathbb{Q}$$
13	3	nnzd	$$⊢\phi \to C\in \mathbb{Z}$$
14		znq	$$⊢\left(C\in \mathbb{Z}\wedge A\in \mathbb{N}\right)\to \frac{C}{A}\in \mathbb{Q}$$
15	13 1 14	syl2anc	$$⊢\phi \to \frac{C}{A}\in \mathbb{Q}$$
16		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)$$
17	15 16	syl	$$⊢\phi \to \left(2^{\frac{1}{N}}=\frac{C}{A}\to 2^{\frac{1}{N}}\in \mathbb{Q}\right)$$
18	17	necon3bd	$$⊢\phi \to \left(\neg 2^{\frac{1}{N}}\in \mathbb{Q}\to 2^{\frac{1}{N}}\ne \frac{C}{A}\right)$$
19	12 18	mpd	$$⊢\phi \to 2^{\frac{1}{N}}\ne \frac{C}{A}$$
20		2rp	$$⊢2\in {ℝ}^{+}$$
21	20	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
22		eluzge3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
23	4 22	syl	$$⊢\phi \to N\in \mathbb{N}$$
24	23	nnrecred	$$⊢\phi \to \frac{1}{N}\in ℝ$$
25	21 24	rpcxpcld	$$⊢\phi \to 2^{\frac{1}{N}}\in {ℝ}^{+}$$
26	25	adantr	$$⊢\left(\phi \wedge A=B\right)\to 2^{\frac{1}{N}}\in {ℝ}^{+}$$
27	3	nnrpd	$$⊢\phi \to C\in {ℝ}^{+}$$
28	1	nnrpd	$$⊢\phi \to A\in {ℝ}^{+}$$
29	27 28	rpdivcld	$$⊢\phi \to \frac{C}{A}\in {ℝ}^{+}$$
30	29	adantr	$$⊢\left(\phi \wedge A=B\right)\to \frac{C}{A}\in {ℝ}^{+}$$
31		simpl	$$⊢\left(\phi \wedge A=B\right)\to \phi$$
32		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
33	31 4 32	3syl	$$⊢\left(\phi \wedge A=B\right)\to N\in \mathbb{Z}$$
34	23	nnne0d	$$⊢\phi \to N\ne 0$$
35	34	adantr	$$⊢\left(\phi \wedge A=B\right)\to N\ne 0$$
36	1	nncnd	$$⊢\phi \to A\in ℂ$$
37	23	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
38	36 37	expcld	$$⊢\phi \to A^N\in ℂ$$
39	38	adantr	$$⊢\left(\phi \wedge A=B\right)\to A^N\in ℂ$$
40		2cnd	$$⊢\left(\phi \wedge A=B\right)\to 2\in ℂ$$
41	1	nnne0d	$$⊢\phi \to A\ne 0$$
42	4 32	syl	$$⊢\phi \to N\in \mathbb{Z}$$
43	36 41 42	expne0d	$$⊢\phi \to A^N\ne 0$$
44	43	adantr	$$⊢\left(\phi \wedge A=B\right)\to A^N\ne 0$$
45	39	times2d	$$⊢\left(\phi \wedge A=B\right)\to A^N\cdot 2=A^N+A^N$$
46		simpr	$$⊢\left(\phi \wedge A=B\right)\to A=B$$
47	46	oveq1d	$$⊢\left(\phi \wedge A=B\right)\to A^N=B^N$$
48	47	oveq2d	$$⊢\left(\phi \wedge A=B\right)\to A^N+A^N=A^N+B^N$$
49	5	adantr	$$⊢\left(\phi \wedge A=B\right)\to A^N+B^N=C^N$$
50	45 48 49	3eqtrd	$$⊢\left(\phi \wedge A=B\right)\to A^N\cdot 2=C^N$$
51	39 40 44 50	mvllmuld	$$⊢\left(\phi \wedge A=B\right)\to 2=\frac{C^N}{A^N}$$
52	23	adantr	$$⊢\left(\phi \wedge A=B\right)\to N\in \mathbb{N}$$
53		cxproot	$$⊢\left(2\in ℂ\wedge N\in \mathbb{N}\right)\to {\left(2^{\frac{1}{N}}\right)}^N=2$$
54	40 52 53	syl2anc	$$⊢\left(\phi \wedge A=B\right)\to {\left(2^{\frac{1}{N}}\right)}^N=2$$
55	3	nncnd	$$⊢\phi \to C\in ℂ$$
56	55 36 41 37	expdivd	$$⊢\phi \to {\left(\frac{C}{A}\right)}^N=\frac{C^N}{A^N}$$
57	56	adantr	$$⊢\left(\phi \wedge A=B\right)\to {\left(\frac{C}{A}\right)}^N=\frac{C^N}{A^N}$$
58	51 54 57	3eqtr4d	$$⊢\left(\phi \wedge A=B\right)\to {\left(2^{\frac{1}{N}}\right)}^N={\left(\frac{C}{A}\right)}^N$$
59	26 30 33 35 58	exp11d	$$⊢\left(\phi \wedge A=B\right)\to 2^{\frac{1}{N}}=\frac{C}{A}$$
60	19 59	mteqand	$$⊢\phi \to A\ne B$$