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	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	fltne.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	fltne.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	fltne.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
	fltne.1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
Assertion	fltne	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fltne.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		fltne.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		fltne.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4		fltne.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
5		fltne.1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6		2prm	⊢ 2 ∈ ℙ
7		rtprmirr	⊢ ( ( 2 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ( ℝ ∖ ℚ ) )
8	6 4 7	sylancr	⊢ ( 𝜑 → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ( ℝ ∖ ℚ ) )
9	8	eldifbd	⊢ ( 𝜑 → ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ )
10	3	nnzd	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
11		znq	⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( 𝐶 / 𝐴 ) ∈ ℚ )
12	10 1 11	syl2anc	⊢ ( 𝜑 → ( 𝐶 / 𝐴 ) ∈ ℚ )
13		eleq1a	⊢ ( ( 𝐶 / 𝐴 ) ∈ ℚ → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝐶 / 𝐴 ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) )
14	12 13	syl	⊢ ( 𝜑 → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝐶 / 𝐴 ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) )
15	14	necon3bd	⊢ ( 𝜑 → ( ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ≠ ( 𝐶 / 𝐴 ) ) )
16	9 15	mpd	⊢ ( 𝜑 → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ≠ ( 𝐶 / 𝐴 ) )
17		2rp	⊢ 2 ∈ ℝ+
18	17	a1i	⊢ ( 𝜑 → 2 ∈ ℝ+ )
19		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
20	4 19	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
21	20	nnrecred	⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ )
22	18 21	rpcxpcld	⊢ ( 𝜑 → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℝ+ )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℝ+ )
24	3	nnrpd	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
25	1	nnrpd	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
26	24 25	rpdivcld	⊢ ( 𝜑 → ( 𝐶 / 𝐴 ) ∈ ℝ+ )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐶 / 𝐴 ) ∈ ℝ+ )
28	20	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝑁 ∈ ℕ )
29	20	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
30	1 29	nnexpcld	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
32	31	nncnd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
33		2cnd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 2 ∈ ℂ )
34	31	nnne0d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
35	30	nncnd	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
36	35	times2d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) · 2 ) = ( ( 𝐴 ↑ 𝑁 ) + ( 𝐴 ↑ 𝑁 ) ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) · 2 ) = ( ( 𝐴 ↑ 𝑁 ) + ( 𝐴 ↑ 𝑁 ) ) )
38		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
39	38	oveq1d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
40	39	oveq2d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐴 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) )
41	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
42	37 40 41	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) · 2 ) = ( 𝐶 ↑ 𝑁 ) )
43	32 33 34 42	mvllmuld	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 2 = ( ( 𝐶 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑁 ) ) )
44		2cn	⊢ 2 ∈ ℂ
45		cxproot	⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 2 )
46	44 20 45	sylancr	⊢ ( 𝜑 → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 2 )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 2 )
48	3	nncnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
49	1	nncnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
50	1	nnne0d	⊢ ( 𝜑 → 𝐴 ≠ 0 )
51	48 49 50 29	expdivd	⊢ ( 𝜑 → ( ( 𝐶 / 𝐴 ) ↑ 𝑁 ) = ( ( 𝐶 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑁 ) ) )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 𝐶 / 𝐴 ) ↑ 𝑁 ) = ( ( 𝐶 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑁 ) ) )
53	43 47 52	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = ( ( 𝐶 / 𝐴 ) ↑ 𝑁 ) )
54	23 27 28 53	exp11nnd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝐶 / 𝐴 ) )
55	16 54	mteqand	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )