Theorem flt4lem3

Description: Equivalent to pythagtriplem4 . Show that C + A and C - A are coprime. (Contributed by SN, 22-Aug-2024)

	Ref	Expression
Hypotheses	flt4lem3.a	|- ( ph -> A e. NN )
	flt4lem3.b	|- ( ph -> B e. NN )
	flt4lem3.c	|- ( ph -> C e. NN )
	flt4lem3.1	|- ( ph -> 2 || A )
	flt4lem3.2	|- ( ph -> ( A gcd B ) = 1 )
	flt4lem3.3	|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
Assertion	flt4lem3	|- ( ph -> ( ( C + A ) gcd ( C - A ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		flt4lem3.a	|- ( ph -> A e. NN )
2		flt4lem3.b	|- ( ph -> B e. NN )
3		flt4lem3.c	|- ( ph -> C e. NN )
4		flt4lem3.1	|- ( ph -> 2 || A )
5		flt4lem3.2	|- ( ph -> ( A gcd B ) = 1 )
6		flt4lem3.3	|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
7	3	nnzd	|- ( ph -> C e. ZZ )
8	1	nnzd	|- ( ph -> A e. ZZ )
9	7 8	zaddcld	|- ( ph -> ( C + A ) e. ZZ )
10	7 8	zsubcld	|- ( ph -> ( C - A ) e. ZZ )
11	9 10	gcdcomd	|- ( ph -> ( ( C + A ) gcd ( C - A ) ) = ( ( C - A ) gcd ( C + A ) ) )
12	2	nnsqcld	|- ( ph -> ( B ^ 2 ) e. NN )
13	12	nncnd	|- ( ph -> ( B ^ 2 ) e. CC )
14	1	nnsqcld	|- ( ph -> ( A ^ 2 ) e. NN )
15	14	nncnd	|- ( ph -> ( A ^ 2 ) e. CC )
16	13 15	addcomd	|- ( ph -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
17	16 6	eqtrd	|- ( ph -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) )
18	2	nnzd	|- ( ph -> B e. ZZ )
19	18 8	gcdcomd	|- ( ph -> ( B gcd A ) = ( A gcd B ) )
20	19 5	eqtrd	|- ( ph -> ( B gcd A ) = 1 )
21	1 2 4 5	flt4lem2	|- ( ph -> -. 2 || B )
22		pythagtriplem4	|- ( ( ( B e. NN /\ A e. NN /\ C e. NN ) /\ ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) /\ ( ( B gcd A ) = 1 /\ -. 2 || B ) ) -> ( ( C - A ) gcd ( C + A ) ) = 1 )
23	2 1 3 17 20 21 22	syl312anc	|- ( ph -> ( ( C - A ) gcd ( C + A ) ) = 1 )
24	11 23	eqtrd	|- ( ph -> ( ( C + A ) gcd ( C - A ) ) = 1 )