flt4lem3

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

Step	Hyp	Ref	Expression
1		flt4lem3.a	$⊢ φ \to A \in ℕ$
2		flt4lem3.b	$⊢ φ \to B \in ℕ$
3		flt4lem3.c	$⊢ φ \to C \in ℕ$
4		flt4lem3.1	$⊢ φ \to 2 ∥ A$
5		flt4lem3.2	$⊢ φ \to A \gcd C = 1$
6		flt4lem3.3	$⊢ φ \to A^{2} + B^{2} = C^{2}$
7	3	nnzd	$⊢ φ \to C \in ℤ$
8	1	nnzd	$⊢ φ \to A \in ℤ$
9	7 8	zaddcld	$⊢ φ \to C + A \in ℤ$
10	7 8	zsubcld	$⊢ φ \to C - A \in ℤ$
11	9 10	gcdcomd	$⊢ φ \to (C + A) \gcd (C - A) = (C - A) \gcd (C + A)$
12	1 2 3 4 5 6	flt4lem2	$⊢ φ \to \neg 2 ∥ B$
13		2nn0	$⊢ 2 \in ℕ_{0}$
14	13	a1i	$⊢ φ \to 2 \in ℕ_{0}$
15	1 2 3 5 6	fltabcoprm	$⊢ φ \to A \gcd B = 1$
16	1 2 3 14 6 15	fltbccoprm	$⊢ φ \to B \gcd C = 1$
17	2	nnsqcld	$⊢ φ \to B^{2} \in ℕ$
18	17	nncnd	$⊢ φ \to B^{2} \in ℂ$
19	1	nnsqcld	$⊢ φ \to A^{2} \in ℕ$
20	19	nncnd	$⊢ φ \to A^{2} \in ℂ$
21	18 20	addcomd	$⊢ φ \to B^{2} + A^{2} = A^{2} + B^{2}$
22	21 6	eqtrd	$⊢ φ \to B^{2} + A^{2} = C^{2}$
23	2 1 3 12 16 22	flt4lem1	$⊢ φ \to ((B \in ℕ \land A \in ℕ \land C \in ℕ) \land B^{2} + A^{2} = C^{2} \land (B \gcd A = 1 \land \neg 2 ∥ B))$
24		pythagtriplem4	$⊢ ((B \in ℕ \land A \in ℕ \land C \in ℕ) \land B^{2} + A^{2} = C^{2} \land (B \gcd A = 1 \land \neg 2 ∥ B)) \to (C - A) \gcd (C + A) = 1$
25	23 24	syl	$⊢ φ \to (C - A) \gcd (C + A) = 1$
26	11 25	eqtrd	$⊢ φ \to (C + A) \gcd (C - A) = 1$

Metamath Proof Explorer