Metamath Proof Explorer

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 )