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	$⊢ φ \to A \in ℕ$
	fltltc.b	$⊢ φ \to B \in ℕ$
	fltltc.c	$⊢ φ \to C \in ℕ$
	fltltc.n	$⊢ φ \to N \in ℤ_{\geq 3}$
	fltltc.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
	fltnlta.1	$⊢ φ \to A < B$
Assertion	fltnlta	$⊢ φ \to N < A$

Proof

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

Metamath Proof Explorer

Theorem fltnlta

Proof