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 eluzge3nn ( 𝑁 ∈ ( ℤ ‘ 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 mulid2d ( 𝜑 → ( 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 ( 𝜑𝑁 < 𝐴 )