Theorem flt0

Description: A counterexample for FLT does not exist for N = 0 . (Contributed by SN, 20-Aug-2024)

	Ref	Expression
Hypotheses	flt0.a	|- ( ph -> A e. CC )
	flt0.b	|- ( ph -> B e. CC )
	flt0.c	|- ( ph -> C e. CC )
	flt0.n	|- ( ph -> N e. NN0 )
	flt0.1	|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
Assertion	flt0	|- ( ph -> N e. NN )

Proof

Step	Hyp	Ref	Expression
1		flt0.a	|- ( ph -> A e. CC )
2		flt0.b	|- ( ph -> B e. CC )
3		flt0.c	|- ( ph -> C e. CC )
4		flt0.n	|- ( ph -> N e. NN0 )
5		flt0.1	|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
6		1p1e2	|- ( 1 + 1 ) = 2
7		sn-1ne2	|- 1 =/= 2
8	7	necomi	|- 2 =/= 1
9	6 8	eqnetri	|- ( 1 + 1 ) =/= 1
10	9	a1i	|- ( ph -> ( 1 + 1 ) =/= 1 )
11	1	exp0d	|- ( ph -> ( A ^ 0 ) = 1 )
12	2	exp0d	|- ( ph -> ( B ^ 0 ) = 1 )
13	11 12	oveq12d	|- ( ph -> ( ( A ^ 0 ) + ( B ^ 0 ) ) = ( 1 + 1 ) )
14	3	exp0d	|- ( ph -> ( C ^ 0 ) = 1 )
15	10 13 14	3netr4d	|- ( ph -> ( ( A ^ 0 ) + ( B ^ 0 ) ) =/= ( C ^ 0 ) )
16		oveq2	|- ( N = 0 -> ( A ^ N ) = ( A ^ 0 ) )
17		oveq2	|- ( N = 0 -> ( B ^ N ) = ( B ^ 0 ) )
18	16 17	oveq12d	|- ( N = 0 -> ( ( A ^ N ) + ( B ^ N ) ) = ( ( A ^ 0 ) + ( B ^ 0 ) ) )
19		oveq2	|- ( N = 0 -> ( C ^ N ) = ( C ^ 0 ) )
20	18 19	eqeq12d	|- ( N = 0 -> ( ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) <-> ( ( A ^ 0 ) + ( B ^ 0 ) ) = ( C ^ 0 ) ) )
21	5 20	syl5ibcom	|- ( ph -> ( N = 0 -> ( ( A ^ 0 ) + ( B ^ 0 ) ) = ( C ^ 0 ) ) )
22	21	imp	|- ( ( ph /\ N = 0 ) -> ( ( A ^ 0 ) + ( B ^ 0 ) ) = ( C ^ 0 ) )
23	15 22	mteqand	|- ( ph -> N =/= 0 )
24		elnnne0	|- ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
25	4 23 24	sylanbrc	|- ( ph -> N e. NN )