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	1 2 3 4 5 6	flt4lem2	⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )
13		2nn0	⊢ 2 ∈ ℕ0
14	13	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
15	1 2 3 5 6	fltabcoprm	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
16	1 2 3 14 6 15	fltbccoprm	⊢ ( 𝜑 → ( 𝐵 gcd 𝐶 ) = 1 )
17	2	nnsqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℕ )
18	17	nncnd	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
19	1	nnsqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
20	19	nncnd	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
21	18 20	addcomd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
22	21 6	eqtrd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
23	2 1 3 12 16 22	flt4lem1	⊢ ( 𝜑 → ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐵 gcd 𝐴 ) = 1 ∧ ¬ 2 ∥ 𝐵 ) ) )
24		pythagtriplem4	⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐵 gcd 𝐴 ) = 1 ∧ ¬ 2 ∥ 𝐵 ) ) → ( ( 𝐶 − 𝐴 ) gcd ( 𝐶 + 𝐴 ) ) = 1 )
25	23 24	syl	⊢ ( 𝜑 → ( ( 𝐶 − 𝐴 ) gcd ( 𝐶 + 𝐴 ) ) = 1 )
26	11 25	eqtrd	⊢ ( 𝜑 → ( ( 𝐶 + 𝐴 ) gcd ( 𝐶 − 𝐴 ) ) = 1 )