pythagtriplem4

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

		Ref	Expression
	Assertion	pythagtriplem4	$⊢ ((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 (C - B) \gcd (C + B) = 1$

Proof

Step	Hyp	Ref	Expression
1		simp3r	$⊢ ((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 \neg 2 ∥ A$
2		nnz	$⊢ C \in ℕ \to C \in ℤ$
3		nnz	$⊢ B \in ℕ \to B \in ℤ$
4		zsubcl	$⊢ (C \in ℤ \land B \in ℤ) \to C - B \in ℤ$
5	2 3 4	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C - B \in ℤ$
6	5	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℤ$
7	6	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 C - B \in ℤ$
8		simp13	$⊢ ((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 C \in ℕ$
9		simp12	$⊢ ((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 \in ℕ$
10	8 9	nnaddcld	$⊢ ((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 C + B \in ℕ$
11	10	nnzd	$⊢ ((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 C + B \in ℤ$
12		gcddvds	$⊢ (C - B \in ℤ \land C + B \in ℤ) \to (((C - B) \gcd (C + B)) ∥ (C - B) \land ((C - B) \gcd (C + B)) ∥ (C + B))$
13	7 11 12	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 (((C - B) \gcd (C + B)) ∥ (C - B) \land ((C - B) \gcd (C + B)) ∥ (C + B))$
14	13	simprd	$⊢ ((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 ((C - B) \gcd (C + B)) ∥ (C + B)$
15		breq1	$⊢ (C - B) \gcd (C + B) = 2 \to (((C - B) \gcd (C + B)) ∥ (C + B) \leftrightarrow 2 ∥ (C + B))$
16	15	biimpd	$⊢ (C - B) \gcd (C + B) = 2 \to (((C - B) \gcd (C + B)) ∥ (C + B) \to 2 ∥ (C + B))$
17	14 16	mpan9	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to 2 ∥ (C + B)$
18		2z	$⊢ 2 \in ℤ$
19		simpl13	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to C \in ℕ$
20	19	nnzd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to C \in ℤ$
21		simpl12	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to B \in ℕ$
22	21	nnzd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to B \in ℤ$
23	20 22	zaddcld	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to C + B \in ℤ$
24	20 22	zsubcld	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to C - B \in ℤ$
25		dvdsmultr1	$⊢ (2 \in ℤ \land C + B \in ℤ \land C - B \in ℤ) \to (2 ∥ (C + B) \to 2 ∥ (C + B) (C - B))$
26	18 23 24 25	mp3an2i	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to (2 ∥ (C + B) \to 2 ∥ (C + B) (C - B))$
27	17 26	mpd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to 2 ∥ (C + B) (C - B)$
28	19	nncnd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to C \in ℂ$
29	21	nncnd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to B \in ℂ$
30		subsq	$⊢ (C \in ℂ \land B \in ℂ) \to C^{2} - B^{2} = (C + B) (C - B)$
31	28 29 30	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)) \land (C - B) \gcd (C + B) = 2) \to C^{2} - B^{2} = (C + B) (C - B)$
32	27 31	breqtrrd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to 2 ∥ (C^{2} - B^{2})$
33		simpl2	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to A^{2} + B^{2} = C^{2}$
34	33	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)) \land (C - B) \gcd (C + B) = 2) \to A^{2} + B^{2} - B^{2} = C^{2} - B^{2}$
35		simpl11	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to A \in ℕ$
36	35	nnsqcld	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to A^{2} \in ℕ$
37	36	nncnd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to A^{2} \in ℂ$
38	21	nnsqcld	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to B^{2} \in ℕ$
39	38	nncnd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to B^{2} \in ℂ$
40	37 39	pncand	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to A^{2} + B^{2} - B^{2} = A^{2}$
41	34 40	eqtr3d	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to C^{2} - B^{2} = A^{2}$
42	32 41	breqtrd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to 2 ∥ A^{2}$
43		nnz	$⊢ A \in ℕ \to A \in ℤ$
44	43	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
45	44	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 A \in ℤ$
46	45	adantr	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to A \in ℤ$
47		2prm	$⊢ 2 \in ℙ$
48		2nn	$⊢ 2 \in ℕ$
49		prmdvdsexp	$⊢ (2 \in ℙ \land A \in ℤ \land 2 \in ℕ) \to (2 ∥ A^{2} \leftrightarrow 2 ∥ A)$
50	47 48 49	mp3an13	$⊢ A \in ℤ \to (2 ∥ A^{2} \leftrightarrow 2 ∥ A)$
51	46 50	syl	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land (C - B) \gcd (C + B) = 2) \to (2 ∥ A^{2} \leftrightarrow 2 ∥ A)$
52	42 51	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)) \land (C - B) \gcd (C + B) = 2) \to 2 ∥ A$
53	1 52	mtand	$⊢ ((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 \neg (C - B) \gcd (C + B) = 2$
54		neg1z	$⊢ - 1 \in ℤ$
55		gcdaddm	$⊢ (- 1 \in ℤ \land C - B \in ℤ \land C + B \in ℤ) \to (C - B) \gcd (C + B) = (C - B) \gcd (C + B + -1 (C - B))$
56	54 7 11 55	mp3an2i	$⊢ ((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 (C - B) \gcd (C + B) = (C - B) \gcd (C + B + -1 (C - B))$
57	8	nncnd	$⊢ ((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 C \in ℂ$
58	9	nncnd	$⊢ ((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 \in ℂ$
59		pnncan	$⊢ (C \in ℂ \land B \in ℂ \land B \in ℂ) \to C + B - (C - B) = B + B$
60	59	3anidm23	$⊢ (C \in ℂ \land B \in ℂ) \to C + B - (C - B) = B + B$
61		subcl	$⊢ (C \in ℂ \land B \in ℂ) \to C - B \in ℂ$
62	61	mulm1d	$⊢ (C \in ℂ \land B \in ℂ) \to -1 (C - B) = - (C - B)$
63	62	oveq2d	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + -1 (C - B) = C + B + (- (C - B))$
64		addcl	$⊢ (C \in ℂ \land B \in ℂ) \to C + B \in ℂ$
65	64 61	negsubd	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + (- (C - B)) = C + B - (C - B)$
66	63 65	eqtrd	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + -1 (C - B) = C + B - (C - B)$
67		2times	$⊢ B \in ℂ \to 2 B = B + B$
68	67	adantl	$⊢ (C \in ℂ \land B \in ℂ) \to 2 B = B + B$
69	60 66 68	3eqtr4d	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + -1 (C - B) = 2 B$
70	69	oveq2d	$⊢ (C \in ℂ \land B \in ℂ) \to (C - B) \gcd (C + B + -1 (C - B)) = (C - B) \gcd 2 B$
71	57 58 70	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 (C - B) \gcd (C + B + -1 (C - B)) = (C - B) \gcd 2 B$
72	56 71	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 (C - B) \gcd (C + B) = (C - B) \gcd 2 B$
73	9	nnzd	$⊢ ((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 \in ℤ$
74		zmulcl	$⊢ (2 \in ℤ \land B \in ℤ) \to 2 B \in ℤ$
75	18 73 74	sylancr	$⊢ ((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 2 B \in ℤ$
76		gcddvds	$⊢ (C - B \in ℤ \land 2 B \in ℤ) \to (((C - B) \gcd 2 B) ∥ (C - B) \land ((C - B) \gcd 2 B) ∥ 2 B)$
77	7 75 76	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 (((C - B) \gcd 2 B) ∥ (C - B) \land ((C - B) \gcd 2 B) ∥ 2 B)$
78	77	simprd	$⊢ ((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 ((C - B) \gcd 2 B) ∥ 2 B$
79	72 78	eqbrtrd	$⊢ ((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 ((C - B) \gcd (C + B)) ∥ 2 B$
80		1z	$⊢ 1 \in ℤ$
81		gcdaddm	$⊢ (1 \in ℤ \land C - B \in ℤ \land C + B \in ℤ) \to (C - B) \gcd (C + B) = (C - B) \gcd (C + B + 1 (C - B))$
82	80 7 11 81	mp3an2i	$⊢ ((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 (C - B) \gcd (C + B) = (C - B) \gcd (C + B + 1 (C - B))$
83		ppncan	$⊢ (C \in ℂ \land B \in ℂ \land C \in ℂ) \to C + B + (C - B) = C + C$
84	83	3anidm13	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + (C - B) = C + C$
85	61	mulid2d	$⊢ (C \in ℂ \land B \in ℂ) \to 1 (C - B) = C - B$
86	85	oveq2d	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + 1 (C - B) = C + B + (C - B)$
87		2times	$⊢ C \in ℂ \to 2 C = C + C$
88	87	adantr	$⊢ (C \in ℂ \land B \in ℂ) \to 2 C = C + C$
89	84 86 88	3eqtr4d	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + 1 (C - B) = 2 C$
90	57 58 89	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 C + B + 1 (C - B) = 2 C$
91	90	oveq2d	$⊢ ((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 (C - B) \gcd (C + B + 1 (C - B)) = (C - B) \gcd 2 C$
92	82 91	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 (C - B) \gcd (C + B) = (C - B) \gcd 2 C$
93	8	nnzd	$⊢ ((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 C \in ℤ$
94		zmulcl	$⊢ (2 \in ℤ \land C \in ℤ) \to 2 C \in ℤ$
95	18 93 94	sylancr	$⊢ ((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 2 C \in ℤ$
96		gcddvds	$⊢ (C - B \in ℤ \land 2 C \in ℤ) \to (((C - B) \gcd 2 C) ∥ (C - B) \land ((C - B) \gcd 2 C) ∥ 2 C)$
97	7 95 96	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 (((C - B) \gcd 2 C) ∥ (C - B) \land ((C - B) \gcd 2 C) ∥ 2 C)$
98	97	simprd	$⊢ ((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 ((C - B) \gcd 2 C) ∥ 2 C$
99	92 98	eqbrtrd	$⊢ ((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 ((C - B) \gcd (C + B)) ∥ 2 C$
100		nnaddcl	$⊢ (C \in ℕ \land B \in ℕ) \to C + B \in ℕ$
101	100	nnne0d	$⊢ (C \in ℕ \land B \in ℕ) \to C + B \neq 0$
102	101	ancoms	$⊢ (B \in ℕ \land C \in ℕ) \to C + B \neq 0$
103	102	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \neq 0$
104	103	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 C + B \neq 0$
105	104	neneqd	$⊢ ((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 \neg C + B = 0$
106	105	intnand	$⊢ ((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 \neg (C - B = 0 \land C + B = 0)$
107		gcdn0cl	$⊢ ((C - B \in ℤ \land C + B \in ℤ) \land \neg (C - B = 0 \land C + B = 0)) \to (C - B) \gcd (C + B) \in ℕ$
108	7 11 106 107	syl21anc	$⊢ ((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 (C - B) \gcd (C + B) \in ℕ$
109	108	nnzd	$⊢ ((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 (C - B) \gcd (C + B) \in ℤ$
110		dvdsgcd	$⊢ ((C - B) \gcd (C + B) \in ℤ \land 2 B \in ℤ \land 2 C \in ℤ) \to ((((C - B) \gcd (C + B)) ∥ 2 B \land ((C - B) \gcd (C + B)) ∥ 2 C) \to ((C - B) \gcd (C + B)) ∥ (2 B \gcd 2 C))$
111	109 75 95 110	syl3anc	$⊢ ((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 ((((C - B) \gcd (C + B)) ∥ 2 B \land ((C - B) \gcd (C + B)) ∥ 2 C) \to ((C - B) \gcd (C + B)) ∥ (2 B \gcd 2 C))$
112	79 99 111	mp2and	$⊢ ((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 ((C - B) \gcd (C + B)) ∥ (2 B \gcd 2 C)$
113		2nn0	$⊢ 2 \in ℕ_{0}$
114		mulgcd	$⊢ (2 \in ℕ_{0} \land B \in ℤ \land C \in ℤ) \to 2 B \gcd 2 C = 2 (B \gcd C)$
115	113 73 93 114	mp3an2i	$⊢ ((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 2 B \gcd 2 C = 2 (B \gcd C)$
116		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$
117	116	oveq2d	$⊢ ((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 2 (B \gcd C) = 2 \cdot 1$
118		2t1e2	$⊢ 2 \cdot 1 = 2$
119	117 118	eqtrdi	$⊢ ((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 2 (B \gcd C) = 2$
120	115 119	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 2 B \gcd 2 C = 2$
121	112 120	breqtrd	$⊢ ((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 ((C - B) \gcd (C + B)) ∥ 2$
122		dvdsprime	$⊢ (2 \in ℙ \land (C - B) \gcd (C + B) \in ℕ) \to (((C - B) \gcd (C + B)) ∥ 2 \leftrightarrow ((C - B) \gcd (C + B) = 2 \lor (C - B) \gcd (C + B) = 1))$
123	47 108 122	sylancr	$⊢ ((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 (((C - B) \gcd (C + B)) ∥ 2 \leftrightarrow ((C - B) \gcd (C + B) = 2 \lor (C - B) \gcd (C + B) = 1))$
124	121 123	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 ((C - B) \gcd (C + B) = 2 \lor (C - B) \gcd (C + B) = 1)$
125		orel1	$⊢ \neg (C - B) \gcd (C + B) = 2 \to (((C - B) \gcd (C + B) = 2 \lor (C - B) \gcd (C + B) = 1) \to (C - B) \gcd (C + B) = 1)$
126	53 124 125	sylc	$⊢ ((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 (C - B) \gcd (C + B) = 1$

Metamath Proof Explorer

Theorem pythagtriplem4

Proof