Theorem flt4lem1

Description: Satisfy the antecedent used in several pythagtrip lemmas, with A , C coprime rather than A , B . (Contributed by SN, 21-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		flt4lem1.a	|- ( ph -> A e. NN )
2		flt4lem1.b	|- ( ph -> B e. NN )
3		flt4lem1.c	|- ( ph -> C e. NN )
4		flt4lem1.1	|- ( ph -> -. 2 || A )
5		flt4lem1.2	|- ( ph -> ( A gcd C ) = 1 )
6		flt4lem1.3	|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
7	1 2 3	3jca	|- ( ph -> ( A e. NN /\ B e. NN /\ C e. NN ) )
8	1 2 3 5 6	fltabcoprm	|- ( ph -> ( A gcd B ) = 1 )
9	8 4	jca	|- ( ph -> ( ( A gcd B ) = 1 /\ -. 2 || A ) )
10	7 6 9	3jca	|- ( ph -> ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) )