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	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	⊢ ( 𝜑 → 𝑁 < 𝐴 )