fvprmselgcd1

Description: The greatest common divisor of two values of the prime selection function for different arguments is 1. (Contributed by AV, 19-Aug-2020)

		Ref	Expression
	Hypothesis	fvprmselelfz.f	$⊢ F = (m \in ℕ ⟼ if (m \in ℙ, m, 1))$
	Assertion	fvprmselgcd1	$⊢ (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to F (X) \gcd F (Y) = 1$

Proof

Step	Hyp	Ref	Expression
1		fvprmselelfz.f	$⊢ F = (m \in ℕ ⟼ if (m \in ℙ, m, 1))$
2		eleq1	$⊢ m = X \to (m \in ℙ \leftrightarrow X \in ℙ)$
3		id	$⊢ m = X \to m = X$
4	2 3	ifbieq1d	$⊢ m = X \to if (m \in ℙ, m, 1) = if (X \in ℙ, X, 1)$
5		iftrue	$⊢ X \in ℙ \to if (X \in ℙ, X, 1) = X$
6	5	ad2antrr	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to if (X \in ℙ, X, 1) = X$
7	4 6	sylan9eqr	$⊢ (((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \land m = X) \to if (m \in ℙ, m, 1) = X$
8		elfznn	$⊢ X \in (1 \dots N) \to X \in ℕ$
9	8	3ad2ant1	$⊢ (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to X \in ℕ$
10	9	adantl	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to X \in ℕ$
11	1 7 10 10	fvmptd2	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) = X$
12		eleq1	$⊢ m = Y \to (m \in ℙ \leftrightarrow Y \in ℙ)$
13		id	$⊢ m = Y \to m = Y$
14	12 13	ifbieq1d	$⊢ m = Y \to if (m \in ℙ, m, 1) = if (Y \in ℙ, Y, 1)$
15		iftrue	$⊢ Y \in ℙ \to if (Y \in ℙ, Y, 1) = Y$
16	15	ad2antlr	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to if (Y \in ℙ, Y, 1) = Y$
17	14 16	sylan9eqr	$⊢ (((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \land m = Y) \to if (m \in ℙ, m, 1) = Y$
18		elfznn	$⊢ Y \in (1 \dots N) \to Y \in ℕ$
19	18	3ad2ant2	$⊢ (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to Y \in ℕ$
20	19	adantl	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to Y \in ℕ$
21	1 17 20 20	fvmptd2	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (Y) = Y$
22	11 21	oveq12d	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) \gcd F (Y) = X \gcd Y$
23		prmrp	$⊢ (X \in ℙ \land Y \in ℙ) \to (X \gcd Y = 1 \leftrightarrow X \neq Y)$
24	23	biimprcd	$⊢ X \neq Y \to ((X \in ℙ \land Y \in ℙ) \to X \gcd Y = 1)$
25	24	3ad2ant3	$⊢ (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to ((X \in ℙ \land Y \in ℙ) \to X \gcd Y = 1)$
26	25	impcom	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to X \gcd Y = 1$
27	22 26	eqtrd	$⊢ ((X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) \gcd F (Y) = 1$
28	27	ex	$⊢ (X \in ℙ \land Y \in ℙ) \to ((X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to F (X) \gcd F (Y) = 1)$
29	5	ad2antrr	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to if (X \in ℙ, X, 1) = X$
30	4 29	sylan9eqr	$⊢ (((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \land m = X) \to if (m \in ℙ, m, 1) = X$
31	9	adantl	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to X \in ℕ$
32	1 30 31 31	fvmptd2	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) = X$
33		iffalse	$⊢ \neg Y \in ℙ \to if (Y \in ℙ, Y, 1) = 1$
34	33	ad2antlr	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to if (Y \in ℙ, Y, 1) = 1$
35	14 34	sylan9eqr	$⊢ (((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \land m = Y) \to if (m \in ℙ, m, 1) = 1$
36	19	adantl	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to Y \in ℕ$
37		1nn	$⊢ 1 \in ℕ$
38	37	a1i	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to 1 \in ℕ$
39	1 35 36 38	fvmptd2	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (Y) = 1$
40	32 39	oveq12d	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) \gcd F (Y) = X \gcd 1$
41		prmz	$⊢ X \in ℙ \to X \in ℤ$
42		gcd1	$⊢ X \in ℤ \to X \gcd 1 = 1$
43	41 42	syl	$⊢ X \in ℙ \to X \gcd 1 = 1$
44	43	ad2antrr	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to X \gcd 1 = 1$
45	40 44	eqtrd	$⊢ ((X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) \gcd F (Y) = 1$
46	45	ex	$⊢ (X \in ℙ \land \neg Y \in ℙ) \to ((X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to F (X) \gcd F (Y) = 1)$
47		iffalse	$⊢ \neg X \in ℙ \to if (X \in ℙ, X, 1) = 1$
48	47	ad2antrr	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to if (X \in ℙ, X, 1) = 1$
49	4 48	sylan9eqr	$⊢ (((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \land m = X) \to if (m \in ℙ, m, 1) = 1$
50	9	adantl	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to X \in ℕ$
51	37	a1i	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to 1 \in ℕ$
52	1 49 50 51	fvmptd2	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) = 1$
53	15	ad2antlr	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to if (Y \in ℙ, Y, 1) = Y$
54	14 53	sylan9eqr	$⊢ (((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \land m = Y) \to if (m \in ℙ, m, 1) = Y$
55	19	adantl	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to Y \in ℕ$
56	1 54 55 55	fvmptd2	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (Y) = Y$
57	52 56	oveq12d	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) \gcd F (Y) = 1 \gcd Y$
58		prmz	$⊢ Y \in ℙ \to Y \in ℤ$
59		1gcd	$⊢ Y \in ℤ \to 1 \gcd Y = 1$
60	58 59	syl	$⊢ Y \in ℙ \to 1 \gcd Y = 1$
61	60	ad2antlr	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to 1 \gcd Y = 1$
62	57 61	eqtrd	$⊢ ((\neg X \in ℙ \land Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) \gcd F (Y) = 1$
63	62	ex	$⊢ (\neg X \in ℙ \land Y \in ℙ) \to ((X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to F (X) \gcd F (Y) = 1)$
64	47	ad2antrr	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to if (X \in ℙ, X, 1) = 1$
65	4 64	sylan9eqr	$⊢ (((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \land m = X) \to if (m \in ℙ, m, 1) = 1$
66	9	adantl	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to X \in ℕ$
67	37	a1i	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to 1 \in ℕ$
68	1 65 66 67	fvmptd2	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) = 1$
69	33	ad2antlr	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to if (Y \in ℙ, Y, 1) = 1$
70	14 69	sylan9eqr	$⊢ (((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \land m = Y) \to if (m \in ℙ, m, 1) = 1$
71	19	adantl	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to Y \in ℕ$
72	1 70 71 67	fvmptd2	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (Y) = 1$
73	68 72	oveq12d	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) \gcd F (Y) = 1 \gcd 1$
74		1z	$⊢ 1 \in ℤ$
75		1gcd	$⊢ 1 \in ℤ \to 1 \gcd 1 = 1$
76	74 75	mp1i	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to 1 \gcd 1 = 1$
77	73 76	eqtrd	$⊢ ((\neg X \in ℙ \land \neg Y \in ℙ) \land (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y)) \to F (X) \gcd F (Y) = 1$
78	77	ex	$⊢ (\neg X \in ℙ \land \neg Y \in ℙ) \to ((X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to F (X) \gcd F (Y) = 1)$
79	28 46 63 78	4cases	$⊢ (X \in (1 \dots N) \land Y \in (1 \dots N) \land X \neq Y) \to F (X) \gcd F (Y) = 1$

Metamath Proof Explorer

Theorem fvprmselgcd1

Proof