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	$$⊢\phi \to A\in \mathbb{N}$$
	flt4lem3.b	$$⊢\phi \to B\in \mathbb{N}$$
	flt4lem3.c	$$⊢\phi \to C\in \mathbb{N}$$
	flt4lem3.1	$$⊢\phi \to 2\parallel A$$
	flt4lem3.2	$$⊢\phi \to A\gcd B=1$$
	flt4lem3.3	$$⊢\phi \to A^2+B^2=C^2$$
Assertion	flt4lem3	$$⊢\phi \to \left(C+A\right)\gcd \left(C-A\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		flt4lem3.a	$$⊢\phi \to A\in \mathbb{N}$$
2		flt4lem3.b	$$⊢\phi \to B\in \mathbb{N}$$
3		flt4lem3.c	$$⊢\phi \to C\in \mathbb{N}$$
4		flt4lem3.1	$$⊢\phi \to 2\parallel A$$
5		flt4lem3.2	$$⊢\phi \to A\gcd B=1$$
6		flt4lem3.3	$$⊢\phi \to A^2+B^2=C^2$$
7	3	nnzd	$$⊢\phi \to C\in \mathbb{Z}$$
8	1	nnzd	$$⊢\phi \to A\in \mathbb{Z}$$
9	7 8	zaddcld	$$⊢\phi \to C+A\in \mathbb{Z}$$
10	7 8	zsubcld	$$⊢\phi \to C-A\in \mathbb{Z}$$
11	9 10	gcdcomd	$$⊢\phi \to \left(C+A\right)\gcd \left(C-A\right)=\left(C-A\right)\gcd \left(C+A\right)$$
12	2	nnsqcld	$$⊢\phi \to B^2\in \mathbb{N}$$
13	12	nncnd	$$⊢\phi \to B^2\in ℂ$$
14	1	nnsqcld	$$⊢\phi \to A^2\in \mathbb{N}$$
15	14	nncnd	$$⊢\phi \to A^2\in ℂ$$
16	13 15	addcomd	$$⊢\phi \to B^2+A^2=A^2+B^2$$
17	16 6	eqtrd	$$⊢\phi \to B^2+A^2=C^2$$
18	2	nnzd	$$⊢\phi \to B\in \mathbb{Z}$$
19	18 8	gcdcomd	$$⊢\phi \to B\gcd A=A\gcd B$$
20	19 5	eqtrd	$$⊢\phi \to B\gcd A=1$$
21	1 2 4 5	flt4lem2	$$⊢\phi \to \neg 2\parallel B$$
22		pythagtriplem4	$$⊢\left(\left(B\in \mathbb{N}\wedge A\in \mathbb{N}\wedge C\in \mathbb{N}\right)\wedge B^2+A^2=C^2\wedge \left(B\gcd A=1\wedge \neg 2\parallel B\right)\right)\to \left(C-A\right)\gcd \left(C+A\right)=1$$
23	2 1 3 17 20 21 22	syl312anc	$$⊢\phi \to \left(C-A\right)\gcd \left(C+A\right)=1$$
24	11 23	eqtrd	$$⊢\phi \to \left(C+A\right)\gcd \left(C-A\right)=1$$