flt4lem1

Description: Satisfy the antecedent used in several pythagtrip lemmas. (Contributed by SN, 21-Aug-2024)

	Ref	Expression
Hypotheses	flt4lem1.a	$⊢ φ \to A \in ℕ$
	flt4lem1.b	$⊢ φ \to B \in ℕ$
	flt4lem1.c	$⊢ φ \to C \in ℕ$
	flt4lem1.1	$⊢ φ \to \neg 2 ∥ A$
	flt4lem1.2	$⊢ φ \to A \gcd B = 1$
	flt4lem1.3	$⊢ φ \to A^{2} + B^{2} = C^{2}$
Assertion	flt4lem1	$⊢ φ \to ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A))$

Step	Hyp	Ref	Expression
1		flt4lem1.a	$⊢ φ \to A \in ℕ$
2		flt4lem1.b	$⊢ φ \to B \in ℕ$
3		flt4lem1.c	$⊢ φ \to C \in ℕ$
4		flt4lem1.1	$⊢ φ \to \neg 2 ∥ A$
5		flt4lem1.2	$⊢ φ \to A \gcd B = 1$
6		flt4lem1.3	$⊢ φ \to A^{2} + B^{2} = C^{2}$
7	1 2 3	3jca	$⊢ φ \to (A \in ℕ \land B \in ℕ \land C \in ℕ)$
8	5 4	jca	$⊢ φ \to (A \gcd B = 1 \land \neg 2 ∥ A)$
9	7 6 8	3jca	$⊢ φ \to ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A))$

Metamath Proof Explorer