Theorem flt4lem3

Description: Equivalent to pythagtriplem4 . Show that C + A and C - A are coprime. (Contributed by SN, 22-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		flt4lem3.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		flt4lem3.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		flt4lem3.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4		flt4lem3.1	⊢ ( 𝜑 → 2 ∥ 𝐴 )
5		flt4lem3.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
6		flt4lem3.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
7	3	nnzd	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
8	1	nnzd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
9	7 8	zaddcld	⊢ ( 𝜑 → ( 𝐶 + 𝐴 ) ∈ ℤ )
10	7 8	zsubcld	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ∈ ℤ )
11	9 10	gcdcomd	⊢ ( 𝜑 → ( ( 𝐶 + 𝐴 ) gcd ( 𝐶 − 𝐴 ) ) = ( ( 𝐶 − 𝐴 ) gcd ( 𝐶 + 𝐴 ) ) )
12	2	nnsqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℕ )
13	12	nncnd	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
14	1	nnsqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
15	14	nncnd	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
16	13 15	addcomd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
17	16 6	eqtrd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
18	2	nnzd	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
19	18 8	gcdcomd	⊢ ( 𝜑 → ( 𝐵 gcd 𝐴 ) = ( 𝐴 gcd 𝐵 ) )
20	19 5	eqtrd	⊢ ( 𝜑 → ( 𝐵 gcd 𝐴 ) = 1 )
21	1 2 4 5	flt4lem2	⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )
22		pythagtriplem4	⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐵 gcd 𝐴 ) = 1 ∧ ¬ 2 ∥ 𝐵 ) ) → ( ( 𝐶 − 𝐴 ) gcd ( 𝐶 + 𝐴 ) ) = 1 )
23	2 1 3 17 20 21 22	syl312anc	⊢ ( 𝜑 → ( ( 𝐶 − 𝐴 ) gcd ( 𝐶 + 𝐴 ) ) = 1 )
24	11 23	eqtrd	⊢ ( 𝜑 → ( ( 𝐶 + 𝐴 ) gcd ( 𝐶 − 𝐴 ) ) = 1 )