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 bilanri 
 |-  ( ( y C_ NN /\ { z } C_ NN ) -> z e. NN )
8 4 7 sylbir 
 |-  ( ( y u. { z } ) C_ NN -> z e. NN )
9 8 adantr 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> z e. NN )
10 9 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> z e. NN )
11 simplr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> -. z e. y )
12 simprrr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> F : NN --> NN )
13 12 adantr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> F : NN --> NN )
14 simpl 
 |-  ( ( y C_ NN /\ { z } C_ NN ) -> y C_ NN )
15 4 14 sylbir 
 |-  ( ( y u. { z } ) C_ NN -> y C_ NN )
16 15 adantr 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> y C_ NN )
17 16 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> y C_ NN )
18 17 sselda 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> m e. NN )
19 13 18 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 )
20 19 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 )
21 fveq2 
 |-  ( m = z -> ( F ` m ) = ( F ` z ) )
22 12 10 ffvelcdmd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( F ` z ) e. NN )
23 22 nncnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( F ` z ) e. CC )
24 1 2 3 10 11 20 21 23 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 ) ) )
25 24 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 ) ) )
26 simprl 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) -> y e. Fin )
27 simprr 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> F : NN --> NN )
28 27 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) -> F : NN --> NN )
29 28 adantr 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> F : NN --> NN )
30 16 adantr 
 |-  ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) -> y C_ NN )
31 30 sselda 
 |-  ( ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( y e. Fin /\ -. z e. y ) ) /\ m e. y ) -> m e. NN )
32 29 31 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 )
33 26 32 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 )
34 33 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 ) )
35 34 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 ) )
36 35 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 ) )
37 36 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 ) )
38 37 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 )
39 38 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 )
40 27 9 ffvelcdmd 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( F ` z ) e. NN )
41 40 nnzd 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( F ` z ) e. ZZ )
42 41 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 )
43 42 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 )
44 nnz 
 |-  ( K e. NN -> K e. ZZ )
45 44 adantr 
 |-  ( ( K e. NN /\ F : NN --> NN ) -> K e. ZZ )
46 45 adantl 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> K e. ZZ )
47 46 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 )
48 47 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 )
49 39 43 48 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 ) )
50 simpl 
 |-  ( ( F : NN --> NN /\ ( y u. { z } ) C_ NN ) -> F : NN --> NN )
51 8 adantl 
 |-  ( ( F : NN --> NN /\ ( y u. { z } ) C_ NN ) -> z e. NN )
52 50 51 ffvelcdmd 
 |-  ( ( F : NN --> NN /\ ( y u. { z } ) C_ NN ) -> ( F ` z ) e. NN )
53 52 ex 
 |-  ( F : NN --> NN -> ( ( y u. { z } ) C_ NN -> ( F ` z ) e. NN ) )
54 53 adantl 
 |-  ( ( K e. NN /\ F : NN --> NN ) -> ( ( y u. { z } ) C_ NN -> ( F ` z ) e. NN ) )
55 54 impcom 
 |-  ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) -> ( F ` z ) e. NN )
56 55 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( F ` z ) e. NN )
57 3 17 56 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 ) )
58 57 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 ) )
59 12 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 )
60 vsnid 
 |-  z e. { z }
61 60 olci 
 |-  ( z e. y \/ z e. { z } )
62 elun 
 |-  ( z e. ( y u. { z } ) <-> ( z e. y \/ z e. { z } ) )
63 61 62 mpbir 
 |-  z e. ( y u. { z } )
64 63 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 } ) )
65 snssi 
 |-  ( m e. y -> { m } C_ y )
66 65 ssneld 
 |-  ( m e. y -> ( -. z e. y -> -. z e. { m } ) )
67 66 com12 
 |-  ( -. z e. y -> ( m e. y -> -. z e. { m } ) )
68 67 adantl 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( m e. y -> -. z e. { m } ) )
69 68 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) -> ( m e. y -> -. z e. { m } ) )
70 69 imp 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) /\ m e. y ) -> -. z e. { m } )
71 64 70 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 } ) )
72 fveq2 
 |-  ( n = z -> ( F ` n ) = ( F ` z ) )
73 72 oveq2d 
 |-  ( n = z -> ( ( F ` m ) gcd ( F ` n ) ) = ( ( F ` m ) gcd ( F ` z ) ) )
74 73 eqeq1d 
 |-  ( n = z -> ( ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> ( ( F ` m ) gcd ( F ` z ) ) = 1 ) )
75 74 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 ) )
76 71 75 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 ) )
77 76 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 ) )
78 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 ) )
79 78 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 )
80 77 79 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 )
81 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 )
82 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 ) ) )
83 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 )
84 83 birani 
 |-  ( ( 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 )
85 82 84 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 )
86 81 85 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 )
87 86 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 )
88 87 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 )
89 78 88 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 )
90 89 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 )
91 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 ) )
92 91 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 )
93 58 59 80 90 92 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 )
94 93 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 ) )
95 94 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 ) )
96 95 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 ) )
97 96 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 ) )
98 97 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 )
99 82 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 ) )
100 81 99 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 ) )
101 100 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 ) )
102 101 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 ) )
103 78 102 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 ) )
104 ralunb 
 |-  ( A. m e. ( y u. { z } ) ( F ` m ) || K <-> ( A. m e. y ( F ` m ) || K /\ A. m e. { z } ( F ` m ) || K ) )
105 104 simplbi 
 |-  ( A. m e. ( y u. { z } ) ( F ` m ) || K -> A. m e. y ( F ` m ) || K )
106 83 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 )
107 106 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 ) )
108 16 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 )
109 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 )
110 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 )
111 108 109 110 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 ) ) )
112 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 ) )
113 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 ) )
114 111 112 113 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 ) )
115 114 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 ) ) ) )
116 115 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 ) ) ) )
117 116 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 ) ) )
118 117 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 ) )
119 107 118 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 ) )
120 103 105 119 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 ) )
121 120 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 )
122 21 breq1d 
 |-  ( m = z -> ( ( F ` m ) || K <-> ( F ` z ) || K ) )
123 122 rspcv 
 |-  ( z e. ( y u. { z } ) -> ( A. m e. ( y u. { z } ) ( F ` m ) || K -> ( F ` z ) || K ) )
124 63 123 ax-mp 
 |-  ( A. m e. ( y u. { z } ) ( F ` m ) || K -> ( F ` z ) || K )
125 124 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 )
126 125 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 )
127 126 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 )
128 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 ) )
129 128 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 )
130 49 98 121 127 129 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 )
131 25 130 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 )
132 131 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 ) ) )