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	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	flt4lem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	flt4lem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	flt4lem1.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
	flt4lem1.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
	flt4lem1.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
Assertion	flt4lem1	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flt4lem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		flt4lem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		flt4lem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4		flt4lem1.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
5		flt4lem1.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
6		flt4lem1.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
7	1 2 3	3jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) )
8	1 2 3 5 6	fltabcoprm	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
9	8 4	jca	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) )
10	7 6 9	3jca	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) )