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

Metamath Proof Explorer

Theorem lcmfunsnlem2lem1

Description: Lemma 1 for lcmfunsnlem2 . (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion lcmfunsnlem2lem1 
|- ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> A. k e. NN ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) <_ k ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ k ( 0 e/ y /\ z =/= 0 /\ n =/= 0 )
2 nfv 
 |-  F/ k n e. ZZ
3 nfv 
 |-  F/ k ( z e. ZZ /\ y C_ ZZ /\ y e. Fin )
4 nfra1 
 |-  F/ k A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k )
5 nfv 
 |-  F/ k A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n )
6 4 5 nfan 
 |-  F/ k ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) )
7 3 6 nfan 
 |-  F/ k ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) )
8 2 7 nfan 
 |-  F/ k ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) )
9 1 8 nfan 
 |-  F/ k ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) )
10 simprr 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> k e. NN )
11 simp2 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> y C_ ZZ )
12 snssi 
 |-  ( z e. ZZ -> { z } C_ ZZ )
13 12 3ad2ant1 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> { z } C_ ZZ )
14 11 13 unssd 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( y u. { z } ) C_ ZZ )
15 simp3 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> y e. Fin )
16 snfi 
 |-  { z } e. Fin
17 unfi 
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
18 15 16 17 sylancl 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( y u. { z } ) e. Fin )
19 14 18 jca 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( ( y u. { z } ) C_ ZZ /\ ( y u. { z } ) e. Fin ) )
20 lcmfcl 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( y u. { z } ) e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. NN0 )
21 19 20 syl 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. NN0 )
22 21 nn0zd 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` ( y u. { z } ) ) e. ZZ )
23 22 adantl 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( _lcm ` ( y u. { z } ) ) e. ZZ )
24 23 adantr 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( _lcm ` ( y u. { z } ) ) e. ZZ )
25 simprl 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> n e. ZZ )
26 10 24 25 3jca 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) )
27 14 adantl 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( y u. { z } ) C_ ZZ )
28 18 adantl 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( y u. { z } ) e. Fin )
29 df-nel 
 |-  ( 0 e/ y <-> -. 0 e. y )
30 29 biimpi 
 |-  ( 0 e/ y -> -. 0 e. y )
31 elsni 
 |-  ( 0 e. { z } -> 0 = z )
32 31 eqcomd 
 |-  ( 0 e. { z } -> z = 0 )
33 32 necon3ai 
 |-  ( z =/= 0 -> -. 0 e. { z } )
34 30 33 anim12i 
 |-  ( ( 0 e/ y /\ z =/= 0 ) -> ( -. 0 e. y /\ -. 0 e. { z } ) )
35 34 3adant3 
 |-  ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( -. 0 e. y /\ -. 0 e. { z } ) )
36 df-nel 
 |-  ( 0 e/ ( y u. { z } ) <-> -. 0 e. ( y u. { z } ) )
37 ioran 
 |-  ( -. ( 0 e. y \/ 0 e. { z } ) <-> ( -. 0 e. y /\ -. 0 e. { z } ) )
38 elun 
 |-  ( 0 e. ( y u. { z } ) <-> ( 0 e. y \/ 0 e. { z } ) )
39 37 38 xchnxbir 
 |-  ( -. 0 e. ( y u. { z } ) <-> ( -. 0 e. y /\ -. 0 e. { z } ) )
40 36 39 bitri 
 |-  ( 0 e/ ( y u. { z } ) <-> ( -. 0 e. y /\ -. 0 e. { z } ) )
41 35 40 sylibr 
 |-  ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> 0 e/ ( y u. { z } ) )
42 41 adantr 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> 0 e/ ( y u. { z } ) )
43 27 28 42 3jca 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) -> ( ( y u. { z } ) C_ ZZ /\ ( y u. { z } ) e. Fin /\ 0 e/ ( y u. { z } ) ) )
44 43 adantr 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( ( y u. { z } ) C_ ZZ /\ ( y u. { z } ) e. Fin /\ 0 e/ ( y u. { z } ) ) )
45 lcmfn0cl 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( y u. { z } ) e. Fin /\ 0 e/ ( y u. { z } ) ) -> ( _lcm ` ( y u. { z } ) ) e. NN )
46 44 45 syl 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( _lcm ` ( y u. { z } ) ) e. NN )
47 46 nnne0d 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( _lcm ` ( y u. { z } ) ) =/= 0 )
48 47 neneqd 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> -. ( _lcm ` ( y u. { z } ) ) = 0 )
49 neneq 
 |-  ( n =/= 0 -> -. n = 0 )
50 49 3ad2ant3 
 |-  ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> -. n = 0 )
51 50 ad2antrr 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> -. n = 0 )
52 48 51 jca 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( -. ( _lcm ` ( y u. { z } ) ) = 0 /\ -. n = 0 ) )
53 ioran 
 |-  ( -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) <-> ( -. ( _lcm ` ( y u. { z } ) ) = 0 /\ -. n = 0 ) )
54 52 53 sylibr 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) )
55 26 54 jca 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) )
56 55 exp43 
 |-  ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( n e. ZZ -> ( k e. NN -> ( ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) ) ) ) )
57 56 adantrd 
 |-  ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) -> ( n e. ZZ -> ( k e. NN -> ( ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) ) ) ) )
58 57 com23 
 |-  ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( n e. ZZ -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) -> ( k e. NN -> ( ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) ) ) ) )
59 58 imp32 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( k e. NN -> ( ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) ) )
60 59 imp 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) /\ k e. NN ) -> ( ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) )
61 60 adantr 
 |-  ( ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) /\ k e. NN ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) )
62 sneq 
 |-  ( n = z -> { n } = { z } )
63 62 uneq2d 
 |-  ( n = z -> ( y u. { n } ) = ( y u. { z } ) )
64 63 fveq2d 
 |-  ( n = z -> ( _lcm ` ( y u. { n } ) ) = ( _lcm ` ( y u. { z } ) ) )
65 oveq2 
 |-  ( n = z -> ( ( _lcm ` y ) lcm n ) = ( ( _lcm ` y ) lcm z ) )
66 64 65 eqeq12d 
 |-  ( n = z -> ( ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) <-> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
67 66 rspcv 
 |-  ( z e. ZZ -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
68 67 3ad2ant1 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) ) )
69 nnz 
 |-  ( k e. NN -> k e. ZZ )
70 69 adantl 
 |-  ( ( n e. ZZ /\ k e. NN ) -> k e. ZZ )
71 70 adantl 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> k e. ZZ )
72 lcmfcl 
 |-  ( ( y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. NN0 )
73 72 nn0zd 
 |-  ( ( y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. ZZ )
74 73 3adant1 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. ZZ )
75 74 ad2antrr 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( _lcm ` y ) e. ZZ )
76 simpll1 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> z e. ZZ )
77 71 75 76 3jca 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) -> ( k e. ZZ /\ ( _lcm ` y ) e. ZZ /\ z e. ZZ ) )
78 77 ad2antrr 
 |-  ( ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( k e. ZZ /\ ( _lcm ` y ) e. ZZ /\ z e. ZZ ) )
79 elun1 
 |-  ( m e. y -> m e. ( y u. { z } ) )
80 79 orcd 
 |-  ( m e. y -> ( m e. ( y u. { z } ) \/ m e. { n } ) )
81 elun 
 |-  ( m e. ( ( y u. { z } ) u. { n } ) <-> ( m e. ( y u. { z } ) \/ m e. { n } ) )
82 80 81 sylibr 
 |-  ( m e. y -> m e. ( ( y u. { z } ) u. { n } ) )
83 breq1 
 |-  ( i = m -> ( i || k <-> m || k ) )
84 83 rspcv 
 |-  ( m e. ( ( y u. { z } ) u. { n } ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> m || k ) )
85 82 84 syl 
 |-  ( m e. y -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> m || k ) )
86 85 com12 
 |-  ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( m e. y -> m || k ) )
87 86 adantl 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( m e. y -> m || k ) )
88 87 ralrimiv 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> A. m e. y m || k )
89 88 adantr 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) /\ ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) ) -> A. m e. y m || k )
90 breq2 
 |-  ( k = l -> ( m || k <-> m || l ) )
91 90 ralbidv 
 |-  ( k = l -> ( A. m e. y m || k <-> A. m e. y m || l ) )
92 breq2 
 |-  ( k = l -> ( ( _lcm ` y ) || k <-> ( _lcm ` y ) || l ) )
93 91 92 imbi12d 
 |-  ( k = l -> ( ( A. m e. y m || k -> ( _lcm ` y ) || k ) <-> ( A. m e. y m || l -> ( _lcm ` y ) || l ) ) )
94 93 cbvralvw 
 |-  ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) <-> A. l e. ZZ ( A. m e. y m || l -> ( _lcm ` y ) || l ) )
95 70 adantr 
 |-  ( ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> k e. ZZ )
96 95 adantl 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) /\ ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) ) -> k e. ZZ )
97 breq2 
 |-  ( l = k -> ( m || l <-> m || k ) )
98 97 ralbidv 
 |-  ( l = k -> ( A. m e. y m || l <-> A. m e. y m || k ) )
99 breq2 
 |-  ( l = k -> ( ( _lcm ` y ) || l <-> ( _lcm ` y ) || k ) )
100 98 99 imbi12d 
 |-  ( l = k -> ( ( A. m e. y m || l -> ( _lcm ` y ) || l ) <-> ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
101 100 rspcv 
 |-  ( k e. ZZ -> ( A. l e. ZZ ( A. m e. y m || l -> ( _lcm ` y ) || l ) -> ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
102 96 101 syl 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) /\ ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) ) -> ( A. l e. ZZ ( A. m e. y m || l -> ( _lcm ` y ) || l ) -> ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
103 94 102 biimtrid 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) /\ ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) ) -> ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
104 89 103 mpid 
 |-  ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) /\ ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) ) -> ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( _lcm ` y ) || k ) )
105 104 exp31 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( _lcm ` y ) || k ) ) ) )
106 105 com24 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` y ) || k ) ) ) )
107 106 imp 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) -> ( ( ( n e. ZZ /\ k e. NN ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` y ) || k ) ) )
108 107 impl 
 |-  ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` y ) || k ) )
109 108 imp 
 |-  ( ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( _lcm ` y ) || k )
110 vsnid 
 |-  z e. { z }
111 110 olci 
 |-  ( z e. y \/ z e. { z } )
112 elun 
 |-  ( z e. ( y u. { z } ) <-> ( z e. y \/ z e. { z } ) )
113 111 112 mpbir 
 |-  z e. ( y u. { z } )
114 113 orci 
 |-  ( z e. ( y u. { z } ) \/ z e. { n } )
115 elun 
 |-  ( z e. ( ( y u. { z } ) u. { n } ) <-> ( z e. ( y u. { z } ) \/ z e. { n } ) )
116 114 115 mpbir 
 |-  z e. ( ( y u. { z } ) u. { n } )
117 breq1 
 |-  ( i = z -> ( i || k <-> z || k ) )
118 117 rspcv 
 |-  ( z e. ( ( y u. { z } ) u. { n } ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> z || k ) )
119 116 118 mp1i 
 |-  ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> z || k ) )
120 119 imp 
 |-  ( ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> z || k )
121 109 120 jca 
 |-  ( ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( ( _lcm ` y ) || k /\ z || k ) )
122 lcmdvds 
 |-  ( ( k e. ZZ /\ ( _lcm ` y ) e. ZZ /\ z e. ZZ ) -> ( ( ( _lcm ` y ) || k /\ z || k ) -> ( ( _lcm ` y ) lcm z ) || k ) )
123 78 121 122 sylc 
 |-  ( ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( ( _lcm ` y ) lcm z ) || k )
124 breq1 
 |-  ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( ( _lcm ` ( y u. { z } ) ) || k <-> ( ( _lcm ` y ) lcm z ) || k ) )
125 123 124 imbitrrid 
 |-  ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( _lcm ` ( y u. { z } ) ) || k ) )
126 125 expd 
 |-  ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( ( ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) /\ ( n e. ZZ /\ k e. NN ) ) /\ ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) )
127 126 exp5j 
 |-  ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( ( n e. ZZ /\ k e. NN ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) ) ) )
128 127 com12 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) -> ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( ( n e. ZZ /\ k e. NN ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) ) ) )
129 68 128 syld 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( ( n e. ZZ /\ k e. NN ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) ) ) )
130 129 com23 
 |-  ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) -> ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) -> ( A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) -> ( ( n e. ZZ /\ k e. NN ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) ) ) )
131 130 imp32 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) -> ( ( n e. ZZ /\ k e. NN ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) )
132 131 expd 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) -> ( n e. ZZ -> ( k e. NN -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) ) )
133 132 com34 
 |-  ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) -> ( n e. ZZ -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( k e. NN -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) ) )
134 133 com12 
 |-  ( n e. ZZ -> ( ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( k e. NN -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) ) )
135 134 imp 
 |-  ( ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) -> ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( k e. NN -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) )
136 135 com12 
 |-  ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) -> ( ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) -> ( k e. NN -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) ) )
137 136 imp 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( k e. NN -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) )
138 137 imp 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) /\ k e. NN ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( _lcm ` ( y u. { z } ) ) || k ) )
139 138 imp 
 |-  ( ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) /\ k e. NN ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( _lcm ` ( y u. { z } ) ) || k )
140 vsnid 
 |-  n e. { n }
141 140 olci 
 |-  ( n e. ( y u. { z } ) \/ n e. { n } )
142 elun 
 |-  ( n e. ( ( y u. { z } ) u. { n } ) <-> ( n e. ( y u. { z } ) \/ n e. { n } ) )
143 141 142 mpbir 
 |-  n e. ( ( y u. { z } ) u. { n } )
144 breq1 
 |-  ( i = n -> ( i || k <-> n || k ) )
145 144 rspcv 
 |-  ( n e. ( ( y u. { z } ) u. { n } ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> n || k ) )
146 143 145 mp1i 
 |-  ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) /\ k e. NN ) -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> n || k ) )
147 146 imp 
 |-  ( ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) /\ k e. NN ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> n || k )
148 139 147 jca 
 |-  ( ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) /\ k e. NN ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( ( _lcm ` ( y u. { z } ) ) || k /\ n || k ) )
149 lcmledvds 
 |-  ( ( ( k e. NN /\ ( _lcm ` ( y u. { z } ) ) e. ZZ /\ n e. ZZ ) /\ -. ( ( _lcm ` ( y u. { z } ) ) = 0 \/ n = 0 ) ) -> ( ( ( _lcm ` ( y u. { z } ) ) || k /\ n || k ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) <_ k ) )
150 61 148 149 sylc 
 |-  ( ( ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) /\ k e. NN ) /\ A. i e. ( ( y u. { z } ) u. { n } ) i || k ) -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) <_ k )
151 150 exp31 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> ( k e. NN -> ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) <_ k ) ) )
152 9 151 ralrimi 
 |-  ( ( ( 0 e/ y /\ z =/= 0 /\ n =/= 0 ) /\ ( n e. ZZ /\ ( ( z e. ZZ /\ y C_ ZZ /\ y e. Fin ) /\ ( A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) /\ A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) ) ) ) -> A. k e. NN ( A. i e. ( ( y u. { z } ) u. { n } ) i || k -> ( ( _lcm ` ( y u. { z } ) ) lcm n ) <_ k ) )