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	$⊢ φ \to M \in ℕ$
	flt4lem5elem.r	$⊢ φ \to R \in ℕ$
	flt4lem5elem.s	$⊢ φ \to S \in ℕ$
	flt4lem5elem.1	$⊢ φ \to M = R^{2} + S^{2}$
	flt4lem5elem.2	$⊢ φ \to R \gcd S = 1$
Assertion	flt4lem5elem	$⊢ φ \to (R \gcd M = 1 \land S \gcd M = 1)$

Proof

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

Metamath Proof Explorer

Theorem flt4lem5elem

Proof