This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pythagtriplem14

Description: Lemma for pythagtrip . Calculate the square of N . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 pythagtriplem13.1 ⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
2 1 oveq1i ⊢ ( 𝑁 ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 )
3 nncn ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℂ )
4 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
5 addcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
6 3 4 5 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
7 6 sqrtcld ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ )
8 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
9 3 4 8 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
10 9 sqrtcld ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
11 7 10 subcld ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
12 11 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
13 12 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
14 2cn ⊢ 2 ∈ ℂ
15 2ne0 ⊢ 2 ≠ 0
16 sqdiv ⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
17 14 15 16 mp3an23 ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
18 13 17 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
19 14 sqvali ⊢ ( 2 ↑ 2 ) = ( 2 · 2 )
20 19 oveq2i ⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) )
21 13 sqcld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
22 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
23 divdiv1 ⊢ ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / 2 ) / 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) ) )
24 22 22 23 mp3an23 ⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) ∈ ℂ → ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / 2 ) / 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) ) )
25 21 24 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / 2 ) / 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) ) )
26 simp12 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 ∈ ℕ )
27 simp13 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 ∈ ℕ )
28 26 27 7 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ )
29 26 27 10 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
30 binom2sub ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ ∧ ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) )
31 28 29 30 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) )
32 nnre ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℝ )
33 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
34 readdcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
35 32 33 34 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
36 35 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
37 36 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
38 37 recnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
39 resubcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
40 32 33 39 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
41 40 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
42 41 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
43 42 recnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
44 7 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ )
45 10 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
46 44 45 mulcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
47 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ ) → ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
48 14 46 47 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
49 48 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
50 38 43 49 addsubd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) = ( ( ( 𝐶 + 𝐵 ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( 𝐶 − 𝐵 ) ) )
51 27 nncnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 ∈ ℂ )
52 simp11 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℕ )
53 52 nncnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℂ )
54 subdi ⊢ ( ( 2 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · ( 𝐶 − 𝐴 ) ) = ( ( 2 · 𝐶 ) − ( 2 · 𝐴 ) ) )
55 14 51 53 54 mp3an2i ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( 𝐶 − 𝐴 ) ) = ( ( 2 · 𝐶 ) − ( 2 · 𝐴 ) ) )
56 ppncan ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) = ( 𝐶 + 𝐶 ) )
57 56 3anidm13 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) = ( 𝐶 + 𝐶 ) )
58 2times ⊢ ( 𝐶 ∈ ℂ → ( 2 · 𝐶 ) = ( 𝐶 + 𝐶 ) )
59 58 adantr ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐶 ) = ( 𝐶 + 𝐶 ) )
60 57 59 eqtr4d ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐶 ) )
61 3 4 60 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐶 ) )
62 61 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐶 ) )
63 62 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐶 ) )
64 26 nncnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 ∈ ℂ )
65 subsq ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) )
66 51 64 65 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) )
67 oveq1 ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
68 67 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
69 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
70 69 sqcld ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) ∈ ℂ )
71 70 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
72 4 sqcld ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ↑ 2 ) ∈ ℂ )
73 72 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
74 71 73 pncand ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐵 ↑ 2 ) ) = ( 𝐴 ↑ 2 ) )
75 74 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐵 ↑ 2 ) ) = ( 𝐴 ↑ 2 ) )
76 68 75 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( 𝐴 ↑ 2 ) )
77 66 76 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) = ( 𝐴 ↑ 2 ) )
78 77 fveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) ) = ( √ ‘ ( 𝐴 ↑ 2 ) ) )
79 32 adantl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℝ )
80 33 adantr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℝ )
81 nngt0 ⊢ ( 𝐶 ∈ ℕ → 0 < 𝐶 )
82 81 adantl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐶 )
83 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
84 83 adantr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐵 )
85 79 80 82 84 addgt0d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < ( 𝐶 + 𝐵 ) )
86 0re ⊢ 0 ∈ ℝ
87 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ) → ( 0 < ( 𝐶 + 𝐵 ) → 0 ≤ ( 𝐶 + 𝐵 ) ) )
88 86 87 mpan ⊢ ( ( 𝐶 + 𝐵 ) ∈ ℝ → ( 0 < ( 𝐶 + 𝐵 ) → 0 ≤ ( 𝐶 + 𝐵 ) ) )
89 35 85 88 sylc ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 ≤ ( 𝐶 + 𝐵 ) )
90 89 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 ≤ ( 𝐶 + 𝐵 ) )
91 90 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐶 + 𝐵 ) )
92 pythagtriplem10 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 0 < ( 𝐶 − 𝐵 ) )
93 92 3adant3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < ( 𝐶 − 𝐵 ) )
94 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 − 𝐵 ) ∈ ℝ ) → ( 0 < ( 𝐶 − 𝐵 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) )
95 86 94 mpan ⊢ ( ( 𝐶 − 𝐵 ) ∈ ℝ → ( 0 < ( 𝐶 − 𝐵 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) )
96 42 93 95 sylc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐶 − 𝐵 ) )
97 37 91 42 96 sqrtmuld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) ) = ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) )
98 78 97 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) )
99 nnre ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
100 99 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℝ )
101 100 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℝ )
102 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
103 102 nn0ge0d ⊢ ( 𝐴 ∈ ℕ → 0 ≤ 𝐴 )
104 103 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 ≤ 𝐴 )
105 104 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ 𝐴 )
106 101 105 sqrtsqd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )
107 98 106 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) = 𝐴 )
108 107 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) = ( 2 · 𝐴 ) )
109 63 108 oveq12d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) = ( ( 2 · 𝐶 ) − ( 2 · 𝐴 ) ) )
110 55 109 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( 𝐶 − 𝐴 ) ) = ( ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) )
111 resqrtth ⊢ ( ( ( 𝐶 + 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐶 + 𝐵 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) = ( 𝐶 + 𝐵 ) )
112 37 91 111 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) = ( 𝐶 + 𝐵 ) )
113 112 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) = ( ( 𝐶 + 𝐵 ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) )
114 resqrtth ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐶 − 𝐵 ) ) → ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) = ( 𝐶 − 𝐵 ) )
115 42 96 114 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) = ( 𝐶 − 𝐵 ) )
116 113 115 oveq12d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐶 + 𝐵 ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( 𝐶 − 𝐵 ) ) )
117 50 110 116 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( 𝐶 − 𝐴 ) ) )
118 31 117 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) = ( 2 · ( 𝐶 − 𝐴 ) ) )
119 118 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / 2 ) = ( ( 2 · ( 𝐶 − 𝐴 ) ) / 2 ) )
120 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
121 3 69 120 syl2anr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
122 121 3adant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
123 122 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
124 divcan3 ⊢ ( ( ( 𝐶 − 𝐴 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · ( 𝐶 − 𝐴 ) ) / 2 ) = ( 𝐶 − 𝐴 ) )
125 14 15 124 mp3an23 ⊢ ( ( 𝐶 − 𝐴 ) ∈ ℂ → ( ( 2 · ( 𝐶 − 𝐴 ) ) / 2 ) = ( 𝐶 − 𝐴 ) )
126 123 125 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 2 · ( 𝐶 − 𝐴 ) ) / 2 ) = ( 𝐶 − 𝐴 ) )
127 119 126 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / 2 ) = ( 𝐶 − 𝐴 ) )
128 127 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / 2 ) / 2 ) = ( ( 𝐶 − 𝐴 ) / 2 ) )
129 25 128 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) ) = ( ( 𝐶 − 𝐴 ) / 2 ) )
130 20 129 eqtrid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( 𝐶 − 𝐴 ) / 2 ) )
131 18 130 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( 𝐶 − 𝐴 ) / 2 ) )
132 2 131 eqtrid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑁 ↑ 2 ) = ( ( 𝐶 − 𝐴 ) / 2 ) )