Metamath Proof Explorer

Theorem pythagtriplem13

Description: Lemma for pythagtrip . Show that N (which will eventually be closely related to the n in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypothesis pythagtriplem13.1 ⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
Assertion pythagtriplem13 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑁 ∈ ℕ )

Proof

Step Hyp Ref Expression
1 pythagtriplem13.1 ⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
2 pythagtriplem9 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℕ )
3 2 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℤ )
4 simp3r ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ¬ 2 ∥ 𝐴 )
5 2z ⊢ 2 ∈ ℤ
6 simp3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℕ )
7 simp2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℕ )
8 6 7 nnaddcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℕ )
9 8 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℤ )
10 9 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐵 ) ∈ ℤ )
11 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
12 11 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℤ )
13 12 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℤ )
14 dvdsgcdb ⊢ ( ( 2 ∈ ℤ ∧ ( 𝐶 + 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 2 ∥ ( 𝐶 + 𝐵 ) ∧ 2 ∥ 𝐴 ) ↔ 2 ∥ ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) ) )
15 5 10 13 14 mp3an2i ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 2 ∥ ( 𝐶 + 𝐵 ) ∧ 2 ∥ 𝐴 ) ↔ 2 ∥ ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) ) )
16 15 biimpar ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 2 ∥ ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) ) → ( 2 ∥ ( 𝐶 + 𝐵 ) ∧ 2 ∥ 𝐴 ) )
17 16 simprd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 2 ∥ ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) ) → 2 ∥ 𝐴 )
18 4 17 mtand ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ¬ 2 ∥ ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) )
19 pythagtriplem7 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) = ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) )
20 19 breq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 ∥ ( √ ‘ ( 𝐶 + 𝐵 ) ) ↔ 2 ∥ ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) ) )
21 18 20 mtbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ¬ 2 ∥ ( √ ‘ ( 𝐶 + 𝐵 ) ) )
22 pythagtriplem8 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℕ )
23 22 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℤ )
24 nnz ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℤ )
25 24 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℤ )
26 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
27 26 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℤ )
28 25 27 zsubcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℤ )
29 28 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) ∈ ℤ )
30 dvdsgcdb ⊢ ( ( 2 ∈ ℤ ∧ ( 𝐶 − 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 2 ∥ ( 𝐶 − 𝐵 ) ∧ 2 ∥ 𝐴 ) ↔ 2 ∥ ( ( 𝐶 − 𝐵 ) gcd 𝐴 ) ) )
31 5 29 13 30 mp3an2i ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 2 ∥ ( 𝐶 − 𝐵 ) ∧ 2 ∥ 𝐴 ) ↔ 2 ∥ ( ( 𝐶 − 𝐵 ) gcd 𝐴 ) ) )
32 31 biimpar ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 2 ∥ ( ( 𝐶 − 𝐵 ) gcd 𝐴 ) ) → ( 2 ∥ ( 𝐶 − 𝐵 ) ∧ 2 ∥ 𝐴 ) )
33 32 simprd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) ∧ 2 ∥ ( ( 𝐶 − 𝐵 ) gcd 𝐴 ) ) → 2 ∥ 𝐴 )
34 4 33 mtand ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ¬ 2 ∥ ( ( 𝐶 − 𝐵 ) gcd 𝐴 ) )
35 pythagtriplem6 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) = ( ( 𝐶 − 𝐵 ) gcd 𝐴 ) )
36 35 breq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 ∥ ( √ ‘ ( 𝐶 − 𝐵 ) ) ↔ 2 ∥ ( ( 𝐶 − 𝐵 ) gcd 𝐴 ) ) )
37 34 36 mtbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ¬ 2 ∥ ( √ ‘ ( 𝐶 − 𝐵 ) ) )
38 omoe ⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( √ ‘ ( 𝐶 + 𝐵 ) ) ) ∧ ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) → 2 ∥ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) )
39 3 21 23 37 38 syl22anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 2 ∥ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) )
40 28 zred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
41 40 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
42 simp13 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 ∈ ℕ )
43 42 nnred ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 ∈ ℝ )
44 8 nnred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
45 44 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
46 nnrp ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
47 46 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℝ+ )
48 47 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 ∈ ℝ+ )
49 43 48 ltsubrpd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) < 𝐶 )
50 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
51 50 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐵 )
52 51 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < 𝐵 )
53 simp12 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 ∈ ℕ )
54 53 nnred ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 ∈ ℝ )
55 54 43 ltaddposd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 0 < 𝐵 ↔ 𝐶 < ( 𝐶 + 𝐵 ) ) )
56 52 55 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 < ( 𝐶 + 𝐵 ) )
57 41 43 45 49 56 lttrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) < ( 𝐶 + 𝐵 ) )
58 pythagtriplem10 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 0 < ( 𝐶 − 𝐵 ) )
59 58 3adant3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < ( 𝐶 − 𝐵 ) )
60 0re ⊢ 0 ∈ ℝ
61 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 − 𝐵 ) ∈ ℝ ) → ( 0 < ( 𝐶 − 𝐵 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) )
62 60 61 mpan ⊢ ( ( 𝐶 − 𝐵 ) ∈ ℝ → ( 0 < ( 𝐶 − 𝐵 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) )
63 41 59 62 sylc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐶 − 𝐵 ) )
64 nngt0 ⊢ ( 𝐶 ∈ ℕ → 0 < 𝐶 )
65 64 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐶 )
66 65 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < 𝐶 )
67 43 54 66 52 addgt0d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < ( 𝐶 + 𝐵 ) )
68 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ) → ( 0 < ( 𝐶 + 𝐵 ) → 0 ≤ ( 𝐶 + 𝐵 ) ) )
69 60 68 mpan ⊢ ( ( 𝐶 + 𝐵 ) ∈ ℝ → ( 0 < ( 𝐶 + 𝐵 ) → 0 ≤ ( 𝐶 + 𝐵 ) ) )
70 45 67 69 sylc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐶 + 𝐵 ) )
71 41 63 45 70 sqrtltd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 − 𝐵 ) < ( 𝐶 + 𝐵 ) ↔ ( √ ‘ ( 𝐶 − 𝐵 ) ) < ( √ ‘ ( 𝐶 + 𝐵 ) ) ) )
72 57 71 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) < ( √ ‘ ( 𝐶 + 𝐵 ) ) )
73 nnsub ⊢ ( ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℕ ∧ ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℕ ) → ( ( √ ‘ ( 𝐶 − 𝐵 ) ) < ( √ ‘ ( 𝐶 + 𝐵 ) ) ↔ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℕ ) )
74 22 2 73 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 − 𝐵 ) ) < ( √ ‘ ( 𝐶 + 𝐵 ) ) ↔ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℕ ) )
75 72 74 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℕ )
76 75 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℤ )
77 evend2 ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℤ → ( 2 ∥ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↔ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℤ ) )
78 76 77 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 ∥ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↔ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℤ ) )
79 39 78 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℤ )
80 75 nngt0d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) )
81 75 nnred ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℝ )
82 halfpos2 ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℝ → ( 0 < ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↔ 0 < ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) )
83 81 82 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 0 < ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↔ 0 < ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) )
84 80 83 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) )
85 elnnz ⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℕ ↔ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℤ ∧ 0 < ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) )
86 79 84 85 sylanbrc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℕ )
87 1 86 eqeltrid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑁 ∈ ℕ )