pythagtriplem3

Description: Lemma for pythagtrip . Show that C and B are relatively prime under some conditions. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	pythagtriplem3	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to B \gcd C = 1$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ A^{2} + B^{2} = C^{2} \to B^{2} \gcd (A^{2} + B^{2}) = B^{2} \gcd C^{2}$
2	1	adantl	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B^{2} \gcd (A^{2} + B^{2}) = B^{2} \gcd C^{2}$
3		nnz	$⊢ B \in ℕ \to B \in ℤ$
4		zsqcl	$⊢ B \in ℤ \to B^{2} \in ℤ$
5	3 4	syl	$⊢ B \in ℕ \to B^{2} \in ℤ$
6	5	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \in ℤ$
7		nnz	$⊢ A \in ℕ \to A \in ℤ$
8		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
9	7 8	syl	$⊢ A \in ℕ \to A^{2} \in ℤ$
10	9	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} \in ℤ$
11		gcdadd	$⊢ (B^{2} \in ℤ \land A^{2} \in ℤ) \to B^{2} \gcd A^{2} = B^{2} \gcd (A^{2} + B^{2})$
12	6 10 11	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \gcd A^{2} = B^{2} \gcd (A^{2} + B^{2})$
13	6 10	gcdcomd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \gcd A^{2} = A^{2} \gcd B^{2}$
14	12 13	eqtr3d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \gcd (A^{2} + B^{2}) = A^{2} \gcd B^{2}$
15	14	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B^{2} \gcd (A^{2} + B^{2}) = A^{2} \gcd B^{2}$
16	2 15	eqtr3d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B^{2} \gcd C^{2} = A^{2} \gcd B^{2}$
17		simpl2	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B \in ℕ$
18		simpl3	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to C \in ℕ$
19		sqgcd	$⊢ (B \in ℕ \land C \in ℕ) \to {(B \gcd C)}^{2} = B^{2} \gcd C^{2}$
20	17 18 19	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to {(B \gcd C)}^{2} = B^{2} \gcd C^{2}$
21		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to A \in ℕ$
22		sqgcd	$⊢ (A \in ℕ \land B \in ℕ) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$
23	21 17 22	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$
24	16 20 23	3eqtr4d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to {(B \gcd C)}^{2} = {(A \gcd B)}^{2}$
25	24	3adant3	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {(B \gcd C)}^{2} = {(A \gcd B)}^{2}$
26		simp3l	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to A \gcd B = 1$
27	26	oveq1d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {(A \gcd B)}^{2} = 1^{2}$
28	25 27	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {(B \gcd C)}^{2} = 1^{2}$
29	3	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℤ$
30		nnz	$⊢ C \in ℕ \to C \in ℤ$
31	30	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℤ$
32	29 31	gcdcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \gcd C \in ℕ_{0}$
33	32	nn0red	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \gcd C \in ℝ$
34	33	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to B \gcd C \in ℝ$
35	32	nn0ge0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 \leq B \gcd C$
36	35	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 \leq B \gcd C$
37		1re	$⊢ 1 \in ℝ$
38		0le1	$⊢ 0 \leq 1$
39		sq11	$⊢ ((B \gcd C \in ℝ \land 0 \leq B \gcd C) \land (1 \in ℝ \land 0 \leq 1)) \to ({(B \gcd C)}^{2} = 1^{2} \leftrightarrow B \gcd C = 1)$
40	37 38 39	mpanr12	$⊢ (B \gcd C \in ℝ \land 0 \leq B \gcd C) \to ({(B \gcd C)}^{2} = 1^{2} \leftrightarrow B \gcd C = 1)$
41	34 36 40	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to ({(B \gcd C)}^{2} = 1^{2} \leftrightarrow B \gcd C = 1)$
42	28 41	mpbid	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to B \gcd C = 1$

Metamath Proof Explorer

Theorem pythagtriplem3

Proof