Metamath Proof Explorer

Theorem fltnlta

Description: In a Fermat counterexample, the exponent N is less than all three numbers ( A , B , and C ). Note that A < B (hypothesis) and B < C ( fltltc ). See https://youtu.be/EymVXkPWxyc for an outline. (Contributed by SN, 24-Aug-2023)

Ref Expression
Hypotheses fltltc.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltltc.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltltc.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltltc.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
fltltc.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
fltnlta.1 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion fltnlta ( 𝜑 → 𝑁 < 𝐴 )

Proof

Step Hyp Ref Expression
1 fltltc.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 fltltc.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 fltltc.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 fltltc.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
5 fltltc.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6 fltnlta.1 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
7 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
8 4 7 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 8 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10 3 nnred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
11 2 nnred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
12 10 11 resubcld ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℝ )
13 uzuzle23 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
14 uz2m1nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ )
15 4 13 14 3syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ )
16 15 nnnn0d ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
17 10 16 reexpcld ⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
18 15 nnred ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
19 11 16 reexpcld ⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
20 18 19 remulcld ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
21 17 20 readdcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ )
22 12 21 remulcld ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) ∈ ℝ )
23 1 nnrpd ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
24 15 nnzd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
25 23 24 rpexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℝ+ )
26 22 25 rerpdivcld ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
27 1 nnred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
28 19 20 readdcld ⊢ ( 𝜑 → ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ )
29 12 28 remulcld ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) ∈ ℝ )
30 29 25 rerpdivcld ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
31 12 9 remulcld ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · 𝑁 ) ∈ ℝ )
32 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
33 15 nncnd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℂ )
34 19 recnd ⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
35 32 33 34 adddird ⊢ ( 𝜑 → ( ( 1 + ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( ( 1 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) )
36 8 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
37 32 36 pncan3d ⊢ ( 𝜑 → ( 1 + ( 𝑁 − 1 ) ) = 𝑁 )
38 37 oveq1d ⊢ ( 𝜑 → ( ( 1 + ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
39 34 mullidd ⊢ ( 𝜑 → ( 1 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( 𝐵 ↑ ( 𝑁 − 1 ) ) )
40 39 oveq1d ⊢ ( 𝜑 → ( ( 1 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) = ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) )
41 35 38 40 3eqtr3rd ⊢ ( 𝜑 → ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
42 41 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) = ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) )
43 42 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
44 43 30 eqeltrrd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
45 8 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
46 45 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
47 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
48 1 2 3 4 5 fltltc ⊢ ( 𝜑 → 𝐵 < 𝐶 )
49 nnltp1le ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 < 𝐶 ↔ ( 𝐵 + 1 ) ≤ 𝐶 ) )
50 2 3 49 syl2anc ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐵 + 1 ) ≤ 𝐶 ) )
51 48 50 mpbid ⊢ ( 𝜑 → ( 𝐵 + 1 ) ≤ 𝐶 )
52 11 leidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
53 10 11 47 11 51 52 lesub3d ⊢ ( 𝜑 → 1 ≤ ( 𝐶 − 𝐵 ) )
54 9 12 46 53 lemulge12d ⊢ ( 𝜑 → 𝑁 ≤ ( ( 𝐶 − 𝐵 ) · 𝑁 ) )
55 12 recnd ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
56 25 rpred ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
57 56 recnd ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
58 55 36 57 mulassd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · 𝑁 ) · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) )
59 58 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐶 − 𝐵 ) · 𝑁 ) · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
60 55 36 mulcld ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · 𝑁 ) ∈ ℂ )
61 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
62 1 nnne0d ⊢ ( 𝜑 → 𝐴 ≠ 0 )
63 61 62 24 expne0d ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ≠ 0 )
64 60 57 63 divcan4d ⊢ ( 𝜑 → ( ( ( ( 𝐶 − 𝐵 ) · 𝑁 ) · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( 𝐶 − 𝐵 ) · 𝑁 ) )
65 59 64 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( 𝐶 − 𝐵 ) · 𝑁 ) )
66 9 56 remulcld ⊢ ( 𝜑 → ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
67 12 66 remulcld ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ )
68 42 29 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ )
69 41 28 eqeltrrd ⊢ ( 𝜑 → ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
70 difrp ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ( 𝐶 − 𝐵 ) ∈ ℝ+ ) )
71 11 10 70 syl2anc ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐶 − 𝐵 ) ∈ ℝ+ ) )
72 48 71 mpbid ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℝ+ )
73 8 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
74 2 nnrpd ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
75 23 74 15 6 ltexp1dd ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) < ( 𝐵 ↑ ( 𝑁 − 1 ) ) )
76 56 19 73 75 ltmul2dd ⊢ ( 𝜑 → ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) )
77 66 69 72 76 ltmul2dd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) < ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) )
78 67 68 25 77 ltdiv1dd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
79 65 78 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · 𝑁 ) < ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
80 9 31 44 54 79 lelttrd ⊢ ( 𝜑 → 𝑁 < ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
81 80 43 breqtrrd ⊢ ( 𝜑 → 𝑁 < ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
82 3 nnrpd ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
83 74 82 15 48 ltexp1dd ⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) < ( 𝐶 ↑ ( 𝑁 − 1 ) ) )
84 19 17 20 83 ltadd1dd ⊢ ( 𝜑 → ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) < ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) )
85 28 21 72 84 ltmul2dd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) < ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) )
86 29 22 25 85 ltdiv1dd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
87 9 30 26 81 86 lttrd ⊢ ( 𝜑 → 𝑁 < ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
88 27 45 reexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
89 1 2 3 4 5 fltnltalem ⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) < ( 𝐴 ↑ 𝑁 ) )
90 22 88 25 89 ltdiv1dd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
91 36 32 nncand ⊢ ( 𝜑 → ( 𝑁 − ( 𝑁 − 1 ) ) = 1 )
92 91 oveq2d ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − ( 𝑁 − 1 ) ) ) = ( 𝐴 ↑ 1 ) )
93 8 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
94 61 62 24 93 expsubd ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − ( 𝑁 − 1 ) ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) )
95 61 exp1d ⊢ ( 𝜑 → ( 𝐴 ↑ 1 ) = 𝐴 )
96 92 94 95 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = 𝐴 )
97 90 96 breqtrd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < 𝐴 )
98 9 26 27 87 97 lttrd ⊢ ( 𝜑 → 𝑁 < 𝐴 )