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

Proof

Step Hyp Ref Expression
1 pythagtriplem13.1 
 |-  N = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
2 1 oveq1i 
 |-  ( N ^ 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 sqrtcld 
 |-  ( ( B e. NN /\ C e. NN ) -> ( sqrt ` ( C + B ) ) e. CC )
8 subcl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C - B ) e. CC )
9 3 4 8 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( C - B ) e. CC )
10 9 sqrtcld 
 |-  ( ( B e. NN /\ C e. NN ) -> ( sqrt ` ( C - B ) ) e. CC )
11 7 10 subcld 
 |-  ( ( B e. NN /\ C e. NN ) -> ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. CC )
12 11 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. CC )
13 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 ) ) - ( sqrt ` ( C - B ) ) ) e. CC )
14 2cn 
 |-  2 e. CC
15 2ne0 
 |-  2 =/= 0
16 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 ) ) )
17 14 15 16 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 ) ) )
18 13 17 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 ^ 2 ) ) )
19 14 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 13 sqcld 
 |-  ( ( ( 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 ) e. CC )
22 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
23 divdiv1 
 |-  ( ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ^ 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ^ 2 ) / 2 ) / 2 ) = ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ^ 2 ) / ( 2 x. 2 ) ) )
24 22 22 23 mp3an23 
 |-  ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ^ 2 ) e. CC -> ( ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ^ 2 ) / 2 ) / 2 ) = ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ^ 2 ) / ( 2 x. 2 ) ) )
25 21 24 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 ) / 2 ) = ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) ^ 2 ) / ( 2 x. 2 ) ) )
26 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 )
27 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 )
28 26 27 7 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 )
29 26 27 10 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 )
30 binom2sub 
 |-  ( ( ( 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 ) ) )
31 28 29 30 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 ) ) )
32 nnre 
 |-  ( C e. NN -> C e. RR )
33 nnre 
 |-  ( B e. NN -> B e. RR )
34 readdcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + B ) e. RR )
35 32 33 34 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( C + B ) e. RR )
36 35 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. RR )
37 36 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 )
38 37 recnd 
 |-  ( ( ( 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 )
39 resubcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C - B ) e. RR )
40 32 33 39 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( C - B ) e. RR )
41 40 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. RR )
42 41 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 )
43 42 recnd 
 |-  ( ( ( 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 )
44 7 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( sqrt ` ( C + B ) ) e. CC )
45 10 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( sqrt ` ( C - B ) ) e. CC )
46 44 45 mulcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( sqrt ` ( C + B ) ) x. ( sqrt ` ( C - B ) ) ) e. CC )
47 mulcl 
 |-  ( ( 2 e. CC /\ ( ( sqrt ` ( C + B ) ) x. ( sqrt ` ( C - B ) ) ) e. CC ) -> ( 2 x. ( ( sqrt ` ( C + B ) ) x. ( sqrt ` ( C - B ) ) ) ) e. CC )
48 14 46 47 sylancr 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( 2 x. ( ( sqrt ` ( C + B ) ) x. ( sqrt ` ( C - B ) ) ) ) e. CC )
49 48 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 )
50 38 43 49 addsubd 
 |-  ( ( ( 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 ) ) ) ) ) = ( ( ( C + B ) - ( 2 x. ( ( sqrt ` ( C + B ) ) x. ( sqrt ` ( C - B ) ) ) ) ) + ( C - B ) ) )
51 27 nncnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C e. CC )
52 simp11 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A e. NN )
53 52 nncnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A e. CC )
54 subdi 
 |-  ( ( 2 e. CC /\ C e. CC /\ A e. CC ) -> ( 2 x. ( C - A ) ) = ( ( 2 x. C ) - ( 2 x. A ) ) )
55 14 51 53 54 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 ) ) )
56 ppncan 
 |-  ( ( C e. CC /\ B e. CC /\ C e. CC ) -> ( ( C + B ) + ( C - B ) ) = ( C + C ) )
57 56 3anidm13 
 |-  ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + ( C - B ) ) = ( C + C ) )
58 2times 
 |-  ( C e. CC -> ( 2 x. C ) = ( C + C ) )
59 58 adantr 
 |-  ( ( C e. CC /\ B e. CC ) -> ( 2 x. C ) = ( C + C ) )
60 57 59 eqtr4d 
 |-  ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + ( C - B ) ) = ( 2 x. C ) )
61 3 4 60 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( ( C + B ) + ( C - B ) ) = ( 2 x. C ) )
62 61 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C + B ) + ( C - B ) ) = ( 2 x. C ) )
63 62 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. C ) )
64 26 nncnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B e. CC )
65 subsq 
 |-  ( ( C e. CC /\ B e. CC ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C + B ) x. ( C - B ) ) )
66 51 64 65 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 ) ) )
67 oveq1 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( B ^ 2 ) ) = ( ( C ^ 2 ) - ( B ^ 2 ) ) )
68 67 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 ) ) )
69 nncn 
 |-  ( A e. NN -> A e. CC )
70 69 sqcld 
 |-  ( A e. NN -> ( A ^ 2 ) e. CC )
71 70 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. CC )
72 4 sqcld 
 |-  ( B e. NN -> ( B ^ 2 ) e. CC )
73 72 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. CC )
74 71 73 pncand 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( B ^ 2 ) ) = ( A ^ 2 ) )
75 74 3ad2ant1 
 |-  ( ( ( 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 ) )
76 68 75 eqtr3d 
 |-  ( ( ( 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 ) ) = ( A ^ 2 ) )
77 66 76 eqtr3d 
 |-  ( ( ( 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 ) )
78 77 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 ) ) )
79 32 adantl 
 |-  ( ( B e. NN /\ C e. NN ) -> C e. RR )
80 33 adantr 
 |-  ( ( B e. NN /\ C e. NN ) -> B e. RR )
81 nngt0 
 |-  ( C e. NN -> 0 < C )
82 81 adantl 
 |-  ( ( B e. NN /\ C e. NN ) -> 0 < C )
83 nngt0 
 |-  ( B e. NN -> 0 < B )
84 83 adantr 
 |-  ( ( B e. NN /\ C e. NN ) -> 0 < B )
85 79 80 82 84 addgt0d 
 |-  ( ( B e. NN /\ C e. NN ) -> 0 < ( C + B ) )
86 0re 
 |-  0 e. RR
87 ltle 
 |-  ( ( 0 e. RR /\ ( C + B ) e. RR ) -> ( 0 < ( C + B ) -> 0 <_ ( C + B ) ) )
88 86 87 mpan 
 |-  ( ( C + B ) e. RR -> ( 0 < ( C + B ) -> 0 <_ ( C + B ) ) )
89 35 85 88 sylc 
 |-  ( ( B e. NN /\ C e. NN ) -> 0 <_ ( C + B ) )
90 89 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 <_ ( C + B ) )
91 90 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 ) )
92 pythagtriplem10 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C - B ) )
93 92 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 ) )
94 ltle 
 |-  ( ( 0 e. RR /\ ( C - B ) e. RR ) -> ( 0 < ( C - B ) -> 0 <_ ( C - B ) ) )
95 86 94 mpan 
 |-  ( ( C - B ) e. RR -> ( 0 < ( C - B ) -> 0 <_ ( C - B ) ) )
96 42 93 95 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 ) )
97 37 91 42 96 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 ) ) ) )
98 78 97 eqtr3d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( sqrt ` ( A ^ 2 ) ) = ( ( sqrt ` ( C + B ) ) x. ( sqrt ` ( C - B ) ) ) )
99 nnre 
 |-  ( A e. NN -> A e. RR )
100 99 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. RR )
101 100 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 )
102 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
103 102 nn0ge0d 
 |-  ( A e. NN -> 0 <_ A )
104 103 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 <_ A )
105 104 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 <_ A )
106 101 105 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 )
107 98 106 eqtr3d 
 |-  ( ( ( 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 )
108 107 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 ) )
109 63 108 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 ) ) )
110 55 109 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 ) ) ) ) ) )
111 resqrtth 
 |-  ( ( ( C + B ) e. RR /\ 0 <_ ( C + B ) ) -> ( ( sqrt ` ( C + B ) ) ^ 2 ) = ( C + B ) )
112 37 91 111 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 ) )
113 112 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 ) ) ) ) ) )
114 resqrtth 
 |-  ( ( ( C - B ) e. RR /\ 0 <_ ( C - B ) ) -> ( ( sqrt ` ( C - B ) ) ^ 2 ) = ( C - B ) )
115 42 96 114 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 ) )
116 113 115 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 ) ) )
117 50 110 116 3eqtr4rd 
 |-  ( ( ( 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 ) ) = ( 2 x. ( C - A ) ) )
118 31 117 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 ) = ( 2 x. ( C - A ) ) )
119 118 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 ) = ( ( 2 x. ( C - A ) ) / 2 ) )
120 subcl 
 |-  ( ( C e. CC /\ A e. CC ) -> ( C - A ) e. CC )
121 3 69 120 syl2anr 
 |-  ( ( A e. NN /\ C e. NN ) -> ( C - A ) e. CC )
122 121 3adant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - A ) e. CC )
123 122 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 )
124 divcan3 
 |-  ( ( ( C - A ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. ( C - A ) ) / 2 ) = ( C - A ) )
125 14 15 124 mp3an23 
 |-  ( ( C - A ) e. CC -> ( ( 2 x. ( C - A ) ) / 2 ) = ( C - A ) )
126 123 125 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 ) )
127 119 126 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 ) / 2 ) = ( C - A ) )
128 127 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 ) / 2 ) = ( ( C - A ) / 2 ) )
129 25 128 eqtr3d 
 |-  ( ( ( 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 ) ) = ( ( C - A ) / 2 ) )
130 20 129 eqtrid 
 |-  ( ( ( 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 ^ 2 ) ) = ( ( C - A ) / 2 ) )
131 18 130 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 ) ^ 2 ) = ( ( C - A ) / 2 ) )
132 2 131 eqtrid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( N ^ 2 ) = ( ( C - A ) / 2 ) )