Metamath Proof Explorer

Theorem pythagtriplem6

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 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 ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( C e. NN -> C e. ZZ )
2 1 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
3 nnz 
 |-  ( B e. NN -> B e. ZZ )
4 3 3ad2ant2 
 |-  ( ( 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 pythagtriplem10 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C - B ) )
8 7 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 ) )
9 elnnz 
 |-  ( ( C - B ) e. NN <-> ( ( C - B ) e. ZZ /\ 0 < ( C - B ) ) )
10 6 8 9 sylanbrc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( C - B ) e. NN )
11 10 nnnn0d 
 |-  ( ( ( 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 )
12 simp3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. NN )
13 simp2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. NN )
14 12 13 nnaddcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. NN )
15 14 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. ZZ )
16 15 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 )
17 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
18 17 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. NN0 )
19 18 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 )
20 11 16 19 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. NN0 /\ ( C + B ) e. ZZ /\ A e. NN0 ) )
21 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 )
22 21 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 ) )
23 nnz 
 |-  ( A e. NN -> A e. ZZ )
24 23 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
25 24 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 )
26 1gcd 
 |-  ( A e. ZZ -> ( 1 gcd A ) = 1 )
27 25 26 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 )
28 22 27 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 )
29 20 28 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. NN0 /\ ( C + B ) e. ZZ /\ A e. NN0 ) /\ ( ( ( C - B ) gcd ( C + B ) ) gcd A ) = 1 ) )
30 oveq1 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( B ^ 2 ) ) = ( ( C ^ 2 ) - ( B ^ 2 ) ) )
31 30 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 ) ) )
32 24 zcnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. CC )
33 32 sqcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. CC )
34 nncn 
 |-  ( B e. NN -> B e. CC )
35 34 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. CC )
36 35 sqcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. CC )
37 33 36 pncand 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( B ^ 2 ) ) = ( A ^ 2 ) )
38 37 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 ) )
39 nncn 
 |-  ( C e. NN -> C e. CC )
40 39 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. CC )
41 subsq 
 |-  ( ( C e. CC /\ B e. CC ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C + B ) x. ( C - B ) ) )
42 40 35 41 syl2anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C + B ) x. ( C - B ) ) )
43 14 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) e. CC )
44 5 zcnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. CC )
45 43 44 mulcomd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C + B ) x. ( C - B ) ) = ( ( C - B ) x. ( C + B ) ) )
46 42 45 eqtrd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C - B ) x. ( C + B ) ) )
47 46 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 ) ) )
48 31 38 47 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 ) ) )
49 coprimeprodsq 
 |-  ( ( ( ( C - B ) e. NN0 /\ ( C + B ) e. ZZ /\ 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 ) ) )
50 29 48 49 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 ) )
51 50 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 ) ) )
52 6 25 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 )
53 52 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 )
54 52 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 ) )
55 53 54 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 ) )
56 51 55 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 ) )