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 )

Metamath Proof Explorer

Theorem flt4lem5

Proof