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 
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )
Assertion fvprmselgcd1 
|- ( ( X e. ( 1 ... N ) /\ Y e. ( 1 ... N ) /\ X =/= Y ) -> ( ( F ` X ) gcd ( F ` Y ) ) = 1 )

Proof

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