Metamath Proof Explorer

Theorem flt4lem5

Description: In the context of the lemmas of pythagtrip , M and N are coprime. (Contributed by SN, 23-Aug-2024)

Ref Expression
Hypotheses flt4lem5.1 
|- M = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 )
flt4lem5.2 
|- N = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
Assertion flt4lem5 
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( M gcd N ) = 1 )

Proof

Step Hyp Ref Expression
1 flt4lem5.1 
 |-  M = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 )
2 flt4lem5.2 
 |-  N = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
3 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 )
4 simp11 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A e. NN )
5 simp12 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B e. NN )
6 coprmgcdb 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )
7 4 5 6 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )
8 3 7 mpbird 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) )
9 simplr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i e. NN )
10 9 nnzd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i e. ZZ )
11 1 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 )
12 11 ad2antrr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> M e. NN )
13 12 nnsqcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( M ^ 2 ) e. NN )
14 13 nnzd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( M ^ 2 ) e. ZZ )
15 2 pythagtriplem13 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> N e. NN )
16 15 ad2antrr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> N e. NN )
17 16 nnsqcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( N ^ 2 ) e. NN )
18 17 nnzd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( N ^ 2 ) e. ZZ )
19 simprl 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || M )
20 12 nnzd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> M e. ZZ )
21 2nn 
 |-  2 e. NN
22 21 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> 2 e. NN )
23 dvdsexp2im 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ 2 e. NN ) -> ( i || M -> i || ( M ^ 2 ) ) )
24 10 20 22 23 syl3anc 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( i || M -> i || ( M ^ 2 ) ) )
25 19 24 mpd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || ( M ^ 2 ) )
26 simprr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || N )
27 16 nnzd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> N e. ZZ )
28 dvdsexp2im 
 |-  ( ( i e. ZZ /\ N e. ZZ /\ 2 e. NN ) -> ( i || N -> i || ( N ^ 2 ) ) )
29 10 27 22 28 syl3anc 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( i || N -> i || ( N ^ 2 ) ) )
30 26 29 mpd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || ( N ^ 2 ) )
31 10 14 18 25 30 dvds2subd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || ( ( M ^ 2 ) - ( N ^ 2 ) ) )
32 1 2 pythagtriplem15 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A = ( ( M ^ 2 ) - ( N ^ 2 ) ) )
33 32 ad2antrr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> A = ( ( M ^ 2 ) - ( N ^ 2 ) ) )
34 31 33 breqtrrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || A )
35 2z 
 |-  2 e. ZZ
36 35 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> 2 e. ZZ )
37 12 16 nnmulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( M x. N ) 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 ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( M x. N ) e. ZZ )
39 10 20 27 26 dvdsmultr2d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || ( M x. N ) )
40 10 36 38 39 dvdsmultr2d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || ( 2 x. ( M x. N ) ) )
41 1 2 pythagtriplem16 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B = ( 2 x. ( M x. N ) ) )
42 41 ad2antrr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> B = ( 2 x. ( M x. N ) ) )
43 40 42 breqtrrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> i || B )
44 34 43 jca 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) /\ ( i || M /\ i || N ) ) -> ( i || A /\ i || B ) )
45 44 ex 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) -> ( ( i || M /\ i || N ) -> ( i || A /\ i || B ) ) )
46 45 imim1d 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) /\ i e. NN ) -> ( ( ( i || A /\ i || B ) -> i = 1 ) -> ( ( i || M /\ i || N ) -> i = 1 ) ) )
47 46 ralimdva 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) -> A. i e. NN ( ( i || M /\ i || N ) -> i = 1 ) ) )
48 8 47 mpd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A. i e. NN ( ( i || M /\ i || N ) -> i = 1 ) )
49 coprmgcdb 
 |-  ( ( M e. NN /\ N e. NN ) -> ( A. i e. NN ( ( i || M /\ i || N ) -> i = 1 ) <-> ( M gcd N ) = 1 ) )
50 11 15 49 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( A. i e. NN ( ( i || M /\ i || N ) -> i = 1 ) <-> ( M gcd N ) = 1 ) )
51 48 50 mpbid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( M gcd N ) = 1 )