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	$$⊢\phi \to A\in \mathbb{N}$$
	flt4lem1.b	$$⊢\phi \to B\in \mathbb{N}$$
	flt4lem1.c	$$⊢\phi \to C\in \mathbb{N}$$
	flt4lem1.1	$$⊢\phi \to \neg 2\parallel A$$
	flt4lem1.2	$$⊢\phi \to A\gcd C=1$$
	flt4lem1.3	$$⊢\phi \to A^2+B^2=C^2$$
Assertion	flt4lem1	$$⊢\phi \to \left(\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\wedge C\in \mathbb{N}\right)\wedge A^2+B^2=C^2\wedge \left(A\gcd B=1\wedge \neg 2\parallel A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		flt4lem1.a	$$⊢\phi \to A\in \mathbb{N}$$
2		flt4lem1.b	$$⊢\phi \to B\in \mathbb{N}$$
3		flt4lem1.c	$$⊢\phi \to C\in \mathbb{N}$$
4		flt4lem1.1	$$⊢\phi \to \neg 2\parallel A$$
5		flt4lem1.2	$$⊢\phi \to A\gcd C=1$$
6		flt4lem1.3	$$⊢\phi \to A^2+B^2=C^2$$
7	1 2 3	3jca	$$⊢\phi \to \left(A\in \mathbb{N}\wedge B\in \mathbb{N}\wedge C\in \mathbb{N}\right)$$
8	1 2 3 5 6	fltabcoprm	$$⊢\phi \to A\gcd B=1$$
9	8 4	jca	$$⊢\phi \to \left(A\gcd B=1\wedge \neg 2\parallel A\right)$$
10	7 6 9	3jca	$$⊢\phi \to \left(\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\wedge C\in \mathbb{N}\right)\wedge A^2+B^2=C^2\wedge \left(A\gcd B=1\wedge \neg 2\parallel A\right)\right)$$