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 
|- M = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 )
pythagtriplem15.2 
|- N = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
Assertion pythagtriplem16 
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B = ( 2 x. ( M x. N ) ) )

Proof

Step Hyp Ref Expression
1 pythagtriplem15.1 
 |-  M = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 )
2 pythagtriplem15.2 
 |-  N = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
3 1 2 oveq12i 
 |-  ( M x. N ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) )
4 nncn 
 |-  ( C e. NN -> C e. CC )
5 nncn 
 |-  ( B e. NN -> B e. CC )
6 addcl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C + B ) e. CC )
7 4 5 6 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( C + B ) e. CC )
8 7 sqrtcld 
 |-  ( ( B e. NN /\ C e. NN ) -> ( sqrt ` ( C + B ) ) e. CC )
9 subcl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C - B ) e. CC )
10 4 5 9 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( C - B ) e. CC )
11 10 sqrtcld 
 |-  ( ( B e. NN /\ C e. NN ) -> ( sqrt ` ( C - B ) ) e. CC )
12 addcl 
 |-  ( ( ( sqrt ` ( C + B ) ) e. CC /\ ( sqrt ` ( C - B ) ) e. CC ) -> ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) e. CC )
13 8 11 12 syl2anc 
 |-  ( ( B e. NN /\ C e. NN ) -> ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) e. CC )
14 13 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) e. CC )
15 14 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) e. CC )
16 subcl 
 |-  ( ( ( sqrt ` ( C + B ) ) e. CC /\ ( sqrt ` ( C - B ) ) e. CC ) -> ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. CC )
17 8 11 16 syl2anc 
 |-  ( ( B e. NN /\ C e. NN ) -> ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. CC )
18 17 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. CC )
19 18 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. CC )
20 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
21 divmuldiv 
 |-  ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) e. CC /\ ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. CC ) /\ ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) ) -> ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / ( 2 x. 2 ) ) )
22 20 20 21 mpanr12 
 |-  ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) e. CC /\ ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. CC ) -> ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / ( 2 x. 2 ) ) )
23 15 19 22 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / ( 2 x. 2 ) ) )
24 13 17 mulcld 
 |-  ( ( B e. NN /\ C e. NN ) -> ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) e. CC )
25 24 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) e. CC )
26 25 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) e. CC )
27 divdiv1 
 |-  ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / 2 ) / 2 ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / ( 2 x. 2 ) ) )
28 20 20 27 mp3an23 
 |-  ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) e. CC -> ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / 2 ) / 2 ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / ( 2 x. 2 ) ) )
29 26 28 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / 2 ) / 2 ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / ( 2 x. 2 ) ) )
30 23 29 eqtr4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / 2 ) / 2 ) )
31 nnre 
 |-  ( C e. NN -> C e. RR )
32 nnre 
 |-  ( B e. NN -> B e. RR )
33 readdcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + B ) e. RR )
34 31 32 33 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( C + B ) e. RR )
35 34 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. RR )
36 35 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( C + B ) e. RR )
37 31 adantl 
 |-  ( ( B e. NN /\ C e. NN ) -> C e. RR )
38 32 adantr 
 |-  ( ( B e. NN /\ C e. NN ) -> B e. RR )
39 nngt0 
 |-  ( C e. NN -> 0 < C )
40 39 adantl 
 |-  ( ( B e. NN /\ C e. NN ) -> 0 < C )
41 nngt0 
 |-  ( B e. NN -> 0 < B )
42 41 adantr 
 |-  ( ( B e. NN /\ C e. NN ) -> 0 < B )
43 37 38 40 42 addgt0d 
 |-  ( ( B e. NN /\ C e. NN ) -> 0 < ( C + B ) )
44 0re 
 |-  0 e. RR
45 ltle 
 |-  ( ( 0 e. RR /\ ( C + B ) e. RR ) -> ( 0 < ( C + B ) -> 0 <_ ( C + B ) ) )
46 44 45 mpan 
 |-  ( ( C + B ) e. RR -> ( 0 < ( C + B ) -> 0 <_ ( C + B ) ) )
47 34 43 46 sylc 
 |-  ( ( B e. NN /\ C e. NN ) -> 0 <_ ( C + B ) )
48 47 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 <_ ( C + B ) )
49 48 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 <_ ( C + B ) )
50 resqrtth 
 |-  ( ( ( C + B ) e. RR /\ 0 <_ ( C + B ) ) -> ( ( sqrt ` ( C + B ) ) ^ 2 ) = ( C + B ) )
51 36 49 50 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( sqrt ` ( C + B ) ) ^ 2 ) = ( C + B ) )
52 resubcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C - B ) e. RR )
53 31 32 52 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( C - B ) e. RR )
54 53 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. RR )
55 54 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( C - B ) e. RR )
56 pythagtriplem10 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C - B ) )
57 56 3adant3 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 < ( C - B ) )
58 ltle 
 |-  ( ( 0 e. RR /\ ( C - B ) e. RR ) -> ( 0 < ( C - B ) -> 0 <_ ( C - B ) ) )
59 44 58 mpan 
 |-  ( ( C - B ) e. RR -> ( 0 < ( C - B ) -> 0 <_ ( C - B ) ) )
60 55 57 59 sylc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 <_ ( C - B ) )
61 resqrtth 
 |-  ( ( ( C - B ) e. RR /\ 0 <_ ( C - B ) ) -> ( ( sqrt ` ( C - B ) ) ^ 2 ) = ( C - B ) )
62 55 60 61 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( sqrt ` ( C - B ) ) ^ 2 ) = ( C - B ) )
63 51 62 oveq12d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( sqrt ` ( C + B ) ) ^ 2 ) - ( ( sqrt ` ( C - B ) ) ^ 2 ) ) = ( ( C + B ) - ( C - B ) ) )
64 63 oveq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( ( sqrt ` ( C + B ) ) ^ 2 ) - ( ( sqrt ` ( C - B ) ) ^ 2 ) ) / 2 ) = ( ( ( C + B ) - ( C - B ) ) / 2 ) )
65 simp12 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B e. NN )
66 simp13 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C e. NN )
67 65 66 8 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( sqrt ` ( C + B ) ) e. CC )
68 65 66 11 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( sqrt ` ( C - B ) ) e. CC )
69 subsq 
 |-  ( ( ( sqrt ` ( C + B ) ) e. CC /\ ( sqrt ` ( C - B ) ) e. CC ) -> ( ( ( sqrt ` ( C + B ) ) ^ 2 ) - ( ( sqrt ` ( C - B ) ) ^ 2 ) ) = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) )
70 67 68 69 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( sqrt ` ( C + B ) ) ^ 2 ) - ( ( sqrt ` ( C - B ) ) ^ 2 ) ) = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) )
71 70 oveq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( ( sqrt ` ( C + B ) ) ^ 2 ) - ( ( sqrt ` ( C - B ) ) ^ 2 ) ) / 2 ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / 2 ) )
72 pnncan 
 |-  ( ( C e. CC /\ B e. CC /\ B e. CC ) -> ( ( C + B ) - ( C - B ) ) = ( B + B ) )
73 72 3anidm23 
 |-  ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) - ( C - B ) ) = ( B + B ) )
74 2times 
 |-  ( B e. CC -> ( 2 x. B ) = ( B + B ) )
75 74 adantl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( 2 x. B ) = ( B + B ) )
76 73 75 eqtr4d 
 |-  ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) - ( C - B ) ) = ( 2 x. B ) )
77 4 5 76 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( ( C + B ) - ( C - B ) ) = ( 2 x. B ) )
78 77 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C + B ) - ( C - B ) ) = ( 2 x. B ) )
79 78 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( C + B ) - ( C - B ) ) = ( 2 x. B ) )
80 79 oveq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( C + B ) - ( C - B ) ) / 2 ) = ( ( 2 x. B ) / 2 ) )
81 2cn 
 |-  2 e. CC
82 2ne0 
 |-  2 =/= 0
83 divcan3 
 |-  ( ( B e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. B ) / 2 ) = B )
84 81 82 83 mp3an23 
 |-  ( B e. CC -> ( ( 2 x. B ) / 2 ) = B )
85 65 5 84 3syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( 2 x. B ) / 2 ) = B )
86 80 85 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( C + B ) - ( C - B ) ) / 2 ) = B )
87 64 71 86 3eqtr3d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / 2 ) = B )
88 87 oveq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) x. ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ) / 2 ) / 2 ) = ( B / 2 ) )
89 30 88 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) = ( B / 2 ) )
90 3 89 syl5eq 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( M x. N ) = ( B / 2 ) )
91 90 oveq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 2 x. ( M x. N ) ) = ( 2 x. ( B / 2 ) ) )
92 divcan2 
 |-  ( ( B e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( B / 2 ) ) = B )
93 81 82 92 mp3an23 
 |-  ( B e. CC -> ( 2 x. ( B / 2 ) ) = B )
94 5 93 syl 
 |-  ( B e. NN -> ( 2 x. ( B / 2 ) ) = B )
95 94 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( 2 x. ( B / 2 ) ) = B )
96 95 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 2 x. ( B / 2 ) ) = B )
97 91 96 eqtr2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B = ( 2 x. ( M x. N ) ) )