Metamath Proof Explorer

Theorem 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 ⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) )
Assertion fvprmselgcd1 ( ( 𝑋 ∈ ( 1 ... 𝑁 ) ∧ 𝑌 ∈ ( 1 ... 𝑁 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐹 ‘ 𝑋 ) gcd ( 𝐹 ‘ 𝑌 ) ) = 1 )

Proof

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