Metamath Proof Explorer

Theorem coprmprod

Description: The product of the elements of a sequence of pairwise coprime positive integers is coprime to a positive integer which is coprime to all integers of the sequence. (Contributed by AV, 18-Aug-2020)

Ref Expression
Assertion coprmprod 
|- ( ( ( M e. Fin /\ M C_ NN /\ N e. NN ) /\ F : NN --> NN /\ A. m e. M ( ( F ` m ) gcd N ) = 1 ) -> ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> ( prod_ m e. M ( F ` m ) gcd N ) = 1 ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( x = (/) -> ( x C_ NN <-> (/) C_ NN ) )
2 1 3anbi1d 
 |-  ( x = (/) -> ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) <-> ( (/) C_ NN /\ N e. NN /\ F : NN --> NN ) ) )
3 raleq 
 |-  ( x = (/) -> ( A. m e. x ( ( F ` m ) gcd N ) = 1 <-> A. m e. (/) ( ( F ` m ) gcd N ) = 1 ) )
4 difeq1 
 |-  ( x = (/) -> ( x \ { m } ) = ( (/) \ { m } ) )
5 4 raleqdv 
 |-  ( x = (/) -> ( A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
6 5 raleqbi1dv 
 |-  ( x = (/) -> ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
7 2 3 6 3anbi123d 
 |-  ( x = (/) -> ( ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. x ( ( F ` m ) gcd N ) = 1 /\ A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) <-> ( ( (/) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. (/) ( ( F ` m ) gcd N ) = 1 /\ A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) )
8 prodeq1 
 |-  ( x = (/) -> prod_ m e. x ( F ` m ) = prod_ m e. (/) ( F ` m ) )
9 8 oveq1d 
 |-  ( x = (/) -> ( prod_ m e. x ( F ` m ) gcd N ) = ( prod_ m e. (/) ( F ` m ) gcd N ) )
10 9 eqeq1d 
 |-  ( x = (/) -> ( ( prod_ m e. x ( F ` m ) gcd N ) = 1 <-> ( prod_ m e. (/) ( F ` m ) gcd N ) = 1 ) )
11 7 10 imbi12d 
 |-  ( x = (/) -> ( ( ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. x ( ( F ` m ) gcd N ) = 1 /\ A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. x ( F ` m ) gcd N ) = 1 ) <-> ( ( ( (/) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. (/) ( ( F ` m ) gcd N ) = 1 /\ A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. (/) ( F ` m ) gcd N ) = 1 ) ) )
12 sseq1 
 |-  ( x = y -> ( x C_ NN <-> y C_ NN ) )
13 12 3anbi1d 
 |-  ( x = y -> ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) <-> ( y C_ NN /\ N e. NN /\ F : NN --> NN ) ) )
14 raleq 
 |-  ( x = y -> ( A. m e. x ( ( F ` m ) gcd N ) = 1 <-> A. m e. y ( ( F ` m ) gcd N ) = 1 ) )
15 difeq1 
 |-  ( x = y -> ( x \ { m } ) = ( y \ { m } ) )
16 15 raleqdv 
 |-  ( x = y -> ( A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
17 16 raleqbi1dv 
 |-  ( x = y -> ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
18 13 14 17 3anbi123d 
 |-  ( x = y -> ( ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. x ( ( F ` m ) gcd N ) = 1 /\ A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) <-> ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) )
19 prodeq1 
 |-  ( x = y -> prod_ m e. x ( F ` m ) = prod_ m e. y ( F ` m ) )
20 19 oveq1d 
 |-  ( x = y -> ( prod_ m e. x ( F ` m ) gcd N ) = ( prod_ m e. y ( F ` m ) gcd N ) )
21 20 eqeq1d 
 |-  ( x = y -> ( ( prod_ m e. x ( F ` m ) gcd N ) = 1 <-> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) )
22 18 21 imbi12d 
 |-  ( x = y -> ( ( ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. x ( ( F ` m ) gcd N ) = 1 /\ A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. x ( F ` m ) gcd N ) = 1 ) <-> ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) )
23 sseq1 
 |-  ( x = ( y u. { z } ) -> ( x C_ NN <-> ( y u. { z } ) C_ NN ) )
24 23 3anbi1d 
 |-  ( x = ( y u. { z } ) -> ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) <-> ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) ) )
25 raleq 
 |-  ( x = ( y u. { z } ) -> ( A. m e. x ( ( F ` m ) gcd N ) = 1 <-> A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 ) )
26 difeq1 
 |-  ( x = ( y u. { z } ) -> ( x \ { m } ) = ( ( y u. { z } ) \ { m } ) )
27 26 raleqdv 
 |-  ( x = ( y u. { z } ) -> ( A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
28 27 raleqbi1dv 
 |-  ( x = ( y u. { z } ) -> ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
29 24 25 28 3anbi123d 
 |-  ( x = ( y u. { z } ) -> ( ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. x ( ( F ` m ) gcd N ) = 1 /\ A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) <-> ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) )
30 prodeq1 
 |-  ( x = ( y u. { z } ) -> prod_ m e. x ( F ` m ) = prod_ m e. ( y u. { z } ) ( F ` m ) )
31 30 oveq1d 
 |-  ( x = ( y u. { z } ) -> ( prod_ m e. x ( F ` m ) gcd N ) = ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) )
32 31 eqeq1d 
 |-  ( x = ( y u. { z } ) -> ( ( prod_ m e. x ( F ` m ) gcd N ) = 1 <-> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = 1 ) )
33 29 32 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. x ( ( F ` m ) gcd N ) = 1 /\ A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. x ( F ` m ) gcd N ) = 1 ) <-> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = 1 ) ) )
34 sseq1 
 |-  ( x = M -> ( x C_ NN <-> M C_ NN ) )
35 34 3anbi1d 
 |-  ( x = M -> ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) <-> ( M C_ NN /\ N e. NN /\ F : NN --> NN ) ) )
36 raleq 
 |-  ( x = M -> ( A. m e. x ( ( F ` m ) gcd N ) = 1 <-> A. m e. M ( ( F ` m ) gcd N ) = 1 ) )
37 difeq1 
 |-  ( x = M -> ( x \ { m } ) = ( M \ { m } ) )
38 37 raleqdv 
 |-  ( x = M -> ( A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
39 38 raleqbi1dv 
 |-  ( x = M -> ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
40 35 36 39 3anbi123d 
 |-  ( x = M -> ( ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. x ( ( F ` m ) gcd N ) = 1 /\ A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) <-> ( ( M C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. M ( ( F ` m ) gcd N ) = 1 /\ A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) )
41 prodeq1 
 |-  ( x = M -> prod_ m e. x ( F ` m ) = prod_ m e. M ( F ` m ) )
42 41 oveq1d 
 |-  ( x = M -> ( prod_ m e. x ( F ` m ) gcd N ) = ( prod_ m e. M ( F ` m ) gcd N ) )
43 42 eqeq1d 
 |-  ( x = M -> ( ( prod_ m e. x ( F ` m ) gcd N ) = 1 <-> ( prod_ m e. M ( F ` m ) gcd N ) = 1 ) )
44 40 43 imbi12d 
 |-  ( x = M -> ( ( ( ( x C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. x ( ( F ` m ) gcd N ) = 1 /\ A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. x ( F ` m ) gcd N ) = 1 ) <-> ( ( ( M C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. M ( ( F ` m ) gcd N ) = 1 /\ A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. M ( F ` m ) gcd N ) = 1 ) ) )
45 prod0 
 |-  prod_ m e. (/) ( F ` m ) = 1
46 45 a1i 
 |-  ( N e. NN -> prod_ m e. (/) ( F ` m ) = 1 )
47 46 oveq1d 
 |-  ( N e. NN -> ( prod_ m e. (/) ( F ` m ) gcd N ) = ( 1 gcd N ) )
48 nnz 
 |-  ( N e. NN -> N e. ZZ )
49 1gcd 
 |-  ( N e. ZZ -> ( 1 gcd N ) = 1 )
50 48 49 syl 
 |-  ( N e. NN -> ( 1 gcd N ) = 1 )
51 47 50 eqtrd 
 |-  ( N e. NN -> ( prod_ m e. (/) ( F ` m ) gcd N ) = 1 )
52 51 3ad2ant2 
 |-  ( ( (/) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( prod_ m e. (/) ( F ` m ) gcd N ) = 1 )
53 52 3ad2ant1 
 |-  ( ( ( (/) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. (/) ( ( F ` m ) gcd N ) = 1 /\ A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. (/) ( F ` m ) gcd N ) = 1 )
54 nfv 
 |-  F/ m ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) )
55 nfcv 
 |-  F/_ m ( F ` z )
56 simprl 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> y e. Fin )
57 unss 
 |-  ( ( y C_ NN /\ { z } C_ NN ) <-> ( y u. { z } ) C_ NN )
58 vex 
 |-  z e. _V
59 58 snss 
 |-  ( z e. NN <-> { z } C_ NN )
60 59 bilanri 
 |-  ( ( y C_ NN /\ { z } C_ NN ) -> z e. NN )
61 57 60 sylbir 
 |-  ( ( y u. { z } ) C_ NN -> z e. NN )
62 61 3ad2ant1 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> z e. NN )
63 62 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> z e. NN )
64 simprr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> -. z e. y )
65 simpll3 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> F : NN --> NN )
66 simpl 
 |-  ( ( y C_ NN /\ { z } C_ NN ) -> y C_ NN )
67 57 66 sylbir 
 |-  ( ( y u. { z } ) C_ NN -> y C_ NN )
68 67 3ad2ant1 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> y C_ NN )
69 68 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> y C_ NN )
70 69 sselda 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> m e. NN )
71 65 70 ffvelcdmd 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> ( F ` m ) e. NN )
72 71 nncnd 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> ( F ` m ) e. CC )
73 fveq2 
 |-  ( m = z -> ( F ` m ) = ( F ` z ) )
74 simpr 
 |-  ( ( ( y u. { z } ) C_ NN /\ F : NN --> NN ) -> F : NN --> NN )
75 61 adantr 
 |-  ( ( ( y u. { z } ) C_ NN /\ F : NN --> NN ) -> z e. NN )
76 74 75 ffvelcdmd 
 |-  ( ( ( y u. { z } ) C_ NN /\ F : NN --> NN ) -> ( F ` z ) e. NN )
77 76 3adant2 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( F ` z ) e. NN )
78 77 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( F ` z ) e. NN )
79 78 nncnd 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( F ` z ) e. CC )
80 54 55 56 63 64 72 73 79 fprodsplitsn 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> prod_ m e. ( y u. { z } ) ( F ` m ) = ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) )
81 80 oveq1d 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = ( ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) gcd N ) )
82 56 71 fprodnncl 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> prod_ m e. y ( F ` m ) e. NN )
83 82 nnzd 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> prod_ m e. y ( F ` m ) e. ZZ )
84 78 nnzd 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( F ` z ) e. ZZ )
85 83 84 zmulcld 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) e. ZZ )
86 48 3ad2ant2 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> N e. ZZ )
87 86 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> N e. ZZ )
88 85 87 gcdcomd 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) gcd N ) = ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) )
89 81 88 eqtrd 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) )
90 89 ex 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( ( y e. Fin /\ -. z e. y ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) ) )
91 90 3ad2ant1 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( ( y e. Fin /\ -. z e. y ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) ) )
92 91 com12 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) ) )
93 92 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) ) )
94 93 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) /\ ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) )
95 simpl2 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> N e. NN )
96 95 82 78 3jca 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( N e. NN /\ prod_ m e. y ( F ` m ) e. NN /\ ( F ` z ) e. NN ) )
97 96 ex 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( ( y e. Fin /\ -. z e. y ) -> ( N e. NN /\ prod_ m e. y ( F ` m ) e. NN /\ ( F ` z ) e. NN ) ) )
98 97 3ad2ant1 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( ( y e. Fin /\ -. z e. y ) -> ( N e. NN /\ prod_ m e. y ( F ` m ) e. NN /\ ( F ` z ) e. NN ) ) )
99 98 com12 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( N e. NN /\ prod_ m e. y ( F ` m ) e. NN /\ ( F ` z ) e. NN ) ) )
100 99 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( N e. NN /\ prod_ m e. y ( F ` m ) e. NN /\ ( F ` z ) e. NN ) ) )
101 100 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) /\ ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> ( N e. NN /\ prod_ m e. y ( F ` m ) e. NN /\ ( F ` z ) e. NN ) )
102 87 83 gcdcomd 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( N gcd prod_ m e. y ( F ` m ) ) = ( prod_ m e. y ( F ` m ) gcd N ) )
103 102 ex 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( ( y e. Fin /\ -. z e. y ) -> ( N gcd prod_ m e. y ( F ` m ) ) = ( prod_ m e. y ( F ` m ) gcd N ) ) )
104 103 3ad2ant1 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( ( y e. Fin /\ -. z e. y ) -> ( N gcd prod_ m e. y ( F ` m ) ) = ( prod_ m e. y ( F ` m ) gcd N ) ) )
105 104 com12 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( N gcd prod_ m e. y ( F ` m ) ) = ( prod_ m e. y ( F ` m ) gcd N ) ) )
106 105 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( N gcd prod_ m e. y ( F ` m ) ) = ( prod_ m e. y ( F ` m ) gcd N ) ) )
107 106 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) /\ ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> ( N gcd prod_ m e. y ( F ` m ) ) = ( prod_ m e. y ( F ` m ) gcd N ) )
108 67 a1i 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( y u. { z } ) C_ NN -> y C_ NN ) )
109 idd 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( N e. NN -> N e. NN ) )
110 idd 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( F : NN --> NN -> F : NN --> NN ) )
111 108 109 110 3anim123d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( y C_ NN /\ N e. NN /\ F : NN --> NN ) ) )
112 ssun1 
 |-  y C_ ( y u. { z } )
113 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 -> A. m e. y ( ( F ` m ) gcd N ) = 1 ) )
114 112 113 mp1i 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 -> A. m e. y ( ( F ` m ) gcd N ) = 1 ) )
115 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. m e. y A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
116 112 115 mp1i 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. m e. y A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
117 112 a1i 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ m e. y ) -> y C_ ( y u. { z } ) )
118 117 ssdifd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ m e. y ) -> ( y \ { m } ) C_ ( ( y u. { z } ) \ { m } ) )
119 ssralv 
 |-  ( ( y \ { m } ) C_ ( ( y u. { z } ) \ { m } ) -> ( A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
120 118 119 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ m e. y ) -> ( A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
121 120 ralimdva 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. m e. y A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
122 116 121 syld 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
123 111 114 122 3anim123d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) )
124 123 imim1d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) )
125 124 imp31 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) /\ ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 )
126 107 125 eqtrd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) /\ ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> ( N gcd prod_ m e. y ( F ` m ) ) = 1 )
127 rpmulgcd 
 |-  ( ( ( N e. NN /\ prod_ m e. y ( F ` m ) e. NN /\ ( F ` z ) e. NN ) /\ ( N gcd prod_ m e. y ( F ` m ) ) = 1 ) -> ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) = ( N gcd ( F ` z ) ) )
128 101 126 127 syl2anc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) /\ ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> ( N gcd ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) ) = ( N gcd ( F ` z ) ) )
129 vsnid 
 |-  z e. { z }
130 129 olci 
 |-  ( z e. y \/ z e. { z } )
131 elun 
 |-  ( z e. ( y u. { z } ) <-> ( z e. y \/ z e. { z } ) )
132 130 131 mpbir 
 |-  z e. ( y u. { z } )
133 73 oveq1d 
 |-  ( m = z -> ( ( F ` m ) gcd N ) = ( ( F ` z ) gcd N ) )
134 133 eqeq1d 
 |-  ( m = z -> ( ( ( F ` m ) gcd N ) = 1 <-> ( ( F ` z ) gcd N ) = 1 ) )
135 134 rspcv 
 |-  ( z e. ( y u. { z } ) -> ( A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 -> ( ( F ` z ) gcd N ) = 1 ) )
136 132 135 mp1i 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 -> ( ( F ` z ) gcd N ) = 1 ) )
137 136 imp 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 ) -> ( ( F ` z ) gcd N ) = 1 )
138 77 nnzd 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( F ` z ) e. ZZ )
139 86 138 gcdcomd 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( N gcd ( F ` z ) ) = ( ( F ` z ) gcd N ) )
140 139 eqeq1d 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( ( N gcd ( F ` z ) ) = 1 <-> ( ( F ` z ) gcd N ) = 1 ) )
141 140 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 ) -> ( ( N gcd ( F ` z ) ) = 1 <-> ( ( F ` z ) gcd N ) = 1 ) )
142 137 141 mpbird 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 ) -> ( N gcd ( F ` z ) ) = 1 )
143 142 3adant3 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( N gcd ( F ` z ) ) = 1 )
144 143 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) /\ ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> ( N gcd ( F ` z ) ) = 1 )
145 94 128 144 3eqtrd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) ) /\ ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = 1 )
146 145 exp31 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. y ( ( F ` m ) gcd N ) = 1 /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd N ) = 1 ) -> ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. ( y u. { z } ) ( F ` m ) gcd N ) = 1 ) ) )
147 11 22 33 44 53 146 findcard2s 
 |-  ( M e. Fin -> ( ( ( M C_ NN /\ N e. NN /\ F : NN --> NN ) /\ A. m e. M ( ( F ` m ) gcd N ) = 1 /\ A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. M ( F ` m ) gcd N ) = 1 ) )
148 147 3expd 
 |-  ( M e. Fin -> ( ( M C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( A. m e. M ( ( F ` m ) gcd N ) = 1 -> ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> ( prod_ m e. M ( F ` m ) gcd N ) = 1 ) ) ) )
149 148 3expd 
 |-  ( M e. Fin -> ( M C_ NN -> ( N e. NN -> ( F : NN --> NN -> ( A. m e. M ( ( F ` m ) gcd N ) = 1 -> ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> ( prod_ m e. M ( F ` m ) gcd N ) = 1 ) ) ) ) ) )
150 149 3imp 
 |-  ( ( M e. Fin /\ M C_ NN /\ N e. NN ) -> ( F : NN --> NN -> ( A. m e. M ( ( F ` m ) gcd N ) = 1 -> ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> ( prod_ m e. M ( F ` m ) gcd N ) = 1 ) ) ) )
151 150 3imp 
 |-  ( ( ( M e. Fin /\ M C_ NN /\ N e. NN ) /\ F : NN --> NN /\ A. m e. M ( ( F ` m ) gcd N ) = 1 ) -> ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> ( prod_ m e. M ( F ` m ) gcd N ) = 1 ) )