This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∥ 𝐴 ) ) )