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 biimpri 
 |-  ( { z } C_ NN -> z e. NN )
61 60 adantl 
 |-  ( ( y C_ NN /\ { z } C_ NN ) -> z e. NN )
62 57 61 sylbir 
 |-  ( ( y u. { z } ) C_ NN -> z e. NN )
63 62 3ad2ant1 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> z e. NN )
64 63 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> z e. NN )
65 simprr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> -. z e. y )
66 simpll3 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> F : NN --> NN )
67 simpl 
 |-  ( ( y C_ NN /\ { z } C_ NN ) -> y C_ NN )
68 57 67 sylbir 
 |-  ( ( y u. { z } ) C_ NN -> y C_ NN )
69 68 3ad2ant1 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> y C_ NN )
70 69 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> y C_ NN )
71 70 sselda 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> m e. NN )
72 66 71 ffvelrnd 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> ( F ` m ) e. NN )
73 72 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 )
74 fveq2 
 |-  ( m = z -> ( F ` m ) = ( F ` z ) )
75 simpr 
 |-  ( ( ( y u. { z } ) C_ NN /\ F : NN --> NN ) -> F : NN --> NN )
76 62 adantr 
 |-  ( ( ( y u. { z } ) C_ NN /\ F : NN --> NN ) -> z e. NN )
77 75 76 ffvelrnd 
 |-  ( ( ( y u. { z } ) C_ NN /\ F : NN --> NN ) -> ( F ` z ) e. NN )
78 77 3adant2 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( F ` z ) e. NN )
79 78 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( F ` z ) e. NN )
80 79 nncnd 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( F ` z ) e. CC )
81 54 55 56 64 65 73 74 80 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 ) ) )
82 81 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 ) )
83 56 72 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 )
84 83 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 )
85 79 nnzd 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( F ` z ) e. ZZ )
86 84 85 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 )
87 48 3ad2ant2 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> N e. ZZ )
88 87 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> N e. ZZ )
89 86 88 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 ) ) ) )
90 82 89 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 ) ) ) )
91 90 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 ) ) ) ) )
92 91 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 ) ) ) ) )
93 92 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 ) ) ) ) )
94 93 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 ) ) ) ) )
95 94 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 ) ) ) )
96 simpl2 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) /\ ( y e. Fin /\ -. z e. y ) ) -> N e. NN )
97 96 83 79 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 ) )
98 97 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 ) ) )
99 98 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 ) ) )
100 99 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 ) ) )
101 100 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 ) ) )
102 101 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 ) )
103 88 84 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 ) )
104 103 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 ) ) )
105 104 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 ) ) )
106 105 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 ) ) )
107 106 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 ) ) )
108 107 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 ) )
109 68 a1i 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( y u. { z } ) C_ NN -> y C_ NN ) )
110 idd 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( N e. NN -> N e. NN ) )
111 idd 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( F : NN --> NN -> F : NN --> NN ) )
112 109 110 111 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 ) ) )
113 ssun1 
 |-  y C_ ( y u. { z } )
114 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 ) )
115 113 114 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 ) )
116 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 ) )
117 113 116 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 ) )
118 113 a1i 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ m e. y ) -> y C_ ( y u. { z } ) )
119 118 ssdifd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ m e. y ) -> ( y \ { m } ) C_ ( ( y u. { z } ) \ { m } ) )
120 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 ) )
121 119 120 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 ) )
122 121 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 ) )
123 117 122 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 ) )
124 112 115 123 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 ) ) )
125 124 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 ) ) )
126 125 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 )
127 108 126 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 )
128 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 ) ) )
129 102 127 128 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 ) ) )
130 vsnid 
 |-  z e. { z }
131 130 olci 
 |-  ( z e. y \/ z e. { z } )
132 elun 
 |-  ( z e. ( y u. { z } ) <-> ( z e. y \/ z e. { z } ) )
133 131 132 mpbir 
 |-  z e. ( y u. { z } )
134 74 oveq1d 
 |-  ( m = z -> ( ( F ` m ) gcd N ) = ( ( F ` z ) gcd N ) )
135 134 eqeq1d 
 |-  ( m = z -> ( ( ( F ` m ) gcd N ) = 1 <-> ( ( F ` z ) gcd N ) = 1 ) )
136 135 rspcv 
 |-  ( z e. ( y u. { z } ) -> ( A. m e. ( y u. { z } ) ( ( F ` m ) gcd N ) = 1 -> ( ( F ` z ) gcd N ) = 1 ) )
137 133 136 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 ) )
138 137 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 )
139 78 nnzd 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( F ` z ) e. ZZ )
140 87 139 gcdcomd 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( N gcd ( F ` z ) ) = ( ( F ` z ) gcd N ) )
141 140 eqeq1d 
 |-  ( ( ( y u. { z } ) C_ NN /\ N e. NN /\ F : NN --> NN ) -> ( ( N gcd ( F ` z ) ) = 1 <-> ( ( F ` z ) gcd N ) = 1 ) )
142 141 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 ) )
143 138 142 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 )
144 143 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 )
145 144 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 )
146 95 129 145 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 )
147 146 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 ) ) )
148 11 22 33 44 53 147 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 ) )
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 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 ) ) ) ) ) )
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 ) ) ) )
152 151 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 ) )