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

Metamath Proof Explorer

Theorem pythagtriplem9

Description: Lemma for pythagtrip . Show that ( sqrt( C + B ) ) is a positive integer. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion 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 )

Proof

Step Hyp Ref Expression
1 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 ) )
2 nnz 
 |-  ( C e. NN -> C e. ZZ )
3 nnz 
 |-  ( B e. NN -> B e. ZZ )
4 zaddcl 
 |-  ( ( C e. ZZ /\ B e. ZZ ) -> ( C + B ) e. ZZ )
5 2 3 4 syl2anr 
 |-  ( ( B e. NN /\ C e. NN ) -> ( C + B ) e. ZZ )
6 5 3adant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. ZZ )
7 6 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 )
8 nnz 
 |-  ( A e. NN -> A e. ZZ )
9 8 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A 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 ) ) -> A e. ZZ )
11 nnne0 
 |-  ( A e. NN -> A =/= 0 )
12 11 neneqd 
 |-  ( A e. NN -> -. A = 0 )
13 12 intnand 
 |-  ( A e. NN -> -. ( ( C + B ) = 0 /\ A = 0 ) )
14 13 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> -. ( ( C + B ) = 0 /\ A = 0 ) )
15 14 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> -. ( ( C + B ) = 0 /\ A = 0 ) )
16 gcdn0cl 
 |-  ( ( ( ( C + B ) e. ZZ /\ A e. ZZ ) /\ -. ( ( C + B ) = 0 /\ A = 0 ) ) -> ( ( C + B ) gcd A ) e. NN )
17 7 10 15 16 syl21anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( C + B ) gcd A ) e. NN )
18 1 17 eqeltrd 
 |-  ( ( ( 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 )