Metamath Proof Explorer

Theorem pythagtriplem7

Description: Lemma for pythagtrip . Calculate ( sqrt( C + B ) ) . (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. NN )
2 1 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
3 simp2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. NN )
4 3 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. ZZ )
5 2 4 zsubcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. ZZ )
6 5 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 )
7 1 3 nnaddcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. NN )
8 7 nnnn0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. NN0 )
9 8 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. NN0 )
10 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
11 10 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. NN0 )
12 11 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A e. NN0 )
13 6 9 12 3jca 
 |-  ( ( ( 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 /\ ( C + B ) e. NN0 /\ A e. NN0 ) )
14 pythagtriplem4 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( C - B ) gcd ( C + B ) ) = 1 )
15 14 oveq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( C - B ) gcd ( C + B ) ) gcd A ) = ( 1 gcd A ) )
16 nnz 
 |-  ( A e. NN -> A e. ZZ )
17 16 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
18 17 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 )
19 1gcd 
 |-  ( A e. ZZ -> ( 1 gcd A ) = 1 )
20 18 19 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 1 gcd A ) = 1 )
21 15 20 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( C - B ) gcd ( C + B ) ) gcd A ) = 1 )
22 13 21 jca 
 |-  ( ( ( 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 /\ ( C + B ) e. NN0 /\ A e. NN0 ) /\ ( ( ( C - B ) gcd ( C + B ) ) gcd A ) = 1 ) )
23 oveq1 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( B ^ 2 ) ) = ( ( C ^ 2 ) - ( B ^ 2 ) ) )
24 23 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 ) ) )
25 nncn 
 |-  ( A e. NN -> A e. CC )
26 25 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. CC )
27 26 sqcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. CC )
28 3 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. CC )
29 28 sqcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. CC )
30 27 29 pncand 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( B ^ 2 ) ) = ( A ^ 2 ) )
31 30 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 ) )
32 1 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. CC )
33 subsq 
 |-  ( ( C e. CC /\ B e. CC ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C + B ) x. ( C - B ) ) )
34 32 28 33 syl2anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C + B ) x. ( C - B ) ) )
35 7 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. CC )
36 5 zcnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. CC )
37 35 36 mulcomd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C + B ) x. ( C - B ) ) = ( ( C - B ) x. ( C + B ) ) )
38 34 37 eqtrd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C - B ) x. ( C + B ) ) )
39 38 3ad2ant1 
 |-  ( ( ( 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 ) ) )
40 24 31 39 3eqtr3d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( A ^ 2 ) = ( ( C - B ) x. ( C + B ) ) )
41 coprimeprodsq2 
 |-  ( ( ( ( C - B ) e. ZZ /\ ( C + B ) e. NN0 /\ A e. NN0 ) /\ ( ( ( C - B ) gcd ( C + B ) ) gcd A ) = 1 ) -> ( ( A ^ 2 ) = ( ( C - B ) x. ( C + B ) ) -> ( C + B ) = ( ( ( C + B ) gcd A ) ^ 2 ) ) )
42 22 40 41 sylc 
 |-  ( ( ( 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 ) gcd A ) ^ 2 ) )
43 42 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 ) ) = ( sqrt ` ( ( ( C + B ) gcd A ) ^ 2 ) ) )
44 7 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. ZZ )
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. ZZ )
46 45 18 gcdcld 
 |-  ( ( ( 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. NN0 )
47 46 nn0red 
 |-  ( ( ( 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. RR )
48 46 nn0ge0d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 <_ ( ( C + B ) gcd A ) )
49 47 48 sqrtsqd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( sqrt ` ( ( ( C + B ) gcd A ) ^ 2 ) ) = ( ( C + B ) gcd A ) )
50 43 49 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 ) ) = ( ( C + B ) gcd A ) )