This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coprmproddvdslem

Description: Lemma for coprmproddvds : Induction step. (Contributed by AV, 19-Aug-2020)

Ref Expression
Assertion coprmproddvdslem 
|- ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) -> ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> prod_ m e. ( y u. { z } ) ( F ` m ) || K ) ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ m ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) )
2 nfcv 
 |-  F/_ m ( F ` z )
3 simpll 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> y e. Fin )
4 unss 
 |-  ( ( y C_ NN /\ { z } C_ NN ) <-> ( y u. { z } ) C_ NN )
5 vex 
 |-  z e. _V
6 5 snss 
 |-  ( z e. NN <-> { z } C_ NN )
7 6 biimpri 
 |-  ( { z } C_ NN -> z e. NN )
8 7 adantl 
 |-  ( ( y C_ NN /\ { z } C_ NN ) -> z e. NN )
9 4 8 sylbir 
 |-  ( ( y u. { z } ) C_ NN -> z e. NN )
10 9 adantr 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> z e. NN )
11 10 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> z e. NN )
12 simplr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> -. z e. y )
13 simprrr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> F : NN --> NN )
14 13 adantr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> F : NN --> NN )
15 simpl 
 |-  ( ( y C_ NN /\ { z } C_ NN ) -> y C_ NN )
16 4 15 sylbir 
 |-  ( ( y u. { z } ) C_ NN -> y C_ NN )
17 16 adantr 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> y C_ NN )
18 17 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> y C_ NN )
19 18 sselda 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> m e. NN )
20 14 19 ffvelcdmd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> ( F ` m ) e. NN )
21 20 nncnd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> ( F ` m ) e. CC )
22 fveq2 
 |-  ( m = z -> ( F ` m ) = ( F ` z ) )
23 13 11 ffvelcdmd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( F ` z ) e. NN )
24 23 nncnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( F ` z ) e. CC )
25 1 2 3 11 12 21 22 24 fprodsplitsn 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> prod_ m e. ( y u. { z } ) ( F ` m ) = ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) )
26 25 ad2ant2r 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> prod_ m e. ( y u. { z } ) ( F ` m ) = ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) )
27 simprl 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) -> y e. Fin )
28 simprr 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> F : NN --> NN )
29 28 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) -> F : NN --> NN )
30 29 adantr 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> F : NN --> NN )
31 17 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) -> y C_ NN )
32 31 sselda 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> m e. NN )
33 30 32 ffvelcdmd 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> ( F ` m ) e. NN )
34 27 33 fprodnncl 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) -> prod_ m e. y ( F ` m ) e. NN )
35 34 ex 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( ( y e. Fin /\ -. z e. y ) -> prod_ m e. y ( F ` m ) e. NN ) )
36 35 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> ( ( y e. Fin /\ -. z e. y ) -> prod_ m e. y ( F ` m ) e. NN ) )
37 36 com12 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) e. NN ) )
38 37 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) -> ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) e. NN ) )
39 38 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> prod_ m e. y ( F ` m ) e. NN )
40 39 nnzd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> prod_ m e. y ( F ` m ) e. ZZ )
41 28 10 ffvelcdmd 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( F ` z ) e. NN )
42 41 nnzd 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( F ` z ) e. ZZ )
43 42 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> ( F ` z ) e. ZZ )
44 43 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> ( F ` z ) e. ZZ )
45 nnz 
 |-  ( K e. NN -> K e. ZZ )
46 45 adantr 
 |-  ( ( K e. NN /\ F : NN --> NN ) -> K e. ZZ )
47 46 adantl 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> K e. ZZ )
48 47 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> K e. ZZ )
49 48 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> K e. ZZ )
50 40 44 49 3jca 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> ( prod_ m e. y ( F ` m ) e. ZZ /\ ( F ` z ) e. ZZ /\ K e. ZZ ) )
51 simpl 
 |-  ( ( F : NN --> NN /\ ( y u. { z } ) C_ NN ) -> F : NN --> NN )
52 9 adantl 
 |-  ( ( F : NN --> NN /\ ( y u. { z } ) C_ NN ) -> z e. NN )
53 51 52 ffvelcdmd 
 |-  ( ( F : NN --> NN /\ ( y u. { z } ) C_ NN ) -> ( F ` z ) e. NN )
54 53 ex 
 |-  ( F : NN --> NN -> ( ( y u. { z } ) C_ NN -> ( F ` z ) e. NN ) )
55 54 adantl 
 |-  ( ( K e. NN /\ F : NN --> NN ) -> ( ( y u. { z } ) C_ NN -> ( F ` z ) e. NN ) )
56 55 impcom 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( F ` z ) e. NN )
57 56 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( F ` z ) e. NN )
58 3 18 57 3jca 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( y e. Fin /\ y C_ NN /\ ( F ` z ) e. NN ) )
59 58 adantr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( y e. Fin /\ y C_ NN /\ ( F ` z ) e. NN ) )
60 13 adantr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> F : NN --> NN )
61 vsnid 
 |-  z e. { z }
62 61 olci 
 |-  ( z e. y \/ z e. { z } )
63 elun 
 |-  ( z e. ( y u. { z } ) <-> ( z e. y \/ z e. { z } ) )
64 62 63 mpbir 
 |-  z e. ( y u. { z } )
65 64 a1i 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> z e. ( y u. { z } ) )
66 snssi 
 |-  ( m e. y -> { m } C_ y )
67 66 ssneld 
 |-  ( m e. y -> ( -. z e. y -> -. z e. { m } ) )
68 67 com12 
 |-  ( -. z e. y -> ( m e. y -> -. z e. { m } ) )
69 68 adantl 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( m e. y -> -. z e. { m } ) )
70 69 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( m e. y -> -. z e. { m } ) )
71 70 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> -. z e. { m } )
72 65 71 eldifd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> z e. ( ( y u. { z } ) \ { m } ) )
73 fveq2 
 |-  ( n = z -> ( F ` n ) = ( F ` z ) )
74 73 oveq2d 
 |-  ( n = z -> ( ( F ` m ) gcd ( F ` n ) ) = ( ( F ` m ) gcd ( F ` z ) ) )
75 74 eqeq1d 
 |-  ( n = z -> ( ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> ( ( F ` m ) gcd ( F ` z ) ) = 1 ) )
76 75 rspcv 
 |-  ( z e. ( ( y u. { z } ) \ { m } ) -> ( A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> ( ( F ` m ) gcd ( F ` z ) ) = 1 ) )
77 72 76 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> ( A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> ( ( F ` m ) gcd ( F ` z ) ) = 1 ) )
78 77 ralimdva 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( A. m e. y A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. m e. y ( ( F ` m ) gcd ( F ` z ) ) = 1 ) )
79 ralunb 
 |-  ( 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 /\ A. m e. { z } A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
80 79 simplbi 
 |-  ( 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 )
81 78 80 impel 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> A. m e. y ( ( F ` m ) gcd ( F ` z ) ) = 1 )
82 raldifb 
 |-  ( A. n e. ( y u. { z } ) ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) <-> A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 )
83 ralunb 
 |-  ( A. n e. ( y u. { z } ) ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) <-> ( A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) /\ A. n e. { z } ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) )
84 raldifb 
 |-  ( A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) <-> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 )
85 84 biimpi 
 |-  ( A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 )
86 85 adantr 
 |-  ( ( A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) /\ A. n e. { z } ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) ) -> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 )
87 83 86 sylbi 
 |-  ( A. n e. ( y u. { z } ) ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 )
88 82 87 sylbir 
 |-  ( A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 )
89 88 ralimi 
 |-  ( 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 )
90 89 adantr 
 |-  ( ( A. m e. y A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. { 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 )
91 79 90 sylbi 
 |-  ( 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 )
92 91 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ 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 )
93 coprmprod 
 |-  ( ( ( y e. Fin /\ y C_ NN /\ ( F ` z ) e. NN ) /\ F : NN --> NN /\ A. m e. y ( ( F ` m ) gcd ( F ` z ) ) = 1 ) -> ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> ( prod_ m e. y ( F ` m ) gcd ( F ` z ) ) = 1 ) )
94 93 imp 
 |-  ( ( ( ( y e. Fin /\ y C_ NN /\ ( F ` z ) e. NN ) /\ F : NN --> NN /\ A. m e. y ( ( F ` m ) gcd ( F ` z ) ) = 1 ) /\ A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> ( prod_ m e. y ( F ` m ) gcd ( F ` z ) ) = 1 )
95 59 60 81 92 94 syl31anc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ 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 ( F ` z ) ) = 1 )
96 95 ex 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( 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 ( F ` z ) ) = 1 ) )
97 96 adantrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) -> ( prod_ m e. y ( F ` m ) gcd ( F ` z ) ) = 1 ) )
98 97 expimpd 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> ( prod_ m e. y ( F ` m ) gcd ( F ` z ) ) = 1 ) )
99 98 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) -> ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> ( prod_ m e. y ( F ` m ) gcd ( F ` z ) ) = 1 ) )
100 99 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> ( prod_ m e. y ( F ` m ) gcd ( F ` z ) ) = 1 )
101 83 simplbi 
 |-  ( A. n e. ( y u. { z } ) ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
102 82 101 sylbir 
 |-  ( A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 -> A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
103 102 ralimi 
 |-  ( 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 ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
104 103 adantr 
 |-  ( ( A. m e. y A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. { z } A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) -> A. m e. y A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
105 79 104 sylbi 
 |-  ( 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 ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
106 ralunb 
 |-  ( A. m e. ( y u. { z } ) ( F ` m ) || K <-> ( A. m e. y ( F ` m ) || K /\ A. m e. { z } ( F ` m ) || K ) )
107 106 simplbi 
 |-  ( A. m e. ( y u. { z } ) ( F ` m ) || K -> A. m e. y ( F ` m ) || K )
108 84 ralbii 
 |-  ( A. m e. y A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) <-> A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 )
109 108 anbi1i 
 |-  ( ( A. m e. y A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) /\ A. m e. y ( F ` m ) || K ) <-> ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) )
110 17 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> y C_ NN )
111 simprrl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> K e. NN )
112 simprrr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> F : NN --> NN )
113 110 111 112 jca32 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) )
114 simplr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) )
115 pm2.27 
 |-  ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> ( ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) -> prod_ m e. y ( F ` m ) || K ) )
116 113 114 115 syl2anc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) -> prod_ m e. y ( F ` m ) || K ) )
117 116 exp31 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) -> ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) -> prod_ m e. y ( F ` m ) || K ) ) ) )
118 117 com24 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) -> ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) -> prod_ m e. y ( F ` m ) || K ) ) ) )
119 118 imp 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) -> ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) -> prod_ m e. y ( F ` m ) || K ) ) )
120 119 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) -> prod_ m e. y ( F ` m ) || K ) )
121 109 120 biimtrid 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( ( A. m e. y A. n e. y ( n e/ { m } -> ( ( F ` m ) gcd ( F ` n ) ) = 1 ) /\ A. m e. y ( F ` m ) || K ) -> prod_ m e. y ( F ` m ) || K ) )
122 105 107 121 syl2ani 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) -> prod_ m e. y ( F ` m ) || K ) )
123 122 impr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> prod_ m e. y ( F ` m ) || K )
124 22 breq1d 
 |-  ( m = z -> ( ( F ` m ) || K <-> ( F ` z ) || K ) )
125 124 rspcv 
 |-  ( z e. ( y u. { z } ) -> ( A. m e. ( y u. { z } ) ( F ` m ) || K -> ( F ` z ) || K ) )
126 64 125 ax-mp 
 |-  ( A. m e. ( y u. { z } ) ( F ` m ) || K -> ( F ` z ) || K )
127 126 adantl 
 |-  ( ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) -> ( F ` z ) || K )
128 127 adantl 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> ( F ` z ) || K )
129 128 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> ( F ` z ) || K )
130 coprmdvds2 
 |-  ( ( ( prod_ m e. y ( F ` m ) e. ZZ /\ ( F ` z ) e. ZZ /\ K e. ZZ ) /\ ( prod_ m e. y ( F ` m ) gcd ( F ` z ) ) = 1 ) -> ( ( prod_ m e. y ( F ` m ) || K /\ ( F ` z ) || K ) -> ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) || K ) )
131 130 imp 
 |-  ( ( ( ( prod_ m e. y ( F ` m ) e. ZZ /\ ( F ` z ) e. ZZ /\ K e. ZZ ) /\ ( prod_ m e. y ( F ` m ) gcd ( F ` z ) ) = 1 ) /\ ( prod_ m e. y ( F ` m ) || K /\ ( F ` z ) || K ) ) -> ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) || K )
132 50 100 123 129 131 syl22anc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> ( prod_ m e. y ( F ` m ) x. ( F ` z ) ) || K )
133 26 132 eqbrtrd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) /\ ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) -> prod_ m e. ( y u. { z } ) ( F ` m ) || K )
134 133 exp31 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) -> ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> prod_ m e. ( y u. { z } ) ( F ` m ) || K ) ) )