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

Proof

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