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	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	flt4lem5elem.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	flt4lem5elem.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
	flt4lem5elem.1	⊢ ( 𝜑 → 𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
	flt4lem5elem.2	⊢ ( 𝜑 → ( 𝑅 gcd 𝑆 ) = 1 )
Assertion	flt4lem5elem	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		flt4lem5elem.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		flt4lem5elem.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
3		flt4lem5elem.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
4		flt4lem5elem.1	⊢ ( 𝜑 → 𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
5		flt4lem5elem.2	⊢ ( 𝜑 → ( 𝑅 gcd 𝑆 ) = 1 )
6	2 3	prmdvdsncoprmbd	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) ↔ ( 𝑅 gcd 𝑆 ) ≠ 1 ) )
7	6	necon2bbid	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑆 ) = 1 ↔ ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) ) )
8	5 7	mpbid	⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) )
9		simprl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ 𝑅 )
10		simplr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∈ ℙ )
11		prmz	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
12	10 11	syl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∈ ℤ )
13	1	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
14	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑀 ∈ ℤ )
15	2	nnsqcld	⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) ∈ ℕ )
16	15	nnzd	⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) ∈ ℤ )
17	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑅 ↑ 2 ) ∈ ℤ )
18		simprr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ 𝑀 )
19	2	nnzd	⊢ ( 𝜑 → 𝑅 ∈ ℤ )
20	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑅 ∈ ℤ )
21		prmdvdssq	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑅 ∈ ℤ ) → ( 𝑝 ∥ 𝑅 ↔ 𝑝 ∥ ( 𝑅 ↑ 2 ) ) )
22	10 20 21	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑝 ∥ 𝑅 ↔ 𝑝 ∥ ( 𝑅 ↑ 2 ) ) )
23	9 22	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ ( 𝑅 ↑ 2 ) )
24	12 14 17 18 23	dvds2subd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ ( 𝑀 − ( 𝑅 ↑ 2 ) ) )
25	15	nncnd	⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) ∈ ℂ )
26	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
27	3	nnsqcld	⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℕ )
28	27	nncnd	⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℂ )
29	28	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑆 ↑ 2 ) ∈ ℂ )
30	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
31	26 29 30	mvrladdd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑀 − ( 𝑅 ↑ 2 ) ) = ( 𝑆 ↑ 2 ) )
32	24 31	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ ( 𝑆 ↑ 2 ) )
33	3	nnzd	⊢ ( 𝜑 → 𝑆 ∈ ℤ )
34	33	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑆 ∈ ℤ )
35		prmdvdssq	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑆 ∈ ℤ ) → ( 𝑝 ∥ 𝑆 ↔ 𝑝 ∥ ( 𝑆 ↑ 2 ) ) )
36	10 34 35	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑝 ∥ 𝑆 ↔ 𝑝 ∥ ( 𝑆 ↑ 2 ) ) )
37	32 36	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ 𝑆 )
38	9 37	jca	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) )
39	38	ex	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) → ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) ) )
40	39	reximdva	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) ) )
41	8 40	mtod	⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) )
42	2 1	prmdvdsncoprmbd	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ↔ ( 𝑅 gcd 𝑀 ) ≠ 1 ) )
43	42	necon2bbid	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑀 ) = 1 ↔ ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀 ) ) )
44	41 43	mpbird	⊢ ( 𝜑 → ( 𝑅 gcd 𝑀 ) = 1 )
45		simplr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∈ ℙ )
46	45 11	syl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∈ ℤ )
47	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑀 ∈ ℤ )
48	27	nnzd	⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℤ )
49	48	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑆 ↑ 2 ) ∈ ℤ )
50		simprr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ 𝑀 )
51		simprl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ 𝑆 )
52	33	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑆 ∈ ℤ )
53	45 52 35	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑝 ∥ 𝑆 ↔ 𝑝 ∥ ( 𝑆 ↑ 2 ) ) )
54	51 53	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ ( 𝑆 ↑ 2 ) )
55	46 47 49 50 54	dvds2subd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ ( 𝑀 − ( 𝑆 ↑ 2 ) ) )
56	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
57	28	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑆 ↑ 2 ) ∈ ℂ )
58	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
59	56 57 58	mvrraddd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑀 − ( 𝑆 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) )
60	55 59	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ ( 𝑅 ↑ 2 ) )
61	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑅 ∈ ℤ )
62	45 61 21	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑝 ∥ 𝑅 ↔ 𝑝 ∥ ( 𝑅 ↑ 2 ) ) )
63	60 62	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → 𝑝 ∥ 𝑅 )
64	63 51	jca	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) → ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) )
65	64	ex	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) → ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) ) )
66	65	reximdva	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆 ) ) )
67	8 66	mtod	⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) )
68	3 1	prmdvdsncoprmbd	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ↔ ( 𝑆 gcd 𝑀 ) ≠ 1 ) )
69	68	necon2bbid	⊢ ( 𝜑 → ( ( 𝑆 gcd 𝑀 ) = 1 ↔ ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀 ) ) )
70	67 69	mpbird	⊢ ( 𝜑 → ( 𝑆 gcd 𝑀 ) = 1 )
71	44 70	jca	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) )