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 
|- ( ph -> A e. NN )
fltltc.b 
|- ( ph -> B e. NN )
fltltc.c 
|- ( ph -> C e. NN )
fltltc.n 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
fltltc.1 
|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
fltnlta.1 
|- ( ph -> A < B )
Assertion fltnlta 
|- ( ph -> N < A )

Proof

Step Hyp Ref Expression
1 fltltc.a 
 |-  ( ph -> A e. NN )
2 fltltc.b 
 |-  ( ph -> B e. NN )
3 fltltc.c 
 |-  ( ph -> C e. NN )
4 fltltc.n 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
5 fltltc.1 
 |-  ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
6 fltnlta.1 
 |-  ( ph -> A < B )
7 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
8 4 7 syl 
 |-  ( ph -> N e. NN )
9 8 nnred 
 |-  ( ph -> N e. RR )
10 3 nnred 
 |-  ( ph -> C e. RR )
11 2 nnred 
 |-  ( ph -> B e. RR )
12 10 11 resubcld 
 |-  ( ph -> ( C - B ) e. RR )
13 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
14 uz2m1nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
15 4 13 14 3syl 
 |-  ( ph -> ( N - 1 ) e. NN )
16 15 nnnn0d 
 |-  ( ph -> ( N - 1 ) e. NN0 )
17 10 16 reexpcld 
 |-  ( ph -> ( C ^ ( N - 1 ) ) e. RR )
18 15 nnred 
 |-  ( ph -> ( N - 1 ) e. RR )
19 11 16 reexpcld 
 |-  ( ph -> ( B ^ ( N - 1 ) ) e. RR )
20 18 19 remulcld 
 |-  ( ph -> ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) e. RR )
21 17 20 readdcld 
 |-  ( ph -> ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) e. RR )
22 12 21 remulcld 
 |-  ( ph -> ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) e. RR )
23 1 nnrpd 
 |-  ( ph -> A e. RR+ )
24 15 nnzd 
 |-  ( ph -> ( N - 1 ) e. ZZ )
25 23 24 rpexpcld 
 |-  ( ph -> ( A ^ ( N - 1 ) ) e. RR+ )
26 22 25 rerpdivcld 
 |-  ( ph -> ( ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) e. RR )
27 1 nnred 
 |-  ( ph -> A e. RR )
28 19 20 readdcld 
 |-  ( ph -> ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) e. RR )
29 12 28 remulcld 
 |-  ( ph -> ( ( C - B ) x. ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) e. RR )
30 29 25 rerpdivcld 
 |-  ( ph -> ( ( ( C - B ) x. ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) e. RR )
31 12 9 remulcld 
 |-  ( ph -> ( ( C - B ) x. N ) e. RR )
32 1cnd 
 |-  ( ph -> 1 e. CC )
33 15 nncnd 
 |-  ( ph -> ( N - 1 ) e. CC )
34 19 recnd 
 |-  ( ph -> ( B ^ ( N - 1 ) ) e. CC )
35 32 33 34 adddird 
 |-  ( ph -> ( ( 1 + ( N - 1 ) ) x. ( B ^ ( N - 1 ) ) ) = ( ( 1 x. ( B ^ ( N - 1 ) ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) )
36 8 nncnd 
 |-  ( ph -> N e. CC )
37 32 36 pncan3d 
 |-  ( ph -> ( 1 + ( N - 1 ) ) = N )
38 37 oveq1d 
 |-  ( ph -> ( ( 1 + ( N - 1 ) ) x. ( B ^ ( N - 1 ) ) ) = ( N x. ( B ^ ( N - 1 ) ) ) )
39 34 mulid2d 
 |-  ( ph -> ( 1 x. ( B ^ ( N - 1 ) ) ) = ( B ^ ( N - 1 ) ) )
40 39 oveq1d 
 |-  ( ph -> ( ( 1 x. ( B ^ ( N - 1 ) ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) = ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) )
41 35 38 40 3eqtr3rd 
 |-  ( ph -> ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) = ( N x. ( B ^ ( N - 1 ) ) ) )
42 41 oveq2d 
 |-  ( ph -> ( ( C - B ) x. ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) = ( ( C - B ) x. ( N x. ( B ^ ( N - 1 ) ) ) ) )
43 42 oveq1d 
 |-  ( ph -> ( ( ( C - B ) x. ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) = ( ( ( C - B ) x. ( N x. ( B ^ ( N - 1 ) ) ) ) / ( A ^ ( N - 1 ) ) ) )
44 43 30 eqeltrrd 
 |-  ( ph -> ( ( ( C - B ) x. ( N x. ( B ^ ( N - 1 ) ) ) ) / ( A ^ ( N - 1 ) ) ) e. RR )
45 8 nnnn0d 
 |-  ( ph -> N e. NN0 )
46 45 nn0ge0d 
 |-  ( ph -> 0 <_ N )
47 1red 
 |-  ( ph -> 1 e. RR )
48 1 2 3 4 5 fltltc 
 |-  ( ph -> B < C )
49 nnltp1le 
 |-  ( ( B e. NN /\ C e. NN ) -> ( B < C <-> ( B + 1 ) <_ C ) )
50 2 3 49 syl2anc 
 |-  ( ph -> ( B < C <-> ( B + 1 ) <_ C ) )
51 48 50 mpbid 
 |-  ( ph -> ( B + 1 ) <_ C )
52 11 leidd 
 |-  ( ph -> B <_ B )
53 10 11 47 11 51 52 lesub3d 
 |-  ( ph -> 1 <_ ( C - B ) )
54 9 12 46 53 lemulge12d 
 |-  ( ph -> N <_ ( ( C - B ) x. N ) )
55 12 recnd 
 |-  ( ph -> ( C - B ) e. CC )
56 25 rpred 
 |-  ( ph -> ( A ^ ( N - 1 ) ) e. RR )
57 56 recnd 
 |-  ( ph -> ( A ^ ( N - 1 ) ) e. CC )
58 55 36 57 mulassd 
 |-  ( ph -> ( ( ( C - B ) x. N ) x. ( A ^ ( N - 1 ) ) ) = ( ( C - B ) x. ( N x. ( A ^ ( N - 1 ) ) ) ) )
59 58 oveq1d 
 |-  ( ph -> ( ( ( ( C - B ) x. N ) x. ( A ^ ( N - 1 ) ) ) / ( A ^ ( N - 1 ) ) ) = ( ( ( C - B ) x. ( N x. ( A ^ ( N - 1 ) ) ) ) / ( A ^ ( N - 1 ) ) ) )
60 55 36 mulcld 
 |-  ( ph -> ( ( C - B ) x. N ) e. CC )
61 1 nncnd 
 |-  ( ph -> A e. CC )
62 1 nnne0d 
 |-  ( ph -> A =/= 0 )
63 61 62 24 expne0d 
 |-  ( ph -> ( A ^ ( N - 1 ) ) =/= 0 )
64 60 57 63 divcan4d 
 |-  ( ph -> ( ( ( ( C - B ) x. N ) x. ( A ^ ( N - 1 ) ) ) / ( A ^ ( N - 1 ) ) ) = ( ( C - B ) x. N ) )
65 59 64 eqtr3d 
 |-  ( ph -> ( ( ( C - B ) x. ( N x. ( A ^ ( N - 1 ) ) ) ) / ( A ^ ( N - 1 ) ) ) = ( ( C - B ) x. N ) )
66 9 56 remulcld 
 |-  ( ph -> ( N x. ( A ^ ( N - 1 ) ) ) e. RR )
67 12 66 remulcld 
 |-  ( ph -> ( ( C - B ) x. ( N x. ( A ^ ( N - 1 ) ) ) ) e. RR )
68 42 29 eqeltrrd 
 |-  ( ph -> ( ( C - B ) x. ( N x. ( B ^ ( N - 1 ) ) ) ) e. RR )
69 41 28 eqeltrrd 
 |-  ( ph -> ( N x. ( B ^ ( N - 1 ) ) ) e. RR )
70 difrp 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B < C <-> ( C - B ) e. RR+ ) )
71 11 10 70 syl2anc 
 |-  ( ph -> ( B < C <-> ( C - B ) e. RR+ ) )
72 48 71 mpbid 
 |-  ( ph -> ( C - B ) e. RR+ )
73 8 nnrpd 
 |-  ( ph -> N e. RR+ )
74 2 nnrpd 
 |-  ( ph -> B e. RR+ )
75 23 74 15 6 ltexp1dd 
 |-  ( ph -> ( A ^ ( N - 1 ) ) < ( B ^ ( N - 1 ) ) )
76 56 19 73 75 ltmul2dd 
 |-  ( ph -> ( N x. ( A ^ ( N - 1 ) ) ) < ( N x. ( B ^ ( N - 1 ) ) ) )
77 66 69 72 76 ltmul2dd 
 |-  ( ph -> ( ( C - B ) x. ( N x. ( A ^ ( N - 1 ) ) ) ) < ( ( C - B ) x. ( N x. ( B ^ ( N - 1 ) ) ) ) )
78 67 68 25 77 ltdiv1dd 
 |-  ( ph -> ( ( ( C - B ) x. ( N x. ( A ^ ( N - 1 ) ) ) ) / ( A ^ ( N - 1 ) ) ) < ( ( ( C - B ) x. ( N x. ( B ^ ( N - 1 ) ) ) ) / ( A ^ ( N - 1 ) ) ) )
79 65 78 eqbrtrrd 
 |-  ( ph -> ( ( C - B ) x. N ) < ( ( ( C - B ) x. ( N x. ( B ^ ( N - 1 ) ) ) ) / ( A ^ ( N - 1 ) ) ) )
80 9 31 44 54 79 lelttrd 
 |-  ( ph -> N < ( ( ( C - B ) x. ( N x. ( B ^ ( N - 1 ) ) ) ) / ( A ^ ( N - 1 ) ) ) )
81 80 43 breqtrrd 
 |-  ( ph -> N < ( ( ( C - B ) x. ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) )
82 3 nnrpd 
 |-  ( ph -> C e. RR+ )
83 74 82 15 48 ltexp1dd 
 |-  ( ph -> ( B ^ ( N - 1 ) ) < ( C ^ ( N - 1 ) ) )
84 19 17 20 83 ltadd1dd 
 |-  ( ph -> ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) < ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) )
85 28 21 72 84 ltmul2dd 
 |-  ( ph -> ( ( C - B ) x. ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) < ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) )
86 29 22 25 85 ltdiv1dd 
 |-  ( ph -> ( ( ( C - B ) x. ( ( B ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) < ( ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) )
87 9 30 26 81 86 lttrd 
 |-  ( ph -> N < ( ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) )
88 27 45 reexpcld 
 |-  ( ph -> ( A ^ N ) e. RR )
89 1 2 3 4 5 fltnltalem 
 |-  ( ph -> ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) < ( A ^ N ) )
90 22 88 25 89 ltdiv1dd 
 |-  ( ph -> ( ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) < ( ( A ^ N ) / ( A ^ ( N - 1 ) ) ) )
91 36 32 nncand 
 |-  ( ph -> ( N - ( N - 1 ) ) = 1 )
92 91 oveq2d 
 |-  ( ph -> ( A ^ ( N - ( N - 1 ) ) ) = ( A ^ 1 ) )
93 8 nnzd 
 |-  ( ph -> N e. ZZ )
94 61 62 24 93 expsubd 
 |-  ( ph -> ( A ^ ( N - ( N - 1 ) ) ) = ( ( A ^ N ) / ( A ^ ( N - 1 ) ) ) )
95 61 exp1d 
 |-  ( ph -> ( A ^ 1 ) = A )
96 92 94 95 3eqtr3d 
 |-  ( ph -> ( ( A ^ N ) / ( A ^ ( N - 1 ) ) ) = A )
97 90 96 breqtrd 
 |-  ( ph -> ( ( ( C - B ) x. ( ( C ^ ( N - 1 ) ) + ( ( N - 1 ) x. ( B ^ ( N - 1 ) ) ) ) ) / ( A ^ ( N - 1 ) ) ) < A )
98 9 26 27 87 97 lttrd 
 |-  ( ph -> N < A )