Metamath Proof Explorer

Theorem pythagtriplem11

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

Proof

Step Hyp Ref Expression
1 pythagtriplem11.1 
 |-  M = ( ( ( 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 nnz 
 |-  ( C e. NN -> C e. ZZ )
7 6 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
8 nnz 
 |-  ( B e. NN -> B e. ZZ )
9 8 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. ZZ )
10 7 9 zaddcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. ZZ )
11 10 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 )
12 nnz 
 |-  ( A e. NN -> A e. ZZ )
13 12 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
14 13 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 )
15 dvdsgcdb 
 |-  ( ( 2 e. ZZ /\ ( C + B ) e. ZZ /\ A e. ZZ ) -> ( ( 2 || ( C + B ) /\ 2 || A ) <-> 2 || ( ( C + B ) gcd A ) ) )
16 5 11 14 15 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 ) ) )
17 16 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 ) )
18 17 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 )
19 4 18 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 ) )
20 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 ) )
21 20 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 ) ) )
22 19 21 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 ) ) )
23 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 )
24 23 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 )
25 7 9 zsubcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. ZZ )
26 25 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 )
27 dvdsgcdb 
 |-  ( ( 2 e. ZZ /\ ( C - B ) e. ZZ /\ A e. ZZ ) -> ( ( 2 || ( C - B ) /\ 2 || A ) <-> 2 || ( ( C - B ) gcd A ) ) )
28 5 26 14 27 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 ) ) )
29 28 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 ) )
30 29 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 )
31 4 30 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 ) )
32 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 ) )
33 32 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 ) ) )
34 31 33 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 ) ) )
35 opoe 
 |-  ( ( ( ( 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 ) ) ) )
36 3 22 24 34 35 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 ) ) ) )
37 2 23 nnaddcld 
 |-  ( ( ( 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 )
38 37 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 )
39 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 ) )
40 38 39 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 ) )
41 36 40 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 )
42 2 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 ) ) e. RR )
43 23 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 ) ) e. RR )
44 2 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 ) ) )
45 23 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 ) ) )
46 42 43 44 45 addgt0d 
 |-  ( ( ( 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 ) ) ) )
47 37 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 )
48 halfpos2 
 |-  ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) e. RR -> ( 0 < ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) <-> 0 < ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ) )
49 47 48 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 ) ) )
50 46 49 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 ) )
51 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 ) ) )
52 41 50 51 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 )
53 1 52 eqeltrid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> M e. NN )