Theorem flt4lem1 28003

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

Hypotheses

Ref	Expression
flt4lem1.a	⊢ (𝜑 → 𝐴 ∈ ℕ)
flt4lem1.b	⊢ (𝜑 → 𝐵 ∈ ℕ)
flt4lem1.c	⊢ (𝜑 → 𝐶 ∈ ℕ)
flt4lem1.1	⊢ (𝜑 → ¬ 2 ∥ 𝐴)
flt4lem1.2	⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
flt4lem1.3	⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))

Assertion

Ref	Expression
flt4lem1	⊢ (𝜑 → ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)))

Proof of Theorem flt4lem1

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   class class class wbr 5106  (class class class)co 7440  1c1 11225   + caddc 11227  ℕcn 12359  2c2 12421  ↑cexp 14228   ∥ cdvds 16448   gcd cgcd 16690

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  flt4lem5a  28009  flt4lem5b  28010  flt4lem5c  28011  flt4lem5d  28012  flt4lem5e  28013