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 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
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 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )