Metamath Proof Explorer

Theorem pythagtriplem16

Description: Lemma for pythagtrip . Show the relationship between M , N , and B . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses pythagtriplem15.1 ⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
pythagtriplem15.2 ⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
Assertion pythagtriplem16 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 = ( 2 · ( 𝑀 · 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 pythagtriplem15.1 ⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
2 pythagtriplem15.2 ⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
3 1 2 oveq12i ⊢ ( 𝑀 · 𝑁 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) )
4 nncn ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℂ )
5 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
6 addcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
7 4 5 6 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
8 7 sqrtcld ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ )
9 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
10 4 5 9 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
11 10 sqrtcld ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
12 addcl ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ ∧ ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
13 8 11 12 syl2anc ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
14 13 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
15 14 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
16 subcl ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ ∧ ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
17 8 11 16 syl2anc ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
18 17 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
19 18 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
20 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
21 divmuldiv ⊢ ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ ∧ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ ) ∧ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / ( 2 · 2 ) ) )
22 20 20 21 mpanr12 ⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ ∧ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / ( 2 · 2 ) ) )
23 15 19 22 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / ( 2 · 2 ) ) )
24 13 17 mulcld ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
25 24 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
26 25 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
27 divdiv1 ⊢ ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / 2 ) / 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / ( 2 · 2 ) ) )
28 20 20 27 mp3an23 ⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ → ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / 2 ) / 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / ( 2 · 2 ) ) )
29 26 28 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / 2 ) / 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / ( 2 · 2 ) ) )
30 23 29 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / 2 ) / 2 ) )
31 nnre ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℝ )
32 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
33 readdcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
34 31 32 33 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
35 34 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
36 35 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
37 31 adantl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℝ )
38 32 adantr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℝ )
39 nngt0 ⊢ ( 𝐶 ∈ ℕ → 0 < 𝐶 )
40 39 adantl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐶 )
41 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
42 41 adantr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐵 )
43 37 38 40 42 addgt0d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < ( 𝐶 + 𝐵 ) )
44 0re ⊢ 0 ∈ ℝ
45 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ) → ( 0 < ( 𝐶 + 𝐵 ) → 0 ≤ ( 𝐶 + 𝐵 ) ) )
46 44 45 mpan ⊢ ( ( 𝐶 + 𝐵 ) ∈ ℝ → ( 0 < ( 𝐶 + 𝐵 ) → 0 ≤ ( 𝐶 + 𝐵 ) ) )
47 34 43 46 sylc ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 ≤ ( 𝐶 + 𝐵 ) )
48 47 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 ≤ ( 𝐶 + 𝐵 ) )
49 48 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐶 + 𝐵 ) )
50 resqrtth ⊢ ( ( ( 𝐶 + 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐶 + 𝐵 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) = ( 𝐶 + 𝐵 ) )
51 36 49 50 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) = ( 𝐶 + 𝐵 ) )
52 resubcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
53 31 32 52 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
54 53 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
55 54 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
56 pythagtriplem10 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 0 < ( 𝐶 − 𝐵 ) )
57 56 3adant3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < ( 𝐶 − 𝐵 ) )
58 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 − 𝐵 ) ∈ ℝ ) → ( 0 < ( 𝐶 − 𝐵 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) )
59 44 58 mpan ⊢ ( ( 𝐶 − 𝐵 ) ∈ ℝ → ( 0 < ( 𝐶 − 𝐵 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) )
60 55 57 59 sylc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐶 − 𝐵 ) )
61 resqrtth ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐶 − 𝐵 ) ) → ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) = ( 𝐶 − 𝐵 ) )
62 55 60 61 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) = ( 𝐶 − 𝐵 ) )
63 51 62 oveq12d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) = ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) )
64 63 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) / 2 ) = ( ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) / 2 ) )
65 simp12 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 ∈ ℕ )
66 simp13 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 ∈ ℕ )
67 65 66 8 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ )
68 65 66 11 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
69 subsq ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ ∧ ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) )
70 67 68 69 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) )
71 70 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) − ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) / 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / 2 ) )
72 pnncan ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) = ( 𝐵 + 𝐵 ) )
73 72 3anidm23 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) = ( 𝐵 + 𝐵 ) )
74 2times ⊢ ( 𝐵 ∈ ℂ → ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 ) )
75 74 adantl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 ) )
76 73 75 eqtr4d ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐵 ) )
77 4 5 76 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐵 ) )
78 77 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐵 ) )
79 78 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐵 ) )
80 79 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) / 2 ) = ( ( 2 · 𝐵 ) / 2 ) )
81 2cn ⊢ 2 ∈ ℂ
82 2ne0 ⊢ 2 ≠ 0
83 divcan3 ⊢ ( ( 𝐵 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝐵 ) / 2 ) = 𝐵 )
84 81 82 83 mp3an23 ⊢ ( 𝐵 ∈ ℂ → ( ( 2 · 𝐵 ) / 2 ) = 𝐵 )
85 65 5 84 3syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 2 · 𝐵 ) / 2 ) = 𝐵 )
86 80 85 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐵 ) − ( 𝐶 − 𝐵 ) ) / 2 ) = 𝐵 )
87 64 71 86 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / 2 ) = 𝐵 )
88 87 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) / 2 ) / 2 ) = ( 𝐵 / 2 ) )
89 30 88 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) = ( 𝐵 / 2 ) )
90 3 89 eqtrid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑀 · 𝑁 ) = ( 𝐵 / 2 ) )
91 90 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( 𝑀 · 𝑁 ) ) = ( 2 · ( 𝐵 / 2 ) ) )
92 divcan2 ⊢ ( ( 𝐵 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝐵 / 2 ) ) = 𝐵 )
93 81 82 92 mp3an23 ⊢ ( 𝐵 ∈ ℂ → ( 2 · ( 𝐵 / 2 ) ) = 𝐵 )
94 5 93 syl ⊢ ( 𝐵 ∈ ℕ → ( 2 · ( 𝐵 / 2 ) ) = 𝐵 )
95 94 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 2 · ( 𝐵 / 2 ) ) = 𝐵 )
96 95 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( 𝐵 / 2 ) ) = 𝐵 )
97 91 96 eqtr2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 = ( 2 · ( 𝑀 · 𝑁 ) ) )