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

Metamath Proof Explorer

Theorem pythagtriplem3

Description: Lemma for pythagtrip . Show that C and B are relatively prime under some conditions. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem3 
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( B gcd C ) = 1 )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) -> ( ( B ^ 2 ) gcd ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( B ^ 2 ) gcd ( C ^ 2 ) ) )
2 1 adantl 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( B ^ 2 ) gcd ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( B ^ 2 ) gcd ( C ^ 2 ) ) )
3 nnz 
 |-  ( B e. NN -> B e. ZZ )
4 zsqcl 
 |-  ( B e. ZZ -> ( B ^ 2 ) e. ZZ )
5 3 4 syl 
 |-  ( B e. NN -> ( B ^ 2 ) e. ZZ )
6 5 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. ZZ )
7 nnz 
 |-  ( A e. NN -> A e. ZZ )
8 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
9 7 8 syl 
 |-  ( A e. NN -> ( A ^ 2 ) e. ZZ )
10 9 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. ZZ )
11 gcdadd 
 |-  ( ( ( B ^ 2 ) e. ZZ /\ ( A ^ 2 ) e. ZZ ) -> ( ( B ^ 2 ) gcd ( A ^ 2 ) ) = ( ( B ^ 2 ) gcd ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
12 6 10 11 syl2anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( B ^ 2 ) gcd ( A ^ 2 ) ) = ( ( B ^ 2 ) gcd ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
13 6 10 gcdcomd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( B ^ 2 ) gcd ( A ^ 2 ) ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
14 12 13 eqtr3d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( B ^ 2 ) gcd ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
15 14 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( B ^ 2 ) gcd ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
16 2 15 eqtr3d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( B ^ 2 ) gcd ( C ^ 2 ) ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
17 simpl2 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> B e. NN )
18 simpl3 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> C e. NN )
19 sqgcd 
 |-  ( ( B e. NN /\ C e. NN ) -> ( ( B gcd C ) ^ 2 ) = ( ( B ^ 2 ) gcd ( C ^ 2 ) ) )
20 17 18 19 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( B gcd C ) ^ 2 ) = ( ( B ^ 2 ) gcd ( C ^ 2 ) ) )
21 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> A e. NN )
22 sqgcd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
23 21 17 22 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
24 16 20 23 3eqtr4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( B gcd C ) ^ 2 ) = ( ( A gcd B ) ^ 2 ) )
25 24 3adant3 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( B gcd C ) ^ 2 ) = ( ( A gcd B ) ^ 2 ) )
26 simp3l 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( A gcd B ) = 1 )
27 26 oveq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( A gcd B ) ^ 2 ) = ( 1 ^ 2 ) )
28 25 27 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( B gcd C ) ^ 2 ) = ( 1 ^ 2 ) )
29 3 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. ZZ )
30 nnz 
 |-  ( C e. NN -> C e. ZZ )
31 30 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
32 29 31 gcdcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B gcd C ) e. NN0 )
33 32 nn0red 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B gcd C ) e. RR )
34 33 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( B gcd C ) e. RR )
35 32 nn0ge0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 <_ ( B gcd C ) )
36 35 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> 0 <_ ( B gcd C ) )
37 1re 
 |-  1 e. RR
38 0le1 
 |-  0 <_ 1
39 sq11 
 |-  ( ( ( ( B gcd C ) e. RR /\ 0 <_ ( B gcd C ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( ( B gcd C ) ^ 2 ) = ( 1 ^ 2 ) <-> ( B gcd C ) = 1 ) )
40 37 38 39 mpanr12 
 |-  ( ( ( B gcd C ) e. RR /\ 0 <_ ( B gcd C ) ) -> ( ( ( B gcd C ) ^ 2 ) = ( 1 ^ 2 ) <-> ( B gcd C ) = 1 ) )
41 34 36 40 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( B gcd C ) ^ 2 ) = ( 1 ^ 2 ) <-> ( B gcd C ) = 1 ) )
42 28 41 mpbid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( B gcd C ) = 1 )