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 C ) = 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 C ) = 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	1 2 3 4 5 6	flt4lem2	|- ( ph -> -. 2 || B )
13		2nn0	|- 2 e. NN0
14	13	a1i	|- ( ph -> 2 e. NN0 )
15	1 2 3 5 6	fltabcoprm	|- ( ph -> ( A gcd B ) = 1 )
16	1 2 3 14 6 15	fltbccoprm	|- ( ph -> ( B gcd C ) = 1 )
17	2	nnsqcld	|- ( ph -> ( B ^ 2 ) e. NN )
18	17	nncnd	|- ( ph -> ( B ^ 2 ) e. CC )
19	1	nnsqcld	|- ( ph -> ( A ^ 2 ) e. NN )
20	19	nncnd	|- ( ph -> ( A ^ 2 ) e. CC )
21	18 20	addcomd	|- ( ph -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
22	21 6	eqtrd	|- ( ph -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) )
23	2 1 3 12 16 22	flt4lem1	|- ( ph -> ( ( B e. NN /\ A e. NN /\ C e. NN ) /\ ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) /\ ( ( B gcd A ) = 1 /\ -. 2 || B ) ) )
24		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 )
25	23 24	syl	|- ( ph -> ( ( C - A ) gcd ( C + A ) ) = 1 )
26	11 25	eqtrd	|- ( ph -> ( ( C + A ) gcd ( C - A ) ) = 1 )