Theorem 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	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 − 𝐵 ) gcd ( 𝐶 + 𝐵 ) ) = 1 )

Proof

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