Theorem flt4lem5elem

Description: Version of fltaccoprm and fltbccoprm where M is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd , dvds2addd , and prmdvdsexp , we can show that if two variables are coprime, the third is also coprime to the two. (Contributed by SN, 24-Aug-2024)

	Ref	Expression
Hypotheses	flt4lem5elem.m	|- ( ph -> M e. NN )
	flt4lem5elem.r	|- ( ph -> R e. NN )
	flt4lem5elem.s	|- ( ph -> S e. NN )
	flt4lem5elem.1	|- ( ph -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
	flt4lem5elem.2	|- ( ph -> ( R gcd S ) = 1 )
Assertion	flt4lem5elem	|- ( ph -> ( ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		flt4lem5elem.m	|- ( ph -> M e. NN )
2		flt4lem5elem.r	|- ( ph -> R e. NN )
3		flt4lem5elem.s	|- ( ph -> S e. NN )
4		flt4lem5elem.1	|- ( ph -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
5		flt4lem5elem.2	|- ( ph -> ( R gcd S ) = 1 )
6	2 3	prmdvdsncoprmbd	|- ( ph -> ( E. p e. Prime ( p || R /\ p || S ) <-> ( R gcd S ) =/= 1 ) )
7	6	necon2bbid	|- ( ph -> ( ( R gcd S ) = 1 <-> -. E. p e. Prime ( p || R /\ p || S ) ) )
8	5 7	mpbid	|- ( ph -> -. E. p e. Prime ( p || R /\ p || S ) )
9		simprl	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || R )
10		simplr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p e. Prime )
11		prmz	|- ( p e. Prime -> p e. ZZ )
12	10 11	syl	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p e. ZZ )
13	1	nnzd	|- ( ph -> M e. ZZ )
14	13	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> M e. ZZ )
15	2	nnsqcld	|- ( ph -> ( R ^ 2 ) e. NN )
16	15	nnzd	|- ( ph -> ( R ^ 2 ) e. ZZ )
17	16	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( R ^ 2 ) e. ZZ )
18		simprr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || M )
19	2	nnzd	|- ( ph -> R e. ZZ )
20	19	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> R e. ZZ )
21		prmdvdssq	|- ( ( p e. Prime /\ R e. ZZ ) -> ( p || R <-> p || ( R ^ 2 ) ) )
22	10 20 21	syl2anc	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( p || R <-> p || ( R ^ 2 ) ) )
23	9 22	mpbid	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || ( R ^ 2 ) )
24	12 14 17 18 23	dvds2subd	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || ( M - ( R ^ 2 ) ) )
25	15	nncnd	|- ( ph -> ( R ^ 2 ) e. CC )
26	25	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( R ^ 2 ) e. CC )
27	3	nnsqcld	|- ( ph -> ( S ^ 2 ) e. NN )
28	27	nncnd	|- ( ph -> ( S ^ 2 ) e. CC )
29	28	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( S ^ 2 ) e. CC )
30	4	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
31	26 29 30	mvrladdd	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( M - ( R ^ 2 ) ) = ( S ^ 2 ) )
32	24 31	breqtrd	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || ( S ^ 2 ) )
33	3	nnzd	|- ( ph -> S e. ZZ )
34	33	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> S e. ZZ )
35		prmdvdssq	|- ( ( p e. Prime /\ S e. ZZ ) -> ( p || S <-> p || ( S ^ 2 ) ) )
36	10 34 35	syl2anc	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( p || S <-> p || ( S ^ 2 ) ) )
37	32 36	mpbird	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || S )
38	9 37	jca	|- ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( p || R /\ p || S ) )
39	38	ex	|- ( ( ph /\ p e. Prime ) -> ( ( p || R /\ p || M ) -> ( p || R /\ p || S ) ) )
40	39	reximdva	|- ( ph -> ( E. p e. Prime ( p || R /\ p || M ) -> E. p e. Prime ( p || R /\ p || S ) ) )
41	8 40	mtod	|- ( ph -> -. E. p e. Prime ( p || R /\ p || M ) )
42	2 1	prmdvdsncoprmbd	|- ( ph -> ( E. p e. Prime ( p || R /\ p || M ) <-> ( R gcd M ) =/= 1 ) )
43	42	necon2bbid	|- ( ph -> ( ( R gcd M ) = 1 <-> -. E. p e. Prime ( p || R /\ p || M ) ) )
44	41 43	mpbird	|- ( ph -> ( R gcd M ) = 1 )
45		simplr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p e. Prime )
46	45 11	syl	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p e. ZZ )
47	13	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> M e. ZZ )
48	27	nnzd	|- ( ph -> ( S ^ 2 ) e. ZZ )
49	48	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( S ^ 2 ) e. ZZ )
50		simprr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || M )
51		simprl	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || S )
52	33	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> S e. ZZ )
53	45 52 35	syl2anc	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( p || S <-> p || ( S ^ 2 ) ) )
54	51 53	mpbid	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || ( S ^ 2 ) )
55	46 47 49 50 54	dvds2subd	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || ( M - ( S ^ 2 ) ) )
56	25	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( R ^ 2 ) e. CC )
57	28	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( S ^ 2 ) e. CC )
58	4	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
59	56 57 58	mvrraddd	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( M - ( S ^ 2 ) ) = ( R ^ 2 ) )
60	55 59	breqtrd	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || ( R ^ 2 ) )
61	19	ad2antrr	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> R e. ZZ )
62	45 61 21	syl2anc	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( p || R <-> p || ( R ^ 2 ) ) )
63	60 62	mpbird	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || R )
64	63 51	jca	|- ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( p || R /\ p || S ) )
65	64	ex	|- ( ( ph /\ p e. Prime ) -> ( ( p || S /\ p || M ) -> ( p || R /\ p || S ) ) )
66	65	reximdva	|- ( ph -> ( E. p e. Prime ( p || S /\ p || M ) -> E. p e. Prime ( p || R /\ p || S ) ) )
67	8 66	mtod	|- ( ph -> -. E. p e. Prime ( p || S /\ p || M ) )
68	3 1	prmdvdsncoprmbd	|- ( ph -> ( E. p e. Prime ( p || S /\ p || M ) <-> ( S gcd M ) =/= 1 ) )
69	68	necon2bbid	|- ( ph -> ( ( S gcd M ) = 1 <-> -. E. p e. Prime ( p || S /\ p || M ) ) )
70	67 69	mpbird	|- ( ph -> ( S gcd M ) = 1 )
71	44 70	jca	|- ( ph -> ( ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) )