Theorem fltnlta

Description: N is less than A . See https://www.youtu.be/EymVXkPWxyc for an outline. (Contributed by Steven Nguyen, 24-Aug-2023)

	Ref	Expression
Hypotheses	fltltc.a	$$⊢\phi \to A\in \mathbb{N}$$
	fltltc.b	$$⊢\phi \to B\in \mathbb{N}$$
	fltltc.c	$$⊢\phi \to C\in \mathbb{N}$$
	fltltc.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	fltltc.1	$$⊢\phi \to A^N+B^N=C^N$$
	fltnlta.1	$$⊢\phi \to A<B$$
Assertion	fltnlta	$$⊢\phi \to N<A$$

Proof

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