Metamath Proof Explorer

Theorem pythagtriplem12

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

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

Proof

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