This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pythagtriplem13

Description: Lemma for pythagtrip . Show that N (which will eventually be closely related to the n in the final statement) is a natural. (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 pythagtriplem13 
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> N e. NN )

Proof

Step Hyp Ref Expression
1 pythagtriplem13.1 
 |-  N = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
2 pythagtriplem9 
 |-  ( ( ( 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. NN )
3 2 nnzd 
 |-  ( ( ( 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. ZZ )
4 simp3r 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> -. 2 || A )
5 2z 
 |-  2 e. ZZ
6 simp3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. NN )
7 simp2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. NN )
8 6 7 nnaddcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. NN )
9 8 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. ZZ )
10 9 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. ZZ )
11 nnz 
 |-  ( A e. NN -> A e. ZZ )
12 11 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
13 12 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A e. ZZ )
14 dvdsgcdb 
 |-  ( ( 2 e. ZZ /\ ( C + B ) e. ZZ /\ A e. ZZ ) -> ( ( 2 || ( C + B ) /\ 2 || A ) <-> 2 || ( ( C + B ) gcd A ) ) )
15 5 10 13 14 mp3an2i 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( 2 || ( C + B ) /\ 2 || A ) <-> 2 || ( ( C + B ) gcd A ) ) )
16 15 biimpar 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ 2 || ( ( C + B ) gcd A ) ) -> ( 2 || ( C + B ) /\ 2 || A ) )
17 16 simprd 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ 2 || ( ( C + B ) gcd A ) ) -> 2 || A )
18 4 17 mtand 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> -. 2 || ( ( C + B ) gcd A ) )
19 pythagtriplem7 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( sqrt ` ( C + B ) ) = ( ( C + B ) gcd A ) )
20 19 breq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 2 || ( sqrt ` ( C + B ) ) <-> 2 || ( ( C + B ) gcd A ) ) )
21 18 20 mtbird 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> -. 2 || ( sqrt ` ( C + B ) ) )
22 pythagtriplem8 
 |-  ( ( ( 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. NN )
23 22 nnzd 
 |-  ( ( ( 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. ZZ )
24 nnz 
 |-  ( C e. NN -> C e. ZZ )
25 24 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
26 nnz 
 |-  ( B e. NN -> B e. ZZ )
27 26 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. ZZ )
28 25 27 zsubcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. ZZ )
29 28 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. ZZ )
30 dvdsgcdb 
 |-  ( ( 2 e. ZZ /\ ( C - B ) e. ZZ /\ A e. ZZ ) -> ( ( 2 || ( C - B ) /\ 2 || A ) <-> 2 || ( ( C - B ) gcd A ) ) )
31 5 29 13 30 mp3an2i 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( 2 || ( C - B ) /\ 2 || A ) <-> 2 || ( ( C - B ) gcd A ) ) )
32 31 biimpar 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ 2 || ( ( C - B ) gcd A ) ) -> ( 2 || ( C - B ) /\ 2 || A ) )
33 32 simprd 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ 2 || ( ( C - B ) gcd A ) ) -> 2 || A )
34 4 33 mtand 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> -. 2 || ( ( C - B ) gcd A ) )
35 pythagtriplem6 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( sqrt ` ( C - B ) ) = ( ( C - B ) gcd A ) )
36 35 breq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 2 || ( sqrt ` ( C - B ) ) <-> 2 || ( ( C - B ) gcd A ) ) )
37 34 36 mtbird 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> -. 2 || ( sqrt ` ( C - B ) ) )
38 omoe 
 |-  ( ( ( ( sqrt ` ( C + B ) ) e. ZZ /\ -. 2 || ( sqrt ` ( C + B ) ) ) /\ ( ( sqrt ` ( C - B ) ) e. ZZ /\ -. 2 || ( sqrt ` ( C - B ) ) ) ) -> 2 || ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) )
39 3 21 23 37 38 syl22anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 2 || ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) )
40 28 zred 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. RR )
41 40 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 )
42 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 )
43 42 nnred 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C e. RR )
44 8 nnred 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. RR )
45 44 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 )
46 nnrp 
 |-  ( B e. NN -> B e. RR+ )
47 46 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. RR+ )
48 47 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B e. RR+ )
49 43 48 ltsubrpd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( C - B ) < C )
50 nngt0 
 |-  ( B e. NN -> 0 < B )
51 50 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < B )
52 51 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 < B )
53 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 )
54 53 nnred 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B e. RR )
55 54 43 ltaddposd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 0 < B <-> C < ( C + B ) ) )
56 52 55 mpbid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C < ( C + B ) )
57 41 43 45 49 56 lttrd 
 |-  ( ( ( 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 ) )
58 pythagtriplem10 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C - B ) )
59 58 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 ) )
60 0re 
 |-  0 e. RR
61 ltle 
 |-  ( ( 0 e. RR /\ ( C - B ) e. RR ) -> ( 0 < ( C - B ) -> 0 <_ ( C - B ) ) )
62 60 61 mpan 
 |-  ( ( C - B ) e. RR -> ( 0 < ( C - B ) -> 0 <_ ( C - B ) ) )
63 41 59 62 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 ) )
64 nngt0 
 |-  ( C e. NN -> 0 < C )
65 64 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < C )
66 65 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 < C )
67 43 54 66 52 addgt0d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 < ( C + B ) )
68 ltle 
 |-  ( ( 0 e. RR /\ ( C + B ) e. RR ) -> ( 0 < ( C + B ) -> 0 <_ ( C + B ) ) )
69 60 68 mpan 
 |-  ( ( C + B ) e. RR -> ( 0 < ( C + B ) -> 0 <_ ( C + B ) ) )
70 45 67 69 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 ) )
71 41 63 45 70 sqrtltd 
 |-  ( ( ( 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 ) <-> ( sqrt ` ( C - B ) ) < ( sqrt ` ( C + B ) ) ) )
72 57 71 mpbid 
 |-  ( ( ( 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 ) ) )
73 nnsub 
 |-  ( ( ( sqrt ` ( C - B ) ) e. NN /\ ( sqrt ` ( C + B ) ) e. NN ) -> ( ( sqrt ` ( C - B ) ) < ( sqrt ` ( C + B ) ) <-> ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. NN ) )
74 22 2 73 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 ) ) <-> ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. NN ) )
75 72 74 mpbid 
 |-  ( ( ( 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. NN )
76 75 nnzd 
 |-  ( ( ( 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. ZZ )
77 evend2 
 |-  ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. ZZ -> ( 2 || ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) <-> ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) e. ZZ ) )
78 76 77 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 2 || ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) <-> ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) e. ZZ ) )
79 39 78 mpbid 
 |-  ( ( ( 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. ZZ )
80 75 nngt0d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 < ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) )
81 75 nnred 
 |-  ( ( ( 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. RR )
82 halfpos2 
 |-  ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) e. RR -> ( 0 < ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) <-> 0 < ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) )
83 81 82 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 0 < ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) <-> 0 < ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) )
84 80 83 mpbid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 < ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) )
85 elnnz 
 |-  ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) e. NN <-> ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) e. ZZ /\ 0 < ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) )
86 79 84 85 sylanbrc 
 |-  ( ( ( 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. NN )
87 1 86 eqeltrid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> N e. NN )